AutoSamplingTheory.SALD.cycle11DiscreteForwardKlMiddleContract

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

Map the cycle-focus proof route for thm:forward-KL-discrete from EM interpolation through one-step defects and accumulated errors, while keeping the theorem statement and constants unchanged.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:260-266 and 334-335: define hat X_s and use endpoint laws for hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta.
2. appendix.tex:347-385: define bar b_{k,s} and invoke the conditional-drift Fokker--Planck equation for the frozen EM interpolation.
3. appendix.tex:454-467: apply lem:frozen_delta_cross_lip_sald to introduce the one-step Gamma and Delta defects.
4. appendix.tex:469-523: apply Young to the moving velocity term and then the DV finite-log-mgf witness with the dot t(s)^2 coefficient.
5. appendix.tex:526-553: change from s to t and preserve dot{s}(t)^(-1)*alpha^(-1), 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma, and 2*dot{s}(t)*eta*Delta.
6. appendix.tex:557-590 with main_body.tex:309-323: apply Gronwall, specialize t(s)=s/r, and collect A_alpha, barGamma, and barDelta_{alpha'}.

leanStepMap : List String (explicit)

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

Ordered data items

1. EM endpoint laws and interpolation Fokker--Planck are tracked by SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp.
2. The frozen one-step defect is tracked by SALD.frozenDeltaCrossLipSaldContract and sald.discrete_forward_kl.frozen_delta_cross_lip.
3. The derivative inequality before Gronwall is tracked by SALD.discreteForwardKlDerivativeCandidateContract and sald.discrete_forward_kl.kl_derivative.
4. The DV velocity estimate is split between SALD.discreteForwardKlDvFiniteLogMgfWitnessContract and sald.discrete_forward_kl.dv_velocity_bound.
5. The global scalar step is split between SALD.discreteForwardKlGronwallInstantiationContract, SALD.discreteForwardKlAccumulatedErrorBridgeContract, sald.discrete_forward_kl.residual_exponent_bound, and SALD.discreteForwardKlCoefficientChainAuditContract.

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 Boucheron Corollary 4.15 or the SLT entropy_duality pattern; no SLT theorem is imported.
2. lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor.
3. eq:LSI-KL-FI remains an obligation through probability.lsi_to_kl_fi.
4. SLT one_step_discretization is only a reference pattern for the EM interpolation backend.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.em_endpoint_laws
2. sald.discrete_forward_kl.em_conditional_fokker_planck
3. sald.discrete_forward_kl.stitched_interval_regularity
4. sald.discrete_forward_kl.frozen_delta_cross_lip
5. sald.discrete_forward_kl.kl_derivative
6. sald.discrete_forward_kl.dv_finite_log_mgf_witness
7. sald.discrete_forward_kl.dv_velocity_bound
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.coefficient_chain_audit

lowerPacket : List String (explicit)

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

Ordered data items

1. Preferred lower target for EM work: refine SALD.discreteForwardKlEmInterpolationSideConditionContract or sald.discrete_forward_kl.em_conditional_fokker_planck, keeping endpoint laws and conditional drift separate.
2. Preferred lower target for accumulated-error work: refine SALD.discreteForwardKlAccumulatedErrorBridgeContract or sald.discrete_forward_kl.accumulated_error_bridge, keeping the appendix Gronwall display distinct from the main-body linear-slowdown theorem bound.
3. Cycle 11 lower scalar target: refine sald.discrete_forward_kl.residual_exponent_bound for the residual exponent drop and full-interval Gamma bound.
4. Do not restate thm:forward-KL-discrete, add hidden smoothness assumptions, or alter the Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, or r coefficients.
5. If touching the DV substep, depend on sald.discrete_forward_kl.dv_finite_log_mgf_witness rather than adding a new finite-mgf theorem assumption.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. Every source step from appendix.tex:260-590 maps to an existing Lean contract, cited result, or proof obligation.
2. The EM interpolation backend, frozen-defect lemma, DV witness, Gronwall accumulation, and accumulated-error bridge remain separate lower targets.
3. The final theorem display in main_body.tex:309-323 is unchanged.
4. sald_version_2.tex remains excluded from source correspondence.
5. No analytic dependency is marked formalized and no fake proof closure is introduced.

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 cycle11DiscreteForwardKlMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Map the cycle-focus proof route for thm:forward-KL-discrete from EM interpolation through one-step defects and accumulated errors, while keeping the theorem statement and constants unchanged."
  sourceStepMap := [
    "appendix.tex:260-266 and 334-335: define hat X_s and use endpoint laws for hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta.",
    "appendix.tex:347-385: define bar b_{k,s} and invoke the conditional-drift Fokker--Planck equation for the frozen EM interpolation.",
    "appendix.tex:454-467: apply lem:frozen_delta_cross_lip_sald to introduce the one-step Gamma and Delta defects.",
    "appendix.tex:469-523: apply Young to the moving velocity term and then the DV finite-log-mgf witness with the dot t(s)^2 coefficient.",
    "appendix.tex:526-553: change from s to t and preserve dot{s}(t)^(-1)*alpha^(-1), 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma, and 2*dot{s}(t)*eta*Delta.",
    "appendix.tex:557-590 with main_body.tex:309-323: apply Gronwall, specialize t(s)=s/r, and collect A_alpha, barGamma, and barDelta_{alpha'}."
  ]
  leanStepMap := [
    "EM endpoint laws and interpolation Fokker--Planck are tracked by SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp.",
    "The frozen one-step defect is tracked by SALD.frozenDeltaCrossLipSaldContract and sald.discrete_forward_kl.frozen_delta_cross_lip.",
    "The derivative inequality before Gronwall is tracked by SALD.discreteForwardKlDerivativeCandidateContract and sald.discrete_forward_kl.kl_derivative.",
    "The DV velocity estimate is split between SALD.discreteForwardKlDvFiniteLogMgfWitnessContract and sald.discrete_forward_kl.dv_velocity_bound.",
    "The global scalar step is split between SALD.discreteForwardKlGronwallInstantiationContract, SALD.discreteForwardKlAccumulatedErrorBridgeContract, sald.discrete_forward_kl.residual_exponent_bound, and SALD.discreteForwardKlCoefficientChainAuditContract."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through Boucheron Corollary 4.15 or the SLT entropy_duality pattern; no SLT theorem is imported.",
    "lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor.",
    "eq:LSI-KL-FI remains an obligation through probability.lsi_to_kl_fi.",
    "SLT one_step_discretization is only a reference pattern for the EM interpolation backend."
  ]
  obligations := [
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "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.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 := [
    "Preferred lower target for EM work: refine SALD.discreteForwardKlEmInterpolationSideConditionContract or sald.discrete_forward_kl.em_conditional_fokker_planck, keeping endpoint laws and conditional drift separate.",
    "Preferred lower target for accumulated-error work: refine SALD.discreteForwardKlAccumulatedErrorBridgeContract or sald.discrete_forward_kl.accumulated_error_bridge, keeping the appendix Gronwall display distinct from the main-body linear-slowdown theorem bound.",
    "Cycle 11 lower scalar target: refine sald.discrete_forward_kl.residual_exponent_bound for the residual exponent drop and full-interval Gamma bound.",
    "Do not restate thm:forward-KL-discrete, add hidden smoothness assumptions, or alter the Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, or r coefficients.",
    "If touching the DV substep, depend on sald.discrete_forward_kl.dv_finite_log_mgf_witness rather than adding a new finite-mgf theorem assumption."
  ]
  reviewerChecklist := [
    "Every source step from appendix.tex:260-590 maps to an existing Lean contract, cited result, or proof obligation.",
    "The EM interpolation backend, frozen-defect lemma, DV witness, Gronwall accumulation, and accumulated-error bridge remain separate lower targets.",
    "The final theorem display in main_body.tex:309-323 is unchanged.",
    "sald_version_2.tex remains excluded from source correspondence.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation