AutoSamplingTheory.SALD.cycle46DiscreteForwardKlSkeletonMiddleContract

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

Middle source-to-Lean audit for main skeleton sprint 3: verify that cycle46DiscreteForwardKlSkeletonObligation consumes the EM endpoint/conditional-FP, frozen-defect plus LSI, DV velocity, Gronwall, and accumulated-error interfaces in the exact appendix.tex:260-592 order, while main_body.tex:299-323 remains the unchanged theorem statement.

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 the linear slowdown theorem: t(s)=s/r with r>=1, the Theorem thm:forward-KL assumptions, Lipschitz conditions, alpha0' finite score and 1+M complexities, 4*eta^2*L_space^2<1/2, alpha in (0,alpha0), alpha' in (0,alpha0'], and the displayed barGamma/barDelta bound.
2. appendix.tex:260-330 introduces the frozen EM interpolation, frozen field delta_pi_t, and the SALD frozen-defect lemma obtained from the later general lemma with c=0 and sigma_eta(t)=sqrt(2).
3. appendix.tex:334-385 fixes k and s in [s_k,s_{k+1}], identifies the endpoint laws, defines bar b_{k,s}, and uses the EM conditional Fokker-Planck equation plus the Laplacian split.
4. appendix.tex:388-491 differentiates KL(hat rho_s||tilde pi_s), evaluates the first and target-velocity terms, inserts the frozen cross bound and the moving Young bound, then applies eq:LSI-KL-FI to get the pre-DV s-time inequality.
5. appendix.tex:493-523 applies lem:dv_variation under the EM interpolation law with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2, preserving the dot t(s)^2 and alpha^(-1) coefficients.
6. appendix.tex:526-553 changes from s to t and obtains the source coefficient dot s(t)*C_LSI(t)-dot s(t)^(-1)*alpha^(-1)-2*dot s(t)*eta^2*alpha'^(-1)*Gamma(t).
7. appendix.tex:557-592 applies lem:gronwall to the general-schedule bound; main_body.tex:309-323 then specializes t(s)=s/r and collects A_alpha(pi,v), barGamma, and barDelta_alpha'.

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; the middle contract only audits the route wrapper.
2. Use SALD.cycle44MainSkeletonAnalyticInterfaceLedger and SALD.cycle46DiscreteForwardKlSkeletonObligation as the parent theorem-skeleton interfaces.
3. Route appendix.tex:260-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:268-330 and 454-491 through SALD.frozenDeltaCrossLipSaldContract, sald.discrete_forward_kl.frozen_delta_cross_lip, SALD.discreteForwardKlDerivativeCandidateContract, and sald.discrete_forward_kl.kl_derivative.
5. Route the LSI step through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; density-test, zero-set, admissibility, entropy, and Fisher-chain backends remain obligations.
6. Route appendix.tex:493-523 through SALD.discreteForwardKlDvFiniteLogMgfWitnessContract, sald.discrete_forward_kl.dv_finite_log_mgf_witness, and sald.discrete_forward_kl.dv_velocity_bound; DV remains source-cited.
7. Route appendix.tex:526-592 through SALD.discreteForwardKlGronwallInstantiationContract, sald.discrete_forward_kl.gronwall_accumulation, SALD.discreteForwardKlAccumulatedErrorBridgeContract, sald.discrete_forward_kl.linear_slowdown_specialization, sald.discrete_forward_kl.residual_exponent_bound, and sald.discrete_forward_kl.accumulated_error_bridge.
8. Select the next lower target as sald.discrete_forward_kl.accumulated_error_bridge, because the theorem-level route is wired and the remaining statement-display risk is the linear-slowdown collection of A_alpha, barGamma, and barDelta.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:dv_variation remains source-cited through the common-space and finite-log-mgf interface; no entropy-duality theorem is imported or marked formalized.
2. lem:gronwall remains the endpoint-safe real-analysis obligation with stitched-interval regularity, coefficient regularity, endpoint rewrites, and exponent side conditions.
3. eq:LSI-KL-FI remains the density-test and Fisher-chain obligation; compiled scalar and RN-density helpers are dependencies only.
4. The continuous forward-KL derivative/Fokker-Planck route remains a reusable obligation for the target transport term; it is not promoted by this discrete middle audit.
5. The EM interpolation endpoint and conditional-law Fokker-Planck backend remains the discrete slow backend; endpoint vector/law algebra is only a local handoff.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle46_theorem_skeleton_route
2. sald.discrete_forward_kl.cycle46_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.linear_slowdown_specialization
14. sald.discrete_forward_kl.residual_exponent_bound
15. sald.discrete_forward_kl.accumulated_error_bridge
16. sald.discrete_forward_kl.coefficient_chain_audit

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.
2. First lower sub-slice: expose the endpointBridge and initialExponentSplit for K(0)=KL(rho_0||pi_0), K(T)=KL(rho_K^eta||pi_T), and the two source exponent factors after t(s)=s/r.
3. Cycle 46 lower compiled the initial-exponent scalar/integral split as SALD.discreteForwardKlGronwallCoeffIntervalIntegrable, SALD.discreteForwardKlGronwallCoeffIntegralSubSub, SALD.discreteForwardKlGronwallInitialExponentSplitScalar, and SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces.
4. Second lower sub-slice: connect the already compiled collection algebra SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, and SALD.discreteForwardKlAccumulatedErrorCollectionScalar to the theorem display, without changing constants.
5. Leave residual-exponent monotonicity, barGamma identification, stitched-interval Gronwall, EM conditional-FP, frozen-defect specialization, DV finite-log-mgf, and LSI/KL/FI as obligations unless exact compiled proofs are added.
6. Do not work on the general VA-SALD discrete theorem in this lower packet; this cycle stabilizes thm:forward-KL-discrete first.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract lists SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle46_middle_route_audit after the theorem skeleton route and before lower EM, defect, DV, and Gronwall nodes.
3. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle46DiscreteForwardKlSkeletonMiddleContract, SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle46_middle_route_audit.
4. No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.
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 cycle46DiscreteForwardKlSkeletonMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Middle source-to-Lean audit for main skeleton sprint 3: verify that cycle46DiscreteForwardKlSkeletonObligation consumes the EM endpoint/conditional-FP, frozen-defect plus LSI, DV velocity, Gronwall, and accumulated-error interfaces in the exact appendix.tex:260-592 order, while main_body.tex:299-323 remains the unchanged theorem statement."
  sourceStepMap := [
    "main_body.tex:299-323 fixes the linear slowdown theorem: t(s)=s/r with r>=1, the Theorem thm:forward-KL assumptions, Lipschitz conditions, alpha0' finite score and 1+M complexities, 4*eta^2*L_space^2<1/2, alpha in (0,alpha0), alpha' in (0,alpha0'], and the displayed barGamma/barDelta bound.",
    "appendix.tex:260-330 introduces the frozen EM interpolation, frozen field delta_pi_t, and the SALD frozen-defect lemma obtained from the later general lemma with c=0 and sigma_eta(t)=sqrt(2).",
    "appendix.tex:334-385 fixes k and s in [s_k,s_{k+1}], identifies the endpoint laws, defines bar b_{k,s}, and uses the EM conditional Fokker-Planck equation plus the Laplacian split.",
    "appendix.tex:388-491 differentiates KL(hat rho_s||tilde pi_s), evaluates the first and target-velocity terms, inserts the frozen cross bound and the moving Young bound, then applies eq:LSI-KL-FI to get the pre-DV s-time inequality.",
    "appendix.tex:493-523 applies lem:dv_variation under the EM interpolation law with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2, preserving the dot t(s)^2 and alpha^(-1) coefficients.",
    "appendix.tex:526-553 changes from s to t and obtains the source coefficient dot s(t)*C_LSI(t)-dot s(t)^(-1)*alpha^(-1)-2*dot s(t)*eta^2*alpha'^(-1)*Gamma(t).",
    "appendix.tex:557-592 applies lem:gronwall to the general-schedule bound; main_body.tex:309-323 then specializes t(s)=s/r and collects A_alpha(pi,v), barGamma, and barDelta_alpha'."
  ]
  leanStepMap := [
    "Keep SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract unchanged; the middle contract only audits the route wrapper.",
    "Use SALD.cycle44MainSkeletonAnalyticInterfaceLedger and SALD.cycle46DiscreteForwardKlSkeletonObligation as the parent theorem-skeleton interfaces.",
    "Route appendix.tex:260-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:268-330 and 454-491 through SALD.frozenDeltaCrossLipSaldContract, sald.discrete_forward_kl.frozen_delta_cross_lip, SALD.discreteForwardKlDerivativeCandidateContract, and sald.discrete_forward_kl.kl_derivative.",
    "Route the LSI step through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; density-test, zero-set, admissibility, entropy, and Fisher-chain backends remain obligations.",
    "Route appendix.tex:493-523 through SALD.discreteForwardKlDvFiniteLogMgfWitnessContract, sald.discrete_forward_kl.dv_finite_log_mgf_witness, and sald.discrete_forward_kl.dv_velocity_bound; DV remains source-cited.",
    "Route appendix.tex:526-592 through SALD.discreteForwardKlGronwallInstantiationContract, sald.discrete_forward_kl.gronwall_accumulation, SALD.discreteForwardKlAccumulatedErrorBridgeContract, sald.discrete_forward_kl.linear_slowdown_specialization, sald.discrete_forward_kl.residual_exponent_bound, and sald.discrete_forward_kl.accumulated_error_bridge.",
    "Select the next lower target as sald.discrete_forward_kl.accumulated_error_bridge, because the theorem-level route is wired and the remaining statement-display risk is the linear-slowdown collection of A_alpha, barGamma, and barDelta."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through the common-space and finite-log-mgf interface; no entropy-duality theorem is imported or marked formalized.",
    "lem:gronwall remains the endpoint-safe real-analysis obligation with stitched-interval regularity, coefficient regularity, endpoint rewrites, and exponent side conditions.",
    "eq:LSI-KL-FI remains the density-test and Fisher-chain obligation; compiled scalar and RN-density helpers are dependencies only.",
    "The continuous forward-KL derivative/Fokker-Planck route remains a reusable obligation for the target transport term; it is not promoted by this discrete middle audit.",
    "The EM interpolation endpoint and conditional-law Fokker-Planck backend remains the discrete slow backend; endpoint vector/law algebra is only a local handoff."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle46_theorem_skeleton_route",
    "sald.discrete_forward_kl.cycle46_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.linear_slowdown_specialization",
    "sald.discrete_forward_kl.residual_exponent_bound",
    "sald.discrete_forward_kl.accumulated_error_bridge",
    "sald.discrete_forward_kl.coefficient_chain_audit"
  ]
  lowerPacket := [
    "Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.",
    "First lower sub-slice: expose the endpointBridge and initialExponentSplit for K(0)=KL(rho_0||pi_0), K(T)=KL(rho_K^eta||pi_T), and the two source exponent factors after t(s)=s/r.",
    "Cycle 46 lower compiled the initial-exponent scalar/integral split as SALD.discreteForwardKlGronwallCoeffIntervalIntegrable, SALD.discreteForwardKlGronwallCoeffIntegralSubSub, SALD.discreteForwardKlGronwallInitialExponentSplitScalar, and SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces.",
    "Second lower sub-slice: connect the already compiled collection algebra SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, and SALD.discreteForwardKlAccumulatedErrorCollectionScalar to the theorem display, without changing constants.",
    "Leave residual-exponent monotonicity, barGamma identification, stitched-interval Gronwall, EM conditional-FP, frozen-defect specialization, DV finite-log-mgf, and LSI/KL/FI as obligations unless exact compiled proofs are added.",
    "Do not work on the general VA-SALD discrete theorem in this lower packet; this cycle stabilizes thm:forward-KL-discrete first."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract lists SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle46_middle_route_audit after the theorem skeleton route and before lower EM, defect, DV, and Gronwall nodes.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle46DiscreteForwardKlSkeletonMiddleContract, SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle46_middle_route_audit.",
    "No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-46 middle obligation tying the discrete route audit to lower work. -/