AutoSamplingTheory.SALD.cycle51DiscreteForwardKlSkeletonMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle51DiscreteForwardKlSkeletonMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract

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.

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

interpolationSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

accumulatedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteAccumulatedErrorSource — 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 51 middle: synchronize the post-cycle-50 thm:forward-KL-discrete route after SALD.cycle51DiscreteForwardKlSkeletonObligation, verify main_body.tex:299-323 and appendix.tex:260-592 in source order, and select sald.discrete_forward_kl.kl_derivative over appendix.tex:334-491 as the next lower backend while consuming EM endpoint/conditional-FP interfaces as source-cited obligations.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:299-323 fixes linear slowdown t(s)=s/r, reuses thm:forward-KL assumptions, adds score Lipschitz and alpha0' complexity hypotheses, assumes 4*eta^2*L_space^2<1/2, and states the exact barGamma/barDelta terminal KL bound.
2. appendix.tex:260-330 defines the frozen EM interpolation and the SALD frozen score-defect lemma; the lemma is still an obligation via the later general frozen-delta result specialized with c=0 and sigma_eta(t)=sqrt(2).
3. appendix.tex:334-385 supplies the inputs to the derivative backend: endpoint laws for hat rho, the conditional frozen drift bar b_{k,s}, the conditional-drift Fokker-Planck equation, and the Laplacian split relative to tilde pi_s.
4. appendix.tex:388-452 differentiates KL(hat rho_s||tilde pi_s), evaluates the EM Fokker-Planck contribution by integration by parts, and imports the target transport term from the continuous route.
5. appendix.tex:454-491 inserts the frozen-cross estimate, the moving Young bound, and eq:LSI-KL-FI to obtain the s-time pre-DV inequality.
6. appendix.tex:493-523 remains the separate DV velocity witness for nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2.
7. appendix.tex:526-592 remains the separate time-change, Gronwall, and accumulated-error bridge to the main-body display.

leanStepMap : List String (explicit)

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

Ordered data items

1. Keep SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract unchanged; this middle record only audits the route.
2. Use SALD.cycle49MainSkeletonAnalyticReadinessObligation, SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation, and SALD.cycle51DiscreteForwardKlSkeletonObligation as parent route checks.
3. Consume appendix.tex:334-385 through SALD.discreteForwardKlEmInterpolationSideConditionContract, sald.discrete_forward_kl.em_endpoint_laws, sald.discrete_forward_kl.conditional_drift_density, sald.discrete_forward_kl.em_conditional_fokker_planck, and sald.discrete_forward_kl.em_interpolation_fp.
4. Route appendix.tex:388-491 through SALD.discreteForwardKlDerivativeCandidateContract, SALD.discreteForwardKlDerivativeObligation, SALD.frozenDeltaCrossLipSaldContract, and SALD.saldLsiKlFiDensityTestContract.
5. Keep appendix.tex:493-523 on SALD.discreteForwardKlDvFiniteLogMgfWitnessContract and sald.discrete_forward_kl.dv_velocity_bound rather than folding DV into the derivative backend.
6. Keep appendix.tex:526-592 on SALD.discreteForwardKlGronwallInstantiationContract and SALD.discreteForwardKlAccumulatedErrorBridgeContract.
7. Select lower work on sald.discrete_forward_kl.kl_derivative, first using the existing EM endpoint/conditional-FP interfaces as hypotheses instead of reproving them.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. EM endpoint and conditional-Fokker-Planck backends are consumed as source-cited obligation interfaces; no Brownian-law, disintegration, or weak-FP theorem is promoted.
2. eq:LSI-KL-FI remains the density-test, entropy, zero-set, and Fisher-chain obligation used to replace one half-FI by C_LSI*K.
3. lem:dv_variation remains source-cited and is used only through the separate discrete DV finite-log-mgf witness after the derivative backend.
4. lem:gronwall remains the endpoint-safe real-analysis obligation with stitched-interval regularity and coefficient integrability.
5. The cycle-50 continuous scalar handoff is reusable coefficient data only and does not close the discrete KL derivative.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle51_theorem_interface_route
2. sald.discrete_forward_kl.cycle51_middle_route_audit
3. sald.discrete_forward_kl.em_endpoint_laws
4. sald.discrete_forward_kl.conditional_drift_density
5. sald.discrete_forward_kl.em_conditional_fokker_planck
6. sald.discrete_forward_kl.em_interpolation_fp
7. sald.discrete_forward_kl.frozen_delta_cross_lip
8. sald.discrete_forward_kl.kl_derivative
9. probability.lsi_to_kl_fi
10. sald.discrete_forward_kl.dv_finite_log_mgf_witness
11. sald.discrete_forward_kl.dv_velocity_bound
12. sald.discrete_forward_kl.gronwall_accumulation
13. sald.discrete_forward_kl.accumulated_error_bridge

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.discreteForwardKlDerivativeCandidateContract / SALD.discreteForwardKlDerivativeObligation / sald.discrete_forward_kl.kl_derivative.
2. First lower sub-slice: appendix.tex:334-385 as inputs, namely endpoint laws, conditional drift density, conditional-Fokker-Planck equation, and Laplacian split; do not prove the EM Fokker-Planck theorem from scratch.
3. Second lower sub-slice: appendix.tex:388-491, using the supplied EM-FP interface to derive the KL derivative identity, frozen-cross contribution, moving Young share, and LSI handoff.
4. Leave appendix.tex:493-523 DV, appendix.tex:526-592 Gronwall, endpoint stitching, residual exponent, and barGamma/barDelta collection in their existing obligations.
5. If a backend is missing, sharpen the named EM, density, absolute-continuity, boundary, or stitched-interval obligation instead of changing thm:forward-KL-discrete.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract lists SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle51_middle_route_audit after the cycle51 theorem-interface route.
3. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle51DiscreteForwardKlSkeletonMiddleContract, SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle51_middle_route_audit.
4. No EM/Fokker-Planck, KL derivative, LSI, DV, Gronwall, or accumulated-error backend is promoted to formalized status.
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 cycle51DiscreteForwardKlSkeletonMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Cycle 51 middle: synchronize the post-cycle-50 thm:forward-KL-discrete route after SALD.cycle51DiscreteForwardKlSkeletonObligation, verify main_body.tex:299-323 and appendix.tex:260-592 in source order, and select sald.discrete_forward_kl.kl_derivative over appendix.tex:334-491 as the next lower backend while consuming EM endpoint/conditional-FP interfaces as source-cited obligations."
  sourceStepMap := [
    "main_body.tex:299-323 fixes linear slowdown t(s)=s/r, reuses thm:forward-KL assumptions, adds score Lipschitz and alpha0' complexity hypotheses, assumes 4*eta^2*L_space^2<1/2, and states the exact barGamma/barDelta terminal KL bound.",
    "appendix.tex:260-330 defines the frozen EM interpolation and the SALD frozen score-defect lemma; the lemma is still an obligation via the later general frozen-delta result specialized with c=0 and sigma_eta(t)=sqrt(2).",
    "appendix.tex:334-385 supplies the inputs to the derivative backend: endpoint laws for hat rho, the conditional frozen drift bar b_{k,s}, the conditional-drift Fokker-Planck equation, and the Laplacian split relative to tilde pi_s.",
    "appendix.tex:388-452 differentiates KL(hat rho_s||tilde pi_s), evaluates the EM Fokker-Planck contribution by integration by parts, and imports the target transport term from the continuous route.",
    "appendix.tex:454-491 inserts the frozen-cross estimate, the moving Young bound, and eq:LSI-KL-FI to obtain the s-time pre-DV inequality.",
    "appendix.tex:493-523 remains the separate DV velocity witness for nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2.",
    "appendix.tex:526-592 remains the separate time-change, Gronwall, and accumulated-error bridge to the main-body display."
  ]
  leanStepMap := [
    "Keep SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract unchanged; this middle record only audits the route.",
    "Use SALD.cycle49MainSkeletonAnalyticReadinessObligation, SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation, and SALD.cycle51DiscreteForwardKlSkeletonObligation as parent route checks.",
    "Consume appendix.tex:334-385 through SALD.discreteForwardKlEmInterpolationSideConditionContract, sald.discrete_forward_kl.em_endpoint_laws, sald.discrete_forward_kl.conditional_drift_density, sald.discrete_forward_kl.em_conditional_fokker_planck, and sald.discrete_forward_kl.em_interpolation_fp.",
    "Route appendix.tex:388-491 through SALD.discreteForwardKlDerivativeCandidateContract, SALD.discreteForwardKlDerivativeObligation, SALD.frozenDeltaCrossLipSaldContract, and SALD.saldLsiKlFiDensityTestContract.",
    "Keep appendix.tex:493-523 on SALD.discreteForwardKlDvFiniteLogMgfWitnessContract and sald.discrete_forward_kl.dv_velocity_bound rather than folding DV into the derivative backend.",
    "Keep appendix.tex:526-592 on SALD.discreteForwardKlGronwallInstantiationContract and SALD.discreteForwardKlAccumulatedErrorBridgeContract.",
    "Select lower work on sald.discrete_forward_kl.kl_derivative, first using the existing EM endpoint/conditional-FP interfaces as hypotheses instead of reproving them."
  ]
  citedResultInterfaces := [
    "EM endpoint and conditional-Fokker-Planck backends are consumed as source-cited obligation interfaces; no Brownian-law, disintegration, or weak-FP theorem is promoted.",
    "eq:LSI-KL-FI remains the density-test, entropy, zero-set, and Fisher-chain obligation used to replace one half-FI by C_LSI*K.",
    "lem:dv_variation remains source-cited and is used only through the separate discrete DV finite-log-mgf witness after the derivative backend.",
    "lem:gronwall remains the endpoint-safe real-analysis obligation with stitched-interval regularity and coefficient integrability.",
    "The cycle-50 continuous scalar handoff is reusable coefficient data only and does not close the discrete KL derivative."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle51_theorem_interface_route",
    "sald.discrete_forward_kl.cycle51_middle_route_audit",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.conditional_drift_density",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "sald.discrete_forward_kl.em_interpolation_fp",
    "sald.discrete_forward_kl.frozen_delta_cross_lip",
    "sald.discrete_forward_kl.kl_derivative",
    "probability.lsi_to_kl_fi",
    "sald.discrete_forward_kl.dv_finite_log_mgf_witness",
    "sald.discrete_forward_kl.dv_velocity_bound",
    "sald.discrete_forward_kl.gronwall_accumulation",
    "sald.discrete_forward_kl.accumulated_error_bridge"
  ]
  lowerPacket := [
    "Target exactly SALD.discreteForwardKlDerivativeCandidateContract / SALD.discreteForwardKlDerivativeObligation / sald.discrete_forward_kl.kl_derivative.",
    "First lower sub-slice: appendix.tex:334-385 as inputs, namely endpoint laws, conditional drift density, conditional-Fokker-Planck equation, and Laplacian split; do not prove the EM Fokker-Planck theorem from scratch.",
    "Second lower sub-slice: appendix.tex:388-491, using the supplied EM-FP interface to derive the KL derivative identity, frozen-cross contribution, moving Young share, and LSI handoff.",
    "Leave appendix.tex:493-523 DV, appendix.tex:526-592 Gronwall, endpoint stitching, residual exponent, and barGamma/barDelta collection in their existing obligations.",
    "If a backend is missing, sharpen the named EM, density, absolute-continuity, boundary, or stitched-interval obligation instead of changing thm:forward-KL-discrete."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract lists SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle51_middle_route_audit after the cycle51 theorem-interface route.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle51DiscreteForwardKlSkeletonMiddleContract, SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle51_middle_route_audit.",
    "No EM/Fokker-Planck, KL derivative, LSI, DV, Gronwall, or accumulated-error backend is promoted to formalized status.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-51 middle obligation tying the discrete route audit to the derivative lower packet. -/