AutoSamplingTheory.SALD.cycle23DiscreteForwardKlMiddleContract

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

Translate the cycle-23 coefficient-chain target into a lower-ready audit for sald.discrete_forward_kl.coefficient_chain_audit, with appendix.tex:454-553 as the first slice and appendix.tex:557-590 to main_body.tex:309-323 kept as the follow-on accumulated-error bridge.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:273-323 fixes the score Lipschitz assumptions, Gamma, Delta, barGamma, barDelta, t(s)=s/r, alpha ranges, step-size condition, and final theorem constants.
2. appendix.tex:454-467 applies lem:frozen_delta_cross_lip_sald and contributes the first (1/4)*FI term plus 2*eta^2*alpha'^(-1)*Gamma(t(s))*K_s and 2*eta*Delta(t(s)).
3. appendix.tex:469-479 applies Cauchy-Schwarz/Young to the moving velocity cross term and contributes the second (1/4)*FI term plus ||tilde v_s||_{L2(hat rho_s)}^2.
4. appendix.tex:481-493 combines the two cross-term bounds, leaves -(1/2)*FI, and invokes the LSI-to-KL/FI comparison to obtain -C_LSI(t(s))*K_s.
5. appendix.tex:496-523 applies DV with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2, preserving the dot t(s)^2*alpha^(-1) coefficient.
6. appendix.tex:526-553 changes variables from s to t and rewrites dot{s}(t)*dot t(s(t))^2 as dot{s}(t)^(-1), while preserving the Gamma and Delta coefficients.
7. appendix.tex:557-590 and main_body.tex:309-323 are not part of the first lower slice; they remain the endpoint, residual-exponent, barGamma, and barDelta accumulated-error bridge.

leanStepMap : List String (explicit)

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

Ordered data items

1. The theorem statement remains SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract; this packet adds no hypothesis and proves no terminal KL bound.
2. The lower-facing ledger is SALD.discreteForwardKlCoefficientChainAuditContract and the named obligation sald.discrete_forward_kl.coefficient_chain_audit.
3. The first lower slice depends on sald.discrete_forward_kl.frozen_delta_cross_lip, sald.discrete_forward_kl.kl_derivative, sald.discrete_forward_kl.dv_finite_log_mgf_witness, sald.discrete_forward_kl.dv_velocity_bound, and probability.lsi_to_kl_fi.
4. The time-change coefficient rewrite uses SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar once inverse-schedule regularity supplies dot t(s(t))=dot{s}(t)^(-1) and dot{s}(t)>0; those analytic facts remain obligations.
5. The follow-on bridge is SALD.discreteForwardKlAccumulatedErrorBridgeContract / sald.discrete_forward_kl.accumulated_error_bridge, with SALD.discreteForwardKlResidualExponentBoundScalar and SALD.discreteForwardKlResidualExpBoundScalar as only the scalar cores already formalized.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. eq:LSI-KL-FI remains the source-cited LSI-to-KL/FI comparison through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi.
2. lem:dv_variation remains source-cited through Boucheron Corollary 4.15 or the SLT entropy_duality pattern; this packet imports no SLT theorem.
3. lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor and is not reopened by the first coefficient slice.
4. The omitted SALD frozen-defect proof remains a faithful specialization obligation from the later general frozen-defect lemma, not a completed local theorem.
5. EM endpoint laws, conditional Fokker-Planck, stitched-interval regularity, coefficient integrability, and interval-integral monotonicity remain explicit obligations.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle23_coefficient_chain_middle
2. sald.discrete_forward_kl.coefficient_chain_audit
3. sald.discrete_forward_kl.frozen_delta_cross_lip
4. sald.discrete_forward_kl.kl_derivative
5. sald.discrete_forward_kl.dv_finite_log_mgf_witness
6. sald.discrete_forward_kl.dv_velocity_bound
7. SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar
8. sald.discrete_forward_kl.gronwall_accumulation
9. sald.discrete_forward_kl.linear_slowdown_specialization
10. sald.discrete_forward_kl.residual_exponent_bound
11. sald.discrete_forward_kl.accumulated_error_bridge
12. sald.discrete_forward_kl.em_endpoint_laws
13. sald.discrete_forward_kl.stitched_interval_regularity

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.discreteForwardKlCoefficientChainAuditContract / SALD.discreteForwardKlCoefficientChainObligation / sald.discrete_forward_kl.coefficient_chain_audit.
2. First sub-slice: appendix.tex:454-553 only, auditing the two (1/4)*FI cross-term coefficients, LSI conversion, DV dot t(s)^2*alpha^(-1) coefficient, and the time-change rewrite to dot{s}(t)^(-1)*alpha^(-1).
3. Do not attempt the full theorem, the EM Fokker-Planck backend, the omitted frozen-defect proof, the DV theorem, the Gronwall theorem, or the accumulated-error bridge in the same lower slice.
4. If the first slice is stable, the next slice is appendix.tex:557-590 to main_body.tex:309-323 through endpoint stitching, residual exponent drop, and full-interval A_alpha, barGamma, and barDelta collection.
5. Report any missing endpoint, integrability, or inverse-schedule fact as the corresponding named ProofObligation rather than adding hypotheses to thm:forward-KL-discrete.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle23_middle_coefficient_chain between the cycle-23 upper packet and the coefficient-chain audit block.
2. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle23DiscreteForwardKlMiddleContract and sald.discrete_forward_kl.cycle23_coefficient_chain_middle.
3. The conversion window, proof-obligation ledger, and SLT audit classify this packet as workflow/obligation data, not as a proof of thm:forward-KL-discrete.
4. The source constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'} are unchanged.
5. No analytic dependency is marked formalized and sald_version_2.tex remains excluded.

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 cycle23DiscreteForwardKlMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Translate the cycle-23 coefficient-chain target into a lower-ready audit for sald.discrete_forward_kl.coefficient_chain_audit, with appendix.tex:454-553 as the first slice and appendix.tex:557-590 to main_body.tex:309-323 kept as the follow-on accumulated-error bridge."
  sourceStepMap := [
    "main_body.tex:273-323 fixes the score Lipschitz assumptions, Gamma, Delta, barGamma, barDelta, t(s)=s/r, alpha ranges, step-size condition, and final theorem constants.",
    "appendix.tex:454-467 applies lem:frozen_delta_cross_lip_sald and contributes the first (1/4)*FI term plus 2*eta^2*alpha'^(-1)*Gamma(t(s))*K_s and 2*eta*Delta(t(s)).",
    "appendix.tex:469-479 applies Cauchy-Schwarz/Young to the moving velocity cross term and contributes the second (1/4)*FI term plus ||tilde v_s||_{L2(hat rho_s)}^2.",
    "appendix.tex:481-493 combines the two cross-term bounds, leaves -(1/2)*FI, and invokes the LSI-to-KL/FI comparison to obtain -C_LSI(t(s))*K_s.",
    "appendix.tex:496-523 applies DV with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2, preserving the dot t(s)^2*alpha^(-1) coefficient.",
    "appendix.tex:526-553 changes variables from s to t and rewrites dot{s}(t)*dot t(s(t))^2 as dot{s}(t)^(-1), while preserving the Gamma and Delta coefficients.",
    "appendix.tex:557-590 and main_body.tex:309-323 are not part of the first lower slice; they remain the endpoint, residual-exponent, barGamma, and barDelta accumulated-error bridge."
  ]
  leanStepMap := [
    "The theorem statement remains SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract; this packet adds no hypothesis and proves no terminal KL bound.",
    "The lower-facing ledger is SALD.discreteForwardKlCoefficientChainAuditContract and the named obligation sald.discrete_forward_kl.coefficient_chain_audit.",
    "The first lower slice depends on sald.discrete_forward_kl.frozen_delta_cross_lip, sald.discrete_forward_kl.kl_derivative, sald.discrete_forward_kl.dv_finite_log_mgf_witness, sald.discrete_forward_kl.dv_velocity_bound, and probability.lsi_to_kl_fi.",
    "The time-change coefficient rewrite uses SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar once inverse-schedule regularity supplies dot t(s(t))=dot{s}(t)^(-1) and dot{s}(t)>0; those analytic facts remain obligations.",
    "The follow-on bridge is SALD.discreteForwardKlAccumulatedErrorBridgeContract / sald.discrete_forward_kl.accumulated_error_bridge, with SALD.discreteForwardKlResidualExponentBoundScalar and SALD.discreteForwardKlResidualExpBoundScalar as only the scalar cores already formalized."
  ]
  citedResultInterfaces := [
    "eq:LSI-KL-FI remains the source-cited LSI-to-KL/FI comparison through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi.",
    "lem:dv_variation remains source-cited through Boucheron Corollary 4.15 or the SLT entropy_duality pattern; this packet imports no SLT theorem.",
    "lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor and is not reopened by the first coefficient slice.",
    "The omitted SALD frozen-defect proof remains a faithful specialization obligation from the later general frozen-defect lemma, not a completed local theorem.",
    "EM endpoint laws, conditional Fokker-Planck, stitched-interval regularity, coefficient integrability, and interval-integral monotonicity remain explicit obligations."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle23_coefficient_chain_middle",
    "sald.discrete_forward_kl.coefficient_chain_audit",
    "sald.discrete_forward_kl.frozen_delta_cross_lip",
    "sald.discrete_forward_kl.kl_derivative",
    "sald.discrete_forward_kl.dv_finite_log_mgf_witness",
    "sald.discrete_forward_kl.dv_velocity_bound",
    "SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar",
    "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.em_endpoint_laws",
    "sald.discrete_forward_kl.stitched_interval_regularity"
  ]
  lowerPacket := [
    "Target exactly SALD.discreteForwardKlCoefficientChainAuditContract / SALD.discreteForwardKlCoefficientChainObligation / sald.discrete_forward_kl.coefficient_chain_audit.",
    "First sub-slice: appendix.tex:454-553 only, auditing the two (1/4)*FI cross-term coefficients, LSI conversion, DV dot t(s)^2*alpha^(-1) coefficient, and the time-change rewrite to dot{s}(t)^(-1)*alpha^(-1).",
    "Do not attempt the full theorem, the EM Fokker-Planck backend, the omitted frozen-defect proof, the DV theorem, the Gronwall theorem, or the accumulated-error bridge in the same lower slice.",
    "If the first slice is stable, the next slice is appendix.tex:557-590 to main_body.tex:309-323 through endpoint stitching, residual exponent drop, and full-interval A_alpha, barGamma, and barDelta collection.",
    "Report any missing endpoint, integrability, or inverse-schedule fact as the corresponding named ProofObligation rather than adding hypotheses to thm:forward-KL-discrete."
  ]
  reviewerChecklist := [
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle23_middle_coefficient_chain between the cycle-23 upper packet and the coefficient-chain audit block.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle23DiscreteForwardKlMiddleContract and sald.discrete_forward_kl.cycle23_coefficient_chain_middle.",
    "The conversion window, proof-obligation ledger, and SLT audit classify this packet as workflow/obligation data, not as a proof of thm:forward-KL-discrete.",
    "The source constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'} are unchanged.",
    "No analytic dependency is marked formalized and sald_version_2.tex remains excluded."
  ]
  status := ProofStatus.obligation

/-- Cycle-27 upper packet for the discrete forward-KL accumulated-error bridge.

This returns to `thm:forward-KL-discrete` after the coefficient-chain audit and
selects the next faithful lower slice inside the final Gronwall-to-theorem
bridge.  The packet does not change the theorem statement or promote any
analytic backend; it only narrows the next lower target.
-/