AutoSamplingTheory.SALD.cycle48UnifiedDiscreteSkeletonMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle48UnifiedDiscreteSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract

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.

guidedResidualSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

generalContinuousSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

unifiedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

discreteSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteSource — 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.

Middle source-to-Lean audit for main skeleton sprint 5: verify that thm:unified-forward-KL is only the paper specialization of thm:general-moving-target-SALD, and that thm:general-moving-target-SALD-discrete consumes the general EM endpoint/conditional-FP, frozen-delta, LSI, residual DV, and Gronwall interfaces in appendix.tex:1313-1603 without changing constants.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:359-368 uses prop:guided_path_residual and eq:poisson-eq to show that u_t+w_t transports pi_t.
2. main_body.tex:372-395 states thm:unified-forward-KL with the correction-field complexity E_alpha(pi_t,w_t) and the exact sigma_t^{-2} dot{s}(t)^{-1} coefficients.
3. appendix.tex:949-951 proves thm:unified-forward-KL by setting c_t <- u_t in thm:general-moving-target-SALD and identifying m_t=w_t.
4. appendix.tex:1313-1347 states thm:general-moving-target-SALD-discrete with the doubled residual coefficient, Gamma coefficient, Delta coefficient, alpha ranges, and constant inverse-schedule assumption.
5. appendix.tex:1354-1387 fixes k, defines hat rho_s, uses endpoint laws, defines the frozen conditional drift, invokes the general EM conditional Fokker-Planck equation, and starts the KL derivative identity.
6. appendix.tex:1389-1467 splits the Laplacian relative to tilde pi_s and combines the slowed target transport velocity with the conditional drift.
7. appendix.tex:1469-1511 rewrites the cross field as delta_pi^VA+dot t(s)*m_{t(s)} and applies the two sigma_eta^2/8 Young splits plus lem:frozen_delta_cross_lip.
8. appendix.tex:1513-1570 applies eq:LSI-KL-FI and lem:dv_variation to obtain the pre-Gronwall differential inequality.
9. appendix.tex:1573-1600 defines K(t), changes variables from s to t, uses dot t(s(t))=dot s(t)^{-1}, and applies lem:gronwall to match the theorem display.
10. appendix.tex:1603 records the discrete guided VA-SALD specialization c <- u.

leanStepMap : List String (explicit)

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

Ordered data items

1. Route main_body.tex:359-395 through SALD.unifiedForwardKlSpecializationContract, sald.unified_forward_kl.transport_bridge_middle, sald.unified_forward_kl.transport_bridge_lower, sald.unified_forward_kl.transport_velocity_bridge, and sald.unified_forward_kl.specialization.
2. Route appendix.tex:949-951 through SALD.generalMovingTargetStatementContract, SALD.generalVaSaldContract, and the continuous general derivative/DV/Gronwall obligations already checked in cycles 47 and 24.
3. Route appendix.tex:1313-1347 through SALD.generalMovingTargetDiscreteStatementContract and SALD.generalVaSaldDiscreteContract; the theorem remains contractOnly.
4. Route appendix.tex:1354-1387 through SALD.generalVaSaldEulerMaruyamaContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, sald.general_moving_target_discrete.em_interpolation_fp, and the cycle-48 EM endpoint/conditional-law audit.
5. Route appendix.tex:1469-1511 through SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector, SALD.generalMovingTargetDiscreteYoungFisherShareScalar, SALD.generalMovingTargetDiscreteTwoYoungFisherBudgetScalar, SALD.generalMovingTargetDiscreteResidualYoungCoefficientScalar, and sald.general_moving_target_discrete.derivative_side_conditions.
6. Route appendix.tex:1513-1570 through probability.lsi_to_kl_fi, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, sald.general_moving_target_discrete.dv_finite_log_mgf_witness, and sald.general_moving_target_discrete.dv_m_energy.
7. Route appendix.tex:1573-1600 through SALD.generalMovingTargetDiscreteGronwallInstantiationContract, SALD.generalMovingTargetDiscreteGronwallSideConditionContract, sald.general_moving_target_discrete.gronwall_application, sald.general_moving_target_discrete.constant_schedule_stitching, and sald.general_moving_target_discrete.gronwall_side_conditions.
8. Select the next lower target as sald.general_moving_target_discrete.kl_derivative, beginning with the appendix.tex:1354-1387 endpoint/conditional-law/Fokker-Planck interface.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains the endpoint-safe real-analysis obligation; the discrete theorem uses it only through sald.general_moving_target_discrete.gronwall_application and gronwall_side_conditions.
2. lem:dv_variation remains source-cited; the discrete residual witness must expose common-space, absolute-continuity, finite-KL, finite-log-mgf, and alpha scaling for the EM interpolation law.
3. eq:LSI-KL-FI remains the density-test/Fisher-chain obligation and is not promoted by the two sigma_eta^2/8 Young bookkeeping helpers.
4. The continuous general Fokker-Planck/KL derivative remains sald.general_moving_target.kl_derivative and is used upstream for the unified specialization.
5. The EM interpolation Fokker-Planck backend remains sald.general_moving_target_discrete.em_interpolation_fp with endpoint laws, conditional-law density, and regular conditional expectation side conditions explicit; the named-interpolation endpoint-law pair is compiled but is not the conditional-FP proof.
6. Local SLT material is reference-only for possible disintegration or one-step patterns; no SLT theorem is imported or marked formalized.

obligations : List String (explicit)

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

Ordered data items

1. sald.unified_discrete_general.cycle48_theorem_skeleton_route
2. sald.unified_discrete_general.cycle48_middle_route_audit
3. sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit
4. sald.unified_forward_kl.transport_velocity_bridge
5. sald.unified_forward_kl.specialization
6. sald.general_moving_target.kl_derivative
7. sald.general_moving_target.dv_finite_log_mgf_witness
8. sald.general_moving_target.gronwall_side_conditions
9. sald.general_moving_target_discrete.em_interpolation_fp
10. sald.general_moving_target_discrete.derivative_side_conditions
11. sald.general_moving_target_discrete.kl_derivative
12. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
13. sald.general_moving_target_discrete.dv_m_energy
14. sald.general_moving_target_discrete.gronwall_application
15. sald.general_moving_target_discrete.gronwall_side_conditions
16. sald.general_moving_target_discrete.unified_specialization

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: sharpen appendix.tex:1354-1387 into law-level endpoint equalities via SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, common-space and absolute-continuity assumptions for hat rho_s and tilde pi_s, conditional-law measurability/integrability for bar b_{k,s}, and the weak Fokker-Planck equation consumed by KL differentiation.
3. Second lower sub-slice: reuse the cycle-28 compiled frozen/residual algebra only after the conditional drift, score, slowed transport, and m_t=v_t-c_t identifications are supplied.
4. Do not restate the discrete theorem or add hypotheses to it; if a measure-theory fact is missing, refine sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit or sald.general_moving_target_discrete.derivative_side_conditions.
5. Treat local SLT one-step and disintegration material as reference-only until a theorem is ported and built locally.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The source-to-Lean map covers main_body.tex:359-395, appendix.tex:949-951, and appendix.tex:1313-1603 in paper order.
2. SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle48UnifiedDiscreteSkeletonMiddleObligation while remaining contractOnly.
3. SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag contain ASTIS.SALD.unified_discrete_general.cycle48_middle_route_audit.
4. SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-48 middle contract, obligation, and DAG route-audit node.
5. The EM endpoint/conditional-law audit remains an obligation; no conditional Fokker-Planck, regular conditional law, density, DV, LSI, or Gronwall backend is marked formalized.
6. No theorem statement, source label, source constant, or source-file scope changes.

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 cycle48UnifiedDiscreteSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Middle source-to-Lean audit for main skeleton sprint 5: verify that thm:unified-forward-KL is only the paper specialization of thm:general-moving-target-SALD, and that thm:general-moving-target-SALD-discrete consumes the general EM endpoint/conditional-FP, frozen-delta, LSI, residual DV, and Gronwall interfaces in appendix.tex:1313-1603 without changing constants."
  sourceStepMap := [
    "main_body.tex:359-368 uses prop:guided_path_residual and eq:poisson-eq to show that u_t+w_t transports pi_t.",
    "main_body.tex:372-395 states thm:unified-forward-KL with the correction-field complexity E_alpha(pi_t,w_t) and the exact sigma_t^{-2} dot{s}(t)^{-1} coefficients.",
    "appendix.tex:949-951 proves thm:unified-forward-KL by setting c_t <- u_t in thm:general-moving-target-SALD and identifying m_t=w_t.",
    "appendix.tex:1313-1347 states thm:general-moving-target-SALD-discrete with the doubled residual coefficient, Gamma coefficient, Delta coefficient, alpha ranges, and constant inverse-schedule assumption.",
    "appendix.tex:1354-1387 fixes k, defines hat rho_s, uses endpoint laws, defines the frozen conditional drift, invokes the general EM conditional Fokker-Planck equation, and starts the KL derivative identity.",
    "appendix.tex:1389-1467 splits the Laplacian relative to tilde pi_s and combines the slowed target transport velocity with the conditional drift.",
    "appendix.tex:1469-1511 rewrites the cross field as delta_pi^VA+dot t(s)*m_{t(s)} and applies the two sigma_eta^2/8 Young splits plus lem:frozen_delta_cross_lip.",
    "appendix.tex:1513-1570 applies eq:LSI-KL-FI and lem:dv_variation to obtain the pre-Gronwall differential inequality.",
    "appendix.tex:1573-1600 defines K(t), changes variables from s to t, uses dot t(s(t))=dot s(t)^{-1}, and applies lem:gronwall to match the theorem display.",
    "appendix.tex:1603 records the discrete guided VA-SALD specialization c <- u."
  ]
  leanStepMap := [
    "Route main_body.tex:359-395 through SALD.unifiedForwardKlSpecializationContract, sald.unified_forward_kl.transport_bridge_middle, sald.unified_forward_kl.transport_bridge_lower, sald.unified_forward_kl.transport_velocity_bridge, and sald.unified_forward_kl.specialization.",
    "Route appendix.tex:949-951 through SALD.generalMovingTargetStatementContract, SALD.generalVaSaldContract, and the continuous general derivative/DV/Gronwall obligations already checked in cycles 47 and 24.",
    "Route appendix.tex:1313-1347 through SALD.generalMovingTargetDiscreteStatementContract and SALD.generalVaSaldDiscreteContract; the theorem remains contractOnly.",
    "Route appendix.tex:1354-1387 through SALD.generalVaSaldEulerMaruyamaContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, sald.general_moving_target_discrete.em_interpolation_fp, and the cycle-48 EM endpoint/conditional-law audit.",
    "Route appendix.tex:1469-1511 through SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector, SALD.generalMovingTargetDiscreteYoungFisherShareScalar, SALD.generalMovingTargetDiscreteTwoYoungFisherBudgetScalar, SALD.generalMovingTargetDiscreteResidualYoungCoefficientScalar, and sald.general_moving_target_discrete.derivative_side_conditions.",
    "Route appendix.tex:1513-1570 through probability.lsi_to_kl_fi, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, sald.general_moving_target_discrete.dv_finite_log_mgf_witness, and sald.general_moving_target_discrete.dv_m_energy.",
    "Route appendix.tex:1573-1600 through SALD.generalMovingTargetDiscreteGronwallInstantiationContract, SALD.generalMovingTargetDiscreteGronwallSideConditionContract, sald.general_moving_target_discrete.gronwall_application, sald.general_moving_target_discrete.constant_schedule_stitching, and sald.general_moving_target_discrete.gronwall_side_conditions.",
    "Select the next lower target as sald.general_moving_target_discrete.kl_derivative, beginning with the appendix.tex:1354-1387 endpoint/conditional-law/Fokker-Planck interface."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains the endpoint-safe real-analysis obligation; the discrete theorem uses it only through sald.general_moving_target_discrete.gronwall_application and gronwall_side_conditions.",
    "lem:dv_variation remains source-cited; the discrete residual witness must expose common-space, absolute-continuity, finite-KL, finite-log-mgf, and alpha scaling for the EM interpolation law.",
    "eq:LSI-KL-FI remains the density-test/Fisher-chain obligation and is not promoted by the two sigma_eta^2/8 Young bookkeeping helpers.",
    "The continuous general Fokker-Planck/KL derivative remains sald.general_moving_target.kl_derivative and is used upstream for the unified specialization.",
    "The EM interpolation Fokker-Planck backend remains sald.general_moving_target_discrete.em_interpolation_fp with endpoint laws, conditional-law density, and regular conditional expectation side conditions explicit; the named-interpolation endpoint-law pair is compiled but is not the conditional-FP proof.",
    "Local SLT material is reference-only for possible disintegration or one-step patterns; no SLT theorem is imported or marked formalized."
  ]
  obligations := [
    "sald.unified_discrete_general.cycle48_theorem_skeleton_route",
    "sald.unified_discrete_general.cycle48_middle_route_audit",
    "sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit",
    "sald.unified_forward_kl.transport_velocity_bridge",
    "sald.unified_forward_kl.specialization",
    "sald.general_moving_target.kl_derivative",
    "sald.general_moving_target.dv_finite_log_mgf_witness",
    "sald.general_moving_target.gronwall_side_conditions",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.derivative_side_conditions",
    "sald.general_moving_target_discrete.kl_derivative",
    "sald.general_moving_target_discrete.dv_finite_log_mgf_witness",
    "sald.general_moving_target_discrete.dv_m_energy",
    "sald.general_moving_target_discrete.gronwall_application",
    "sald.general_moving_target_discrete.gronwall_side_conditions",
    "sald.general_moving_target_discrete.unified_specialization"
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.",
    "First lower sub-slice: sharpen appendix.tex:1354-1387 into law-level endpoint equalities via SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, common-space and absolute-continuity assumptions for hat rho_s and tilde pi_s, conditional-law measurability/integrability for bar b_{k,s}, and the weak Fokker-Planck equation consumed by KL differentiation.",
    "Second lower sub-slice: reuse the cycle-28 compiled frozen/residual algebra only after the conditional drift, score, slowed transport, and m_t=v_t-c_t identifications are supplied.",
    "Do not restate the discrete theorem or add hypotheses to it; if a measure-theory fact is missing, refine sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit or sald.general_moving_target_discrete.derivative_side_conditions.",
    "Treat local SLT one-step and disintegration material as reference-only until a theorem is ported and built locally."
  ]
  reviewerChecklist := [
    "The source-to-Lean map covers main_body.tex:359-395, appendix.tex:949-951, and appendix.tex:1313-1603 in paper order.",
    "SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle48UnifiedDiscreteSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag contain ASTIS.SALD.unified_discrete_general.cycle48_middle_route_audit.",
    "SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-48 middle contract, obligation, and DAG route-audit node.",
    "The EM endpoint/conditional-law audit remains an obligation; no conditional Fokker-Planck, regular conditional law, density, DV, LSI, or Gronwall backend is marked formalized.",
    "No theorem statement, source label, source constant, or source-file scope changes."
  ]
  status := ProofStatus.obligation

/-- Cycle-48 narrow measure-theory audit for the discrete general EM
endpoint and conditional-law Fokker--Planck backend. -/