AutoSamplingTheory.SALD.cycle54MainSkeletonAnalyticMiddleContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.MainSkeletonAnalyticInterfaceLedger. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle54MainSkeletonAnalyticMiddleContract :
    MainSkeletonAnalyticInterfaceLedger

Construction and field-by-field explanation

Construct a data record from explicit fields and the audited defaults shown below.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteDerivativeSource — audited data reference, not expanded and not a compiled dependency edge

objective : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Cycle 54 middle: audit the upper analytic-interface re-check against the six theorem consumers, sharpen the lower packet for appendix.tex:1354-1387, and keep all slow analytic backends below formalized status.

sourceLabels : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. appendix.tex:47-79
2. main_body.tex:202-215
3. appendix.tex:168-252
4. appendix.tex:724-951
5. main_body.tex:359-395
6. appendix.tex:1313-1603
7. appendix.tex:1354-1387

analyticInterfaces : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. Gronwall: theorem consumers use SALD.saldGronwallEndpointCalculusContract plus cycle-36/41 assembly wrappers; the source-level endpoint-safe differentiability/FTC bridge and theorem-specific coefficient regularity stay obligations.
2. DV: theorem consumers use dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, and theorem-specific finite-log-mgf witnesses; common space, absolute continuity, finite KL/log-likelihood, measurability, and finite log-mgf stay source-cited or obligations.
3. LSI/KL/FI: theorem consumers use SALD.saldLsiKlFiDensityTestContract and cycle-43 density/entropy/Fisher-chain helpers; zero-set handling, admissible sqrt-density test or approximation, vector Fisher chain rule, and finite theorem-level KL/FI stay obligations.
4. Continuous Fokker-Planck/KL derivative: forward-KL and continuous general moving-target consumers use SALD.forwardKlDerivativeSideConditionContract, SALD.generalMovingTargetDerivativeCandidateContract, and the cycle-50/52 scalar handoffs; density, boundary, integration-by-parts, transport, and schedule calculus stay obligations.
5. Euler-Maruyama interpolation Fokker-Planck: discrete theorem consumers use SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, the cycle-48/53 endpoint-law handoffs, and SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff for the cycle-54 sigma-weighted divergence regrouping; conditional drift, density/absolute-continuity, weak FP, KL differentiation, and integration by parts stay obligations.

theoremRoute : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. 1. thm:forward-KL remains routed through continuous derivative, LSI, DV velocity, endpoint schedule, and Gronwall side conditions.
2. 2. thm:forward-KL-discrete remains routed through EM conditional-FP, frozen defect, LSI, DV velocity, stitched Gronwall, and accumulated-error interfaces.
3. 3. prop:guided_path_residual remains routed through normalizer differentiation, guided-density differentiation, divergence cancellation, and mean-zero residual obligations.
4. 4. thm:general-moving-target-SALD remains routed through continuous general derivative, residual LSI/DV, sigma-weighted Gronwall, endpoint/exponent, and pure-contraction obligations.
5. 5. thm:unified-forward-KL remains the source specialization of the continuous general theorem via guided residual and the correction-field transport bridge.
6. 6. thm:general-moving-target-SALD-discrete remains routed through general EM endpoint/conditional-FP, frozen delta, discrete KL derivative/LSI, residual DV, constant schedule, and Gronwall stitching.

modeDiscipline : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. faithfulPaper Phase 1: use only original main_body.tex, appendix.tex, and iteration_complexity.tex; sald_version_2.tex remains excluded.
2. Do not change theorem statements, constants, alpha ranges, sigma factors, source labels, or proof routes.
3. Do not classify endpoint-law handoffs as Brownian construction, regular conditional drift, density, weak Fokker-Planck, or KL derivative proofs.
4. Keep systematic SLT/SDE backfill deferred until theorem skeleton interfaces remain green.

nonGoals : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. No new scalar-only lemma unless it directly discharges appendix.tex:1354-1387 endpoint or conditional-law obligations.
2. No imported SLT or external theorem is promoted for DV, LSI, disintegration, concentration, or EM one-step analysis.
3. No hidden endpoint, density, absolute-continuity, finite-KL/FI, finite-log-mgf, boundary, smoothness, conditional-law, or stitched-interval assumptions are added to a paper theorem.
4. No alternate proof route replaces derivative -> LSI -> DV -> Gronwall or the paper EM/frozen-delta route.

lowerPacket : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. Target exactly SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.
2. First lower sub-slice remains appendix.tex:1354-1387 after the endpoint-law handoff: common probability space, hat rho_s and tilde pi_s density/absolute-continuity, regular conditional drift bar b_{k,s}, weak conditional Fokker-Planck equation, KL differentiation under the integral, and integration-by-parts side conditions.
3. Use SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation only as pushforward endpoint-law bookkeeping from named interpolation identities.
4. If conditional-FP is blocked, sharpen the source-cited interface by naming the common-space, absolute-continuity, finite-KL/FI, measurability, endpoint, conditional-law, and weak-FP hypotheses rather than modifying theorem statements.

reviewerChecklist : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. SALD.cycle54MainSkeletonAnalyticMiddleObligation is listed by all six theorem contracts and in saldDependenciesForLabel through the cycle-54 dependency list.
2. SALD.cycle54MainSkeletonAnalyticInterfaceDag contains ASTIS.SALD.cycle54.middle_interface_audit between the upper re-check and lower packet.
3. The conversion window and proof-obligation ledger contain the cycle-54 middle audit and keep appendix.tex:1354-1387 as the lower target.
4. Gronwall, DV, LSI/KL/FI, continuous derivative, EM conditional-FP, and theorem statements are not promoted beyond their current statuses.
5. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

dependencies : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. SALD.cycle54MainSkeletonAnalyticInterfaceLedger
2. SALD.cycle54MainSkeletonAnalyticInterfaceObligation
3. SALD.cycle49MainSkeletonAnalyticMiddleObligation
4. SALD.cycle50ForwardKlSkeletonMiddleObligation
5. SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation
6. SALD.cycle52GuidedGeneralSkeletonMiddleObligation
7. SALD.cycle53UnifiedDiscreteGeneralMiddleObligation
8. SALD.saldGronwallEndpointCalculusContract
9. dvVariationalFormulaInterface saldDvVariationSource
10. SALD.saldLsiKlFiDensityTestContract
11. SALD.forwardKlDerivativeSideConditionContract
12. SALD.generalMovingTargetDerivativeCandidateContract
13. SALD.discreteForwardKlEmInterpolationSideConditionContract
14. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
15. SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation
16. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
17. SALD.cycle54GeneralMovingTargetDiscreteEmFpLowerObligation
18. sald.general_moving_target_discrete.em_interpolation_fp
19. sald.general_moving_target_discrete.kl_derivative

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def cycle54MainSkeletonAnalyticMiddleContract :
    MainSkeletonAnalyticInterfaceLedger where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  objective := "Cycle 54 middle: audit the upper analytic-interface re-check against the six theorem consumers, sharpen the lower packet for appendix.tex:1354-1387, and keep all slow analytic backends below formalized status."
  sourceLabels := [
    "appendix.tex:47-79",
    "main_body.tex:202-215",
    "appendix.tex:168-252",
    "appendix.tex:724-951",
    "main_body.tex:359-395",
    "appendix.tex:1313-1603",
    "appendix.tex:1354-1387"
  ]
  analyticInterfaces := [
    "Gronwall: theorem consumers use SALD.saldGronwallEndpointCalculusContract plus cycle-36/41 assembly wrappers; the source-level endpoint-safe differentiability/FTC bridge and theorem-specific coefficient regularity stay obligations.",
    "DV: theorem consumers use dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, and theorem-specific finite-log-mgf witnesses; common space, absolute continuity, finite KL/log-likelihood, measurability, and finite log-mgf stay source-cited or obligations.",
    "LSI/KL/FI: theorem consumers use SALD.saldLsiKlFiDensityTestContract and cycle-43 density/entropy/Fisher-chain helpers; zero-set handling, admissible sqrt-density test or approximation, vector Fisher chain rule, and finite theorem-level KL/FI stay obligations.",
    "Continuous Fokker-Planck/KL derivative: forward-KL and continuous general moving-target consumers use SALD.forwardKlDerivativeSideConditionContract, SALD.generalMovingTargetDerivativeCandidateContract, and the cycle-50/52 scalar handoffs; density, boundary, integration-by-parts, transport, and schedule calculus stay obligations.",
    "Euler-Maruyama interpolation Fokker-Planck: discrete theorem consumers use SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, the cycle-48/53 endpoint-law handoffs, and SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff for the cycle-54 sigma-weighted divergence regrouping; conditional drift, density/absolute-continuity, weak FP, KL differentiation, and integration by parts stay obligations."
  ]
  theoremRoute := [
    "1. thm:forward-KL remains routed through continuous derivative, LSI, DV velocity, endpoint schedule, and Gronwall side conditions.",
    "2. thm:forward-KL-discrete remains routed through EM conditional-FP, frozen defect, LSI, DV velocity, stitched Gronwall, and accumulated-error interfaces.",
    "3. prop:guided_path_residual remains routed through normalizer differentiation, guided-density differentiation, divergence cancellation, and mean-zero residual obligations.",
    "4. thm:general-moving-target-SALD remains routed through continuous general derivative, residual LSI/DV, sigma-weighted Gronwall, endpoint/exponent, and pure-contraction obligations.",
    "5. thm:unified-forward-KL remains the source specialization of the continuous general theorem via guided residual and the correction-field transport bridge.",
    "6. thm:general-moving-target-SALD-discrete remains routed through general EM endpoint/conditional-FP, frozen delta, discrete KL derivative/LSI, residual DV, constant schedule, and Gronwall stitching."
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only original main_body.tex, appendix.tex, and iteration_complexity.tex; sald_version_2.tex remains excluded.",
    "Do not change theorem statements, constants, alpha ranges, sigma factors, source labels, or proof routes.",
    "Do not classify endpoint-law handoffs as Brownian construction, regular conditional drift, density, weak Fokker-Planck, or KL derivative proofs.",
    "Keep systematic SLT/SDE backfill deferred until theorem skeleton interfaces remain green."
  ]
  nonGoals := [
    "No new scalar-only lemma unless it directly discharges appendix.tex:1354-1387 endpoint or conditional-law obligations.",
    "No imported SLT or external theorem is promoted for DV, LSI, disintegration, concentration, or EM one-step analysis.",
    "No hidden endpoint, density, absolute-continuity, finite-KL/FI, finite-log-mgf, boundary, smoothness, conditional-law, or stitched-interval assumptions are added to a paper theorem.",
    "No alternate proof route replaces derivative -> LSI -> DV -> Gronwall or the paper EM/frozen-delta route."
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.",
    "First lower sub-slice remains appendix.tex:1354-1387 after the endpoint-law handoff: common probability space, hat rho_s and tilde pi_s density/absolute-continuity, regular conditional drift bar b_{k,s}, weak conditional Fokker-Planck equation, KL differentiation under the integral, and integration-by-parts side conditions.",
    "Use SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation only as pushforward endpoint-law bookkeeping from named interpolation identities.",
    "If conditional-FP is blocked, sharpen the source-cited interface by naming the common-space, absolute-continuity, finite-KL/FI, measurability, endpoint, conditional-law, and weak-FP hypotheses rather than modifying theorem statements."
  ]
  reviewerChecklist := [
    "SALD.cycle54MainSkeletonAnalyticMiddleObligation is listed by all six theorem contracts and in saldDependenciesForLabel through the cycle-54 dependency list.",
    "SALD.cycle54MainSkeletonAnalyticInterfaceDag contains ASTIS.SALD.cycle54.middle_interface_audit between the upper re-check and lower packet.",
    "The conversion window and proof-obligation ledger contain the cycle-54 middle audit and keep appendix.tex:1354-1387 as the lower target.",
    "Gronwall, DV, LSI/KL/FI, continuous derivative, EM conditional-FP, and theorem statements are not promoted beyond their current statuses.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  dependencies := [
    "SALD.cycle54MainSkeletonAnalyticInterfaceLedger",
    "SALD.cycle54MainSkeletonAnalyticInterfaceObligation",
    "SALD.cycle49MainSkeletonAnalyticMiddleObligation",
    "SALD.cycle50ForwardKlSkeletonMiddleObligation",
    "SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation",
    "SALD.cycle52GuidedGeneralSkeletonMiddleObligation",
    "SALD.cycle53UnifiedDiscreteGeneralMiddleObligation",
    "SALD.saldGronwallEndpointCalculusContract",
    "dvVariationalFormulaInterface saldDvVariationSource",
    "SALD.saldLsiKlFiDensityTestContract",
    "SALD.forwardKlDerivativeSideConditionContract",
    "SALD.generalMovingTargetDerivativeCandidateContract",
    "SALD.discreteForwardKlEmInterpolationSideConditionContract",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract",
    "SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff",
    "SALD.cycle54GeneralMovingTargetDiscreteEmFpLowerObligation",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.kl_derivative"
  ]
  status := ProofStatus.obligation

/-- Cycle-54 middle obligation tying the analytic-interface audit to the six
theorem contracts and the lower EM conditional-FP packet. -/