AutoSamplingTheory.SALD.cycle53UnifiedDiscreteGeneralMiddleContract

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 cycle53UnifiedDiscreteGeneralMiddleContract :
    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.

Cycle 53 middle: audit the post-upper sprint-5 route in paper order, verify that thm:unified-forward-KL consumes the cycle-52 continuous general skeleton and correction-field specialization, verify that thm:general-moving-target-SALD-discrete consumes the EM endpoint/conditional-FP, frozen-delta, LSI, residual-DV, and Gronwall interfaces, and keep sald.general_moving_target_discrete.kl_derivative over appendix.tex:1354-1387 as the lower target.

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 turn u_t+w_t into a transport velocity for pi_t.
2. main_body.tex:372-395 states thm:unified-forward-KL with correction-field complexity E_alpha(pi_t,w_t) and the source sigma_t^{-2} dot{s}(t)^{-1} coefficients.
3. appendix.tex:949-951 proves thm:unified-forward-KL only by specializing thm:general-moving-target-SALD with c_t=u_t and 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, sigma_eta factors, and constant inverse-schedule assumption.
5. appendix.tex:1354-1387 defines hat rho_s, records endpoint laws, defines the frozen conditional drift, invokes the general EM conditional Fokker-Planck equation, and begins KL differentiation.
6. appendix.tex:1389-1511 performs the Laplacian split, frozen/residual field identification, and two sigma_eta^2/8 Young splits before the frozen-delta bound.
7. appendix.tex:1513-1552 applies eq:LSI-KL-FI and lem:dv_variation to the residual m_t on the EM interpolation law.
8. appendix.tex:1573-1600 changes variables to K(t), uses the constant schedule, and applies lem:gronwall to match the theorem display.
9. appendix.tex:1603 records the discrete guided VA-SALD specialization c_t=u_t.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle53UnifiedDiscreteGeneralUpperPacket and SALD.cycle53UnifiedDiscreteGeneralSkeletonObligation as parent route data; do not replace the cycle-52 continuous general theorem route.
2. Route unified VA-SALD through SALD.unifiedForwardKlSpecializationContract, sald.unified_forward_kl.transport_velocity_bridge, sald.unified_forward_kl.specialization, SALD.generalVaSaldContract, and the cycle-52 guided/general middle and lower obligations.
3. Route appendix.tex:1313-1347 through SALD.generalMovingTargetDiscreteStatementContract and SALD.generalVaSaldDiscreteContract; both remain contractOnly.
4. Route appendix.tex:1354-1387 through SALD.generalVaSaldEulerMaruyamaContract, SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation, SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation, and sald.general_moving_target_discrete.em_interpolation_fp.
5. Route appendix.tex:1469-1511 through SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector, the three cycle-28 Young/Fisher scalar bookkeeping helpers, and sald.general_moving_target_discrete.derivative_side_conditions.
6. Route appendix.tex:1513-1552 through SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, dvVariationalFormulaInterface saldDvVariationSource, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, 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, and sald.general_moving_target_discrete.gronwall_side_conditions.
8. Keep the lower packet at SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative, with the first sub-slice still the common-space, density/AC, regular conditional drift, weak conditional-FP, and KL differentiation backend.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains an endpoint-safe differentiability, FTC, coefficient-regularity, stitching, and display-matching obligation.
2. lem:dv_variation remains source-cited through common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and alpha-scaling witnesses.
3. eq:LSI-KL-FI remains the density, zero-set, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher-chain obligation.
4. The continuous Fokker-Planck/KL derivative is consumed upstream through sald.general_moving_target.kl_derivative and the cycle-52 scalar derivative/DV handoff, not reproved for the unified theorem.
5. The EM interpolation backend remains sald.general_moving_target_discrete.em_interpolation_fp: the cycle-53 Measure.map lemma proves only an endpoint-law congruence after named endpoint identities are supplied.

obligations : List String (explicit)

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

Ordered data items

1. sald.unified_discrete_general.cycle53_upper_route
2. sald.unified_discrete_general.cycle53_middle_route_audit
3. sald.guided_general.cycle52_middle_route_audit
4. sald.general_moving_target.cycle52_derivative_dv_lower
5. sald.unified_forward_kl.transport_velocity_bridge
6. sald.unified_forward_kl.specialization
7. sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit
8. sald.general_moving_target_discrete.em_interpolation_fp
9. sald.general_moving_target_discrete.derivative_side_conditions
10. sald.general_moving_target_discrete.kl_derivative
11. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
12. sald.general_moving_target_discrete.dv_m_energy
13. sald.general_moving_target_discrete.gronwall_application
14. sald.general_moving_target_discrete.gronwall_side_conditions

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: appendix.tex:1354-1387, after the compiled Measure.map endpoint-law handoff, expose the 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. Second lower sub-slice: appendix.tex:1389-1467, Laplacian split relative to tilde pi_s and slowed target transport equation.
4. Third lower sub-slice: appendix.tex:1469-1511, reuse the cycle-28 frozen/residual algebra only after the conditional drift, score, slowed transport, and m_t=v_t-c_t identifications are supplied.
5. Do not restate either theorem, change constants, or promote the Measure.map endpoint backfill into conditional drift, density, Fokker-Planck, or KL derivative formalization.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle53UnifiedDiscreteGeneralMiddleObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag include ASTIS.SALD.unified_discrete_general.cycle53_middle_route_audit.
3. SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-53 middle contract, middle obligation, and sald.unified_discrete_general.cycle53_middle_route_audit.
4. Only AutoSamplingTheory.lawMapEqOfAEEq and SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation are formalized in this cycle; analytic backends remain sourceCited or obligation-level.
5. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

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 cycle53UnifiedDiscreteGeneralMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Cycle 53 middle: audit the post-upper sprint-5 route in paper order, verify that thm:unified-forward-KL consumes the cycle-52 continuous general skeleton and correction-field specialization, verify that thm:general-moving-target-SALD-discrete consumes the EM endpoint/conditional-FP, frozen-delta, LSI, residual-DV, and Gronwall interfaces, and keep sald.general_moving_target_discrete.kl_derivative over appendix.tex:1354-1387 as the lower target."
  sourceStepMap := [
    "main_body.tex:359-368 uses prop:guided_path_residual and eq:poisson-eq to turn u_t+w_t into a transport velocity for pi_t.",
    "main_body.tex:372-395 states thm:unified-forward-KL with correction-field complexity E_alpha(pi_t,w_t) and the source sigma_t^{-2} dot{s}(t)^{-1} coefficients.",
    "appendix.tex:949-951 proves thm:unified-forward-KL only by specializing thm:general-moving-target-SALD with c_t=u_t and 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, sigma_eta factors, and constant inverse-schedule assumption.",
    "appendix.tex:1354-1387 defines hat rho_s, records endpoint laws, defines the frozen conditional drift, invokes the general EM conditional Fokker-Planck equation, and begins KL differentiation.",
    "appendix.tex:1389-1511 performs the Laplacian split, frozen/residual field identification, and two sigma_eta^2/8 Young splits before the frozen-delta bound.",
    "appendix.tex:1513-1552 applies eq:LSI-KL-FI and lem:dv_variation to the residual m_t on the EM interpolation law.",
    "appendix.tex:1573-1600 changes variables to K(t), uses the constant schedule, and applies lem:gronwall to match the theorem display.",
    "appendix.tex:1603 records the discrete guided VA-SALD specialization c_t=u_t."
  ]
  leanStepMap := [
    "Use SALD.cycle53UnifiedDiscreteGeneralUpperPacket and SALD.cycle53UnifiedDiscreteGeneralSkeletonObligation as parent route data; do not replace the cycle-52 continuous general theorem route.",
    "Route unified VA-SALD through SALD.unifiedForwardKlSpecializationContract, sald.unified_forward_kl.transport_velocity_bridge, sald.unified_forward_kl.specialization, SALD.generalVaSaldContract, and the cycle-52 guided/general middle and lower obligations.",
    "Route appendix.tex:1313-1347 through SALD.generalMovingTargetDiscreteStatementContract and SALD.generalVaSaldDiscreteContract; both remain contractOnly.",
    "Route appendix.tex:1354-1387 through SALD.generalVaSaldEulerMaruyamaContract, SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation, SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation, and sald.general_moving_target_discrete.em_interpolation_fp.",
    "Route appendix.tex:1469-1511 through SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector, the three cycle-28 Young/Fisher scalar bookkeeping helpers, and sald.general_moving_target_discrete.derivative_side_conditions.",
    "Route appendix.tex:1513-1552 through SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, dvVariationalFormulaInterface saldDvVariationSource, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, 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, and sald.general_moving_target_discrete.gronwall_side_conditions.",
    "Keep the lower packet at SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative, with the first sub-slice still the common-space, density/AC, regular conditional drift, weak conditional-FP, and KL differentiation backend."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains an endpoint-safe differentiability, FTC, coefficient-regularity, stitching, and display-matching obligation.",
    "lem:dv_variation remains source-cited through common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and alpha-scaling witnesses.",
    "eq:LSI-KL-FI remains the density, zero-set, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher-chain obligation.",
    "The continuous Fokker-Planck/KL derivative is consumed upstream through sald.general_moving_target.kl_derivative and the cycle-52 scalar derivative/DV handoff, not reproved for the unified theorem.",
    "The EM interpolation backend remains sald.general_moving_target_discrete.em_interpolation_fp: the cycle-53 Measure.map lemma proves only an endpoint-law congruence after named endpoint identities are supplied."
  ]
  obligations := [
    "sald.unified_discrete_general.cycle53_upper_route",
    "sald.unified_discrete_general.cycle53_middle_route_audit",
    "sald.guided_general.cycle52_middle_route_audit",
    "sald.general_moving_target.cycle52_derivative_dv_lower",
    "sald.unified_forward_kl.transport_velocity_bridge",
    "sald.unified_forward_kl.specialization",
    "sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit",
    "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"
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.",
    "First lower sub-slice: appendix.tex:1354-1387, after the compiled Measure.map endpoint-law handoff, expose the 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.",
    "Second lower sub-slice: appendix.tex:1389-1467, Laplacian split relative to tilde pi_s and slowed target transport equation.",
    "Third lower sub-slice: appendix.tex:1469-1511, reuse the cycle-28 frozen/residual algebra only after the conditional drift, score, slowed transport, and m_t=v_t-c_t identifications are supplied.",
    "Do not restate either theorem, change constants, or promote the Measure.map endpoint backfill into conditional drift, density, Fokker-Planck, or KL derivative formalization."
  ]
  reviewerChecklist := [
    "SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle53UnifiedDiscreteGeneralMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag include ASTIS.SALD.unified_discrete_general.cycle53_middle_route_audit.",
    "SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-53 middle contract, middle obligation, and sald.unified_discrete_general.cycle53_middle_route_audit.",
    "Only AutoSamplingTheory.lawMapEqOfAEEq and SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation are formalized in this cycle; analytic backends remain sourceCited or obligation-level.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-53 middle obligation tying the final route audit to lower work. -/