AutoSamplingTheory.SALD.cycle64MainSkeletonAnalyticMiddleContract

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 cycle64MainSkeletonAnalyticMiddleContract :
    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 64 middle: audit the upper analytic-interface ledger against the source theorem route, verify that the five slow analytic interfaces are consumed by the six faithful theorem skeletons in paper order, and narrow lower work to sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387 after the cycle-63 endpoint-law Measure.map helpers.

sourceLabels : List String (explicit)

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

Ordered data items

1. lem:gronwall
2. lem:dv_variation
3. eq:LSI-KL-FI
4. proof:thm:forward-KL:derivative
5. proof:thm:forward-KL-discrete:conditional-fp
6. proof:thm:general-moving-target-SALD:derivative
7. proof:thm:general-moving-target-SALD-discrete:em-conditional-fp
8. eq:general_KL_derivative_0_discrete
9. eq:general_moving_target_SALD_frozen_interp
10. thm:forward-KL
11. thm:forward-KL-discrete
12. prop:guided_path_residual
13. thm:general-moving-target-SALD
14. thm:unified-forward-KL
15. thm:general-moving-target-SALD-discrete

analyticInterfaces : List String (explicit)

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

Ordered data items

1. Middle five-backend check, Gronwall: all theorem routes still consume SALD.saldGronwallEndpointCalculusContract and theorem-specific side-condition obligations; no endpoint-safe differentiability, FTC, coefficient-regularity, or display-matching fact is promoted.
2. Middle five-backend check, DV: all DV uses still pass through dvVariationalFormulaInterface saldDvVariationSource plus theorem-specific common-space, absolute-continuity, finite-KL, measurability, positive-alpha, and finite-log-mgf witnesses.
3. Middle five-backend check, LSI/KL/FI: all LSI uses still pass through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi with density, zero-set convention, admissible-test, entropy identity, finite KL/FI, and Fisher-chain assumptions explicit.
4. Middle five-backend check, continuous Fokker-Planck/KL derivative: thm:forward-KL and thm:general-moving-target-SALD consume the existing derivative candidate and side-condition interfaces; cycle-60 and cycle-62 scalar handoffs do not close the analytic backend.
5. Middle five-backend check, EM interpolation Fokker-Planck: discrete theorem routes consume SALD.discreteForwardKlEmInterpolationSideConditionContract and SALD.generalMovingTargetDiscreteDerivativeSideConditionContract; cycle-63 endpoint-law helpers prove only Measure.map bookkeeping, leaving conditional drift, density/AC, weak FP, KL differentiation, and stitching open.

theoremRoute : List String (explicit)

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

Ordered data items

1. 1. thm:forward-KL: appendix.tex:168-252 remains derivative/Fokker-Planck -> LSI/KL/FI -> DV -> Gronwall.
2. 2. thm:forward-KL-discrete: appendix.tex:260-592 remains EM conditional-FP -> KL derivative/frozen defect/LSI -> DV -> Gronwall -> accumulated errors.
3. 3. prop:guided_path_residual: appendix.tex:619-704 remains normalizer differentiation, residual identity, and mean-zero cancellation.
4. 4. thm:general-moving-target-SALD: appendix.tex:724-949 remains continuous general KL derivative -> residual LSI/DV -> sigma-weighted Gronwall.
5. 5. thm:unified-forward-KL: appendix.tex:949-951 remains only the c_t=u_t, m_t=w_t specialization through prop:guided_path_residual and thm:general-moving-target-SALD.
6. 6. thm:general-moving-target-SALD-discrete: appendix.tex:1313-1603 remains general EM endpoint/conditional-FP -> frozen delta -> KL derivative/LSI -> residual DV -> constant-schedule Gronwall/display stitching.

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1: this is source-to-Lean synchronization only, using the original main_body.tex, appendix.tex, and iteration_complexity.tex; sald_version_2.tex remains excluded.
2. The cycle-63 endpoint-law Measure.map helpers may be reused only as common-space endpoint bookkeeping; they do not supply conditional laws, densities, weak Fokker-Planck, KL differentiation, or Gronwall stitching.
3. All theorem contracts remain ProofStatus.contractOnly and all slow analytic interfaces remain ProofStatus.obligation or ProofStatus.sourceCited unless already compiled locally.
4. The selected lower packet is theorem-route useful and narrow: appendix.tex:1358-1387 for the general discrete EM conditional-law/Fokker-Planck backend.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not restate any theorem display, alter alpha ranges, sigma_eta factors, endpoint laws, Gamma/Delta terms, residual coefficients, or source labels.
2. Do not replace the source derivative -> LSI -> DV -> Gronwall proof route or the paper EM/frozen-delta route.
3. Do not begin broad SLT, disintegration, SDE, Gaussian concentration, entropy-duality, or reusable API backfill.
4. Do not mark conditional drift, density/absolute-continuity, weak Fokker-Planck, KL differentiation, DV, LSI/KL/FI, Gronwall, theorem contracts, or SLT reuse as formalized.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation / SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / sald.general_moving_target_discrete.em_interpolation_fp.
2. Source slice appendix.tex:1358-1366: expose endpoint-safe KL differentiation, mass conservation int partial_s hat rho_s dx=0, density and absolute-continuity requirements for hat rho_s and tilde pi_s, and finite KL on the interpolation interval.
3. Source slice appendix.tex:1368-1377: define the frozen conditional drift bar b_{k,s}(x) from the regular conditional law of X_k^eta given hat X_s=x, with measurability and integrability obligations for both drift summands; cycle 64 lower compiles only the abstract linear-combination algebra once conditional-expectation linearity is supplied.
4. Source slice appendix.tex:1379-1387: state the weak conditional Fokker-Planck equation for hat rho_s with drift term -div(hat rho_s bar b_{k,s}) and Laplacian +(sigma_eta^2/2) Delta hat rho_s, preserving the source signs.
5. Keep the Laplacian split after appendix.tex:1389, frozen-delta algebra, LSI, DV, and Gronwall as separate downstream obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.cycle64MainSkeletonAnalyticMiddleObligation is listed by all six theorem contracts while those contracts remain ProofStatus.contractOnly.
2. SALD.cycle64MainSkeletonAnalyticInterfaceDag contains ASTIS.SALD.cycle64.middle_interface_audit before the lower-packet node.
3. SALD.saldDependenciesForLabel includes SALD.cycle64MainSkeletonAnalyticMiddleContract, SALD.cycle64MainSkeletonAnalyticMiddleObligation, and sald.main_skeleton.cycle64_middle_interface_audit through cycle64MainSkeletonDependencyNames.
4. The conversion window and proof-obligation ledger record the source-to-Lean split for appendix.tex:1358-1387.
5. No theorem statement, source constant, source label, source-file scope, SLT reuse entry, or analytic backend status changes.
6. 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.cycle64MainSkeletonAnalyticInterfaceLedger
2. SALD.cycle64MainSkeletonAnalyticInterfaceObligation
3. SALD.cycle63UnifiedDiscreteGeneralMiddleObligation
4. SALD.cycle63UnifiedDiscreteGeneralMeasureBackfillObligation
5. SALD.cycle59MainSkeletonAnalyticMiddleObligation
6. SALD.saldGronwallEndpointCalculusContract
7. dvVariationalFormulaInterface saldDvVariationSource
8. SALD.saldLsiKlFiDensityTestContract
9. SALD.forwardKlDerivativeSideConditionContract
10. SALD.generalMovingTargetDerivativeCandidateContract
11. SALD.discreteForwardKlEmInterpolationSideConditionContract
12. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
13. SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation
14. SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation
15. SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation
16. SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation
17. SALD.generalMovingTargetDiscreteConditionalDriftContract
18. SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination
19. SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination
20. SALD.cycle64GeneralMovingTargetDiscreteConditionalDriftLowerObligation
21. sald.general_moving_target_discrete.em_interpolation_fp

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 cycle64MainSkeletonAnalyticMiddleContract :
    MainSkeletonAnalyticInterfaceLedger where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  objective := "Cycle 64 middle: audit the upper analytic-interface ledger against the source theorem route, verify that the five slow analytic interfaces are consumed by the six faithful theorem skeletons in paper order, and narrow lower work to sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387 after the cycle-63 endpoint-law Measure.map helpers."
  sourceLabels := [
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "proof:thm:forward-KL:derivative",
    "proof:thm:forward-KL-discrete:conditional-fp",
    "proof:thm:general-moving-target-SALD:derivative",
    "proof:thm:general-moving-target-SALD-discrete:em-conditional-fp",
    "eq:general_KL_derivative_0_discrete",
    "eq:general_moving_target_SALD_frozen_interp",
    "thm:forward-KL",
    "thm:forward-KL-discrete",
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete"
  ]
  analyticInterfaces := [
    "Middle five-backend check, Gronwall: all theorem routes still consume SALD.saldGronwallEndpointCalculusContract and theorem-specific side-condition obligations; no endpoint-safe differentiability, FTC, coefficient-regularity, or display-matching fact is promoted.",
    "Middle five-backend check, DV: all DV uses still pass through dvVariationalFormulaInterface saldDvVariationSource plus theorem-specific common-space, absolute-continuity, finite-KL, measurability, positive-alpha, and finite-log-mgf witnesses.",
    "Middle five-backend check, LSI/KL/FI: all LSI uses still pass through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi with density, zero-set convention, admissible-test, entropy identity, finite KL/FI, and Fisher-chain assumptions explicit.",
    "Middle five-backend check, continuous Fokker-Planck/KL derivative: thm:forward-KL and thm:general-moving-target-SALD consume the existing derivative candidate and side-condition interfaces; cycle-60 and cycle-62 scalar handoffs do not close the analytic backend.",
    "Middle five-backend check, EM interpolation Fokker-Planck: discrete theorem routes consume SALD.discreteForwardKlEmInterpolationSideConditionContract and SALD.generalMovingTargetDiscreteDerivativeSideConditionContract; cycle-63 endpoint-law helpers prove only Measure.map bookkeeping, leaving conditional drift, density/AC, weak FP, KL differentiation, and stitching open."
  ]
  theoremRoute := [
    "1. thm:forward-KL: appendix.tex:168-252 remains derivative/Fokker-Planck -> LSI/KL/FI -> DV -> Gronwall.",
    "2. thm:forward-KL-discrete: appendix.tex:260-592 remains EM conditional-FP -> KL derivative/frozen defect/LSI -> DV -> Gronwall -> accumulated errors.",
    "3. prop:guided_path_residual: appendix.tex:619-704 remains normalizer differentiation, residual identity, and mean-zero cancellation.",
    "4. thm:general-moving-target-SALD: appendix.tex:724-949 remains continuous general KL derivative -> residual LSI/DV -> sigma-weighted Gronwall.",
    "5. thm:unified-forward-KL: appendix.tex:949-951 remains only the c_t=u_t, m_t=w_t specialization through prop:guided_path_residual and thm:general-moving-target-SALD.",
    "6. thm:general-moving-target-SALD-discrete: appendix.tex:1313-1603 remains general EM endpoint/conditional-FP -> frozen delta -> KL derivative/LSI -> residual DV -> constant-schedule Gronwall/display stitching."
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: this is source-to-Lean synchronization only, using the original main_body.tex, appendix.tex, and iteration_complexity.tex; sald_version_2.tex remains excluded.",
    "The cycle-63 endpoint-law Measure.map helpers may be reused only as common-space endpoint bookkeeping; they do not supply conditional laws, densities, weak Fokker-Planck, KL differentiation, or Gronwall stitching.",
    "All theorem contracts remain ProofStatus.contractOnly and all slow analytic interfaces remain ProofStatus.obligation or ProofStatus.sourceCited unless already compiled locally.",
    "The selected lower packet is theorem-route useful and narrow: appendix.tex:1358-1387 for the general discrete EM conditional-law/Fokker-Planck backend."
  ]
  nonGoals := [
    "Do not restate any theorem display, alter alpha ranges, sigma_eta factors, endpoint laws, Gamma/Delta terms, residual coefficients, or source labels.",
    "Do not replace the source derivative -> LSI -> DV -> Gronwall proof route or the paper EM/frozen-delta route.",
    "Do not begin broad SLT, disintegration, SDE, Gaussian concentration, entropy-duality, or reusable API backfill.",
    "Do not mark conditional drift, density/absolute-continuity, weak Fokker-Planck, KL differentiation, DV, LSI/KL/FI, Gronwall, theorem contracts, or SLT reuse as formalized."
  ]
  lowerPacket := [
    "Target exactly SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation / SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / sald.general_moving_target_discrete.em_interpolation_fp.",
    "Source slice appendix.tex:1358-1366: expose endpoint-safe KL differentiation, mass conservation int partial_s hat rho_s dx=0, density and absolute-continuity requirements for hat rho_s and tilde pi_s, and finite KL on the interpolation interval.",
    "Source slice appendix.tex:1368-1377: define the frozen conditional drift bar b_{k,s}(x) from the regular conditional law of X_k^eta given hat X_s=x, with measurability and integrability obligations for both drift summands; cycle 64 lower compiles only the abstract linear-combination algebra once conditional-expectation linearity is supplied.",
    "Source slice appendix.tex:1379-1387: state the weak conditional Fokker-Planck equation for hat rho_s with drift term -div(hat rho_s bar b_{k,s}) and Laplacian +(sigma_eta^2/2) Delta hat rho_s, preserving the source signs.",
    "Keep the Laplacian split after appendix.tex:1389, frozen-delta algebra, LSI, DV, and Gronwall as separate downstream obligations."
  ]
  reviewerChecklist := [
    "SALD.cycle64MainSkeletonAnalyticMiddleObligation is listed by all six theorem contracts while those contracts remain ProofStatus.contractOnly.",
    "SALD.cycle64MainSkeletonAnalyticInterfaceDag contains ASTIS.SALD.cycle64.middle_interface_audit before the lower-packet node.",
    "SALD.saldDependenciesForLabel includes SALD.cycle64MainSkeletonAnalyticMiddleContract, SALD.cycle64MainSkeletonAnalyticMiddleObligation, and sald.main_skeleton.cycle64_middle_interface_audit through cycle64MainSkeletonDependencyNames.",
    "The conversion window and proof-obligation ledger record the source-to-Lean split for appendix.tex:1358-1387.",
    "No theorem statement, source constant, source label, source-file scope, SLT reuse entry, or analytic backend status changes.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  dependencies := [
    "SALD.cycle64MainSkeletonAnalyticInterfaceLedger",
    "SALD.cycle64MainSkeletonAnalyticInterfaceObligation",
    "SALD.cycle63UnifiedDiscreteGeneralMiddleObligation",
    "SALD.cycle63UnifiedDiscreteGeneralMeasureBackfillObligation",
    "SALD.cycle59MainSkeletonAnalyticMiddleObligation",
    "SALD.saldGronwallEndpointCalculusContract",
    "dvVariationalFormulaInterface saldDvVariationSource",
    "SALD.saldLsiKlFiDensityTestContract",
    "SALD.forwardKlDerivativeSideConditionContract",
    "SALD.generalMovingTargetDerivativeCandidateContract",
    "SALD.discreteForwardKlEmInterpolationSideConditionContract",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract",
    "SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation",
    "SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteConditionalDriftContract",
    "SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination",
    "SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination",
    "SALD.cycle64GeneralMovingTargetDiscreteConditionalDriftLowerObligation",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  status := ProofStatus.obligation

/-- Cycle-64 middle obligation tying the analytic-interface audit to the
selected EM conditional-law/Fokker--Planck lower packet. -/