AutoSamplingTheory.SALD.discreteForwardKlStatementContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlStatementContract : DiscreteForwardKlStatementContract

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.

theoremLabel : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

thm:forward-KL-discrete

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

emUpdate : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Discrete SALD eq:sald_em_terminal_disc_prop_additive_final with rho_k^eta=Law(X_k^eta), K=S/eta, and t_k=t(k*eta).

interpolation : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The proof uses the continuous EM interpolation hat X_s from eq:frozen_interp_terminal_disc_prop_additive_final and hat rho_s=Law(hat X_s).

linearSlowdown : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The statement is for t(s)=s/r with r>=1, hence S=r*T and dot{s}(t)=r.

lipschitzAssumptions : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Score space Lipschitz eq:lip_SALD_1 and time Lipschitz eq:lip_SALD_2 with constants L_{pi,space}, L_{pi,time} and measurable M.

complexityAssumptions : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

There exists alpha0'>0 with E_{alpha0'}(pi_t,nabla log pi_t)<infty and E_{alpha0'}(pi_t,1+M)<infty for every t in [0,T], in addition to the continuous forward-KL assumptions.

stepSizeCondition : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

4*eta^2*L_{pi,space}^2 < 1/2, matching main_body.tex line 305 and appendix lemma eta^2*L_{pi,space}^2 < 1/8.

alphaRange : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

For any alpha in (0,alpha0) and alpha' in (0,alpha0']; note the source theorem uses an open upper endpoint for alpha here.

gammaDeltaDefinitions : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Gamma(t)=2*L_time^2+64*L_space^2*(dot{s}(t)^(-2)+1+eta^2*L_time^2), Delta(t)=64*eta*L_space^2*E_{alpha'}(pi_t,nabla log pi_t)+2*eta*L_time^2*(1+32*eta^2*L_space^2)*E_{alpha'}(pi_t,1+M)+16*d*L_space^2, with bar Gamma and bar Delta the integrals over [0,T].

terminalBound : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

KL(rho_K^eta||pi_T) <= exp(-r*int_0^T C_LSI(t)dt)*exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha')*KL(rho_0||pi_0) + exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha')*((1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'}).

proofSteps : List String (explicit)

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

Ordered data items

1. main_body.tex:273-298 states the score Lipschitz assumptions and defines Gamma, Delta, bar Gamma, and bar Delta.
2. appendix.tex:260-266 defines the continuous EM interpolation hat X_s whose endpoints match rho_k^eta.
3. appendix.tex:268-330 states lem:frozen_delta_cross_lip_sald for the one-step frozen score defect; its proof is deferred to the general lemma.
4. appendix.tex:334-491 differentiates KL(hat rho_s||tilde pi_s), uses the interpolation Fokker--Planck equation, applies the frozen defect bound, Young, and LSI.
5. appendix.tex:493-523 applies DV with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2 to control the moving velocity term.
6. appendix.tex:526-592 changes from s to t, applies lem:gronwall, then specializes to linear slowdown to reach the main-body theorem bound.

dependencies : List String (explicit)

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

Ordered data items

1. thm:forward-KL
2. eq:frozen_interp_terminal_disc_prop_additive_final
3. lem:frozen_delta_cross_lip_sald
4. lem:dv_variation
5. lem:gronwall
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. sald.discrete_forward_kl.dv_finite_log_mgf_witness
10. sald.discrete_forward_kl.dv_velocity_bound
11. sald.discrete_forward_kl.gronwall_accumulation
12. sald.discrete_forward_kl.linear_slowdown_specialization
13. SALD.cycle19DiscreteForwardKlMiddleContract
14. SALD.cycle23DiscreteForwardKlUpperPacket
15. SALD.cycle23DiscreteForwardKlMiddleContract
16. SALD.cycle27DiscreteForwardKlUpperPacket
17. SALD.cycle27DiscreteForwardKlMiddleContract
18. SALD.cycle40DiscreteForwardKlEmFpMiddleContract
19. sald.discrete_forward_kl.cycle40_em_fp_middle
20. sald.discrete_forward_kl.cycle19_accumulated_error_middle
21. sald.discrete_forward_kl.cycle23_coefficient_chain_middle
22. sald.discrete_forward_kl.cycle27_accumulated_collection_upper
23. sald.discrete_forward_kl.cycle27_accumulated_collection_middle
24. SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces
25. sald.discrete_forward_kl.accumulated_error_bridge
26. sald.discrete_forward_kl.coefficient_chain_audit

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.contractOnly — stored label only; no proof certification

def discreteForwardKlStatementContract : DiscreteForwardKlStatementContract where
  theoremLabel := "thm:forward-KL-discrete"
  sourceStatement := saldForwardKlDiscreteSource
  sourceProof := saldForwardKlDiscreteProofSource
  emUpdate := "Discrete SALD eq:sald_em_terminal_disc_prop_additive_final with rho_k^eta=Law(X_k^eta), K=S/eta, and t_k=t(k*eta)."
  interpolation := "The proof uses the continuous EM interpolation hat X_s from eq:frozen_interp_terminal_disc_prop_additive_final and hat rho_s=Law(hat X_s)."
  linearSlowdown := "The statement is for t(s)=s/r with r>=1, hence S=r*T and dot{s}(t)=r."
  lipschitzAssumptions := "Score space Lipschitz eq:lip_SALD_1 and time Lipschitz eq:lip_SALD_2 with constants L_{pi,space}, L_{pi,time} and measurable M."
  complexityAssumptions := "There exists alpha0'>0 with E_{alpha0'}(pi_t,nabla log pi_t)<infty and E_{alpha0'}(pi_t,1+M)<infty for every t in [0,T], in addition to the continuous forward-KL assumptions."
  stepSizeCondition := "4*eta^2*L_{pi,space}^2 < 1/2, matching main_body.tex line 305 and appendix lemma eta^2*L_{pi,space}^2 < 1/8."
  alphaRange := "For any alpha in (0,alpha0) and alpha' in (0,alpha0']; note the source theorem uses an open upper endpoint for alpha here."
  gammaDeltaDefinitions := "Gamma(t)=2*L_time^2+64*L_space^2*(dot{s}(t)^(-2)+1+eta^2*L_time^2), Delta(t)=64*eta*L_space^2*E_{alpha'}(pi_t,nabla log pi_t)+2*eta*L_time^2*(1+32*eta^2*L_space^2)*E_{alpha'}(pi_t,1+M)+16*d*L_space^2, with bar Gamma and bar Delta the integrals over [0,T]."
  terminalBound := "KL(rho_K^eta||pi_T) <= exp(-r*int_0^T C_LSI(t)dt)*exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha')*KL(rho_0||pi_0) + exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha')*((1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'})."
  proofSteps := [
    "main_body.tex:273-298 states the score Lipschitz assumptions and defines Gamma, Delta, bar Gamma, and bar Delta.",
    "appendix.tex:260-266 defines the continuous EM interpolation hat X_s whose endpoints match rho_k^eta.",
    "appendix.tex:268-330 states lem:frozen_delta_cross_lip_sald for the one-step frozen score defect; its proof is deferred to the general lemma.",
    "appendix.tex:334-491 differentiates KL(hat rho_s||tilde pi_s), uses the interpolation Fokker--Planck equation, applies the frozen defect bound, Young, and LSI.",
    "appendix.tex:493-523 applies DV with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2 to control the moving velocity term.",
    "appendix.tex:526-592 changes from s to t, applies lem:gronwall, then specializes to linear slowdown to reach the main-body theorem bound."
  ]
  dependencies := [
    "thm:forward-KL",
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:frozen_delta_cross_lip_sald",
    "lem:dv_variation",
    "lem:gronwall",
    "sald.discrete_forward_kl.em_interpolation_fp",
    "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.cycle19DiscreteForwardKlMiddleContract",
    "SALD.cycle23DiscreteForwardKlUpperPacket",
    "SALD.cycle23DiscreteForwardKlMiddleContract",
    "SALD.cycle27DiscreteForwardKlUpperPacket",
    "SALD.cycle27DiscreteForwardKlMiddleContract",
    "SALD.cycle40DiscreteForwardKlEmFpMiddleContract",
    "sald.discrete_forward_kl.cycle40_em_fp_middle",
    "sald.discrete_forward_kl.cycle19_accumulated_error_middle",
    "sald.discrete_forward_kl.cycle23_coefficient_chain_middle",
    "sald.discrete_forward_kl.cycle27_accumulated_collection_upper",
    "sald.discrete_forward_kl.cycle27_accumulated_collection_middle",
    "SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces",
    "sald.discrete_forward_kl.accumulated_error_bridge",
    "sald.discrete_forward_kl.coefficient_chain_audit"
  ]
  status := ProofStatus.contractOnly