AutoSamplingTheory.SALD.forwardKlGronwallSideConditionContract

Data definition / provenance and workflow record

Meaning and type

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

def forwardKlGronwallSideConditionContract :
    ForwardKlGronwallSideConditionContract

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.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

endpointScheduleIdentities : String (explicit)

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

The final bound is stated at t=T and t=0; the Lean route must provide the endpoint-schedule interface s(0)=0, S=s(T), t(s(T))=T, and tilde_pi_{s(t)}=pi_t on [0,T].

terminalKlIdentification : String (explicit)

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

The Gronwall output K(T) is rewritten as KL(rho_S||pi_T) using S=s(T) and tilde_pi_{s(T)}=pi_T.

initialKlIdentification : String (explicit)

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

The initial term K(0) is rewritten as KL(rho_0||pi_0) using s(0)=0 and tilde_pi_{s(0)}=pi_0.

coefficientRegularity : String (explicit)

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

a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t) must satisfy the continuity or interval-integrability hypotheses required by lem:gronwall.

signFactsForResidualDrop : String (explicit)

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

The residual-exponent simplification uses C_LSI(u)>=0 and dot{s}(u)>0, so -int_t^T dot{s}(u)*C_LSI(u) du <= 0.

exponentSplitAlgebra : String (explicit)

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

Split exp(-int a) into exp(-int dot{s}*C_LSI)*exp(int (1/2)*dot{s}^(-1)*alpha^(-1)) for the initial term, and use SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces to assemble the LSI/alpha-piece interval-integrability hypotheses before applying the reusable Gronwall congruence.

residualExponentBound : String (explicit)

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

For the residual integral, bound exp(-int_t^T a(u)du) by exp(int_t^T (1/2)*dot{s}(u)^(-1)*alpha^(-1)du) by dropping the nonpositive LSI contribution.

dependencies : List String (explicit)

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

Ordered data items

1. sald.forward_kl.moving_target_dependency_chain
2. sald.forward_kl.endpoint_schedule_identities
3. sald.forward_kl.schedule_time_change
4. sald.forward_kl.kl_derivative
5. sald.forward_kl.dv_energy_bound
6. sald.gronwall.integrating_factor
7. SALD.gronwallIntervalIntegralAdditivityScalar
8. SALD.gronwallExpProductRewriteIntervalIntegral
9. SALD.gronwallExpProductRewriteIntegralCongr
10. SALD.forwardKlGronwallCoeffIntervalIntegrable
11. SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable
12. SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces
13. SALD.forwardKlGronwallCoeffIntegralSub
14. SALD.forwardKlGronwallInitialExponentSplitScalar
15. SALD.forwardKlGronwallInitialExponentSplitOfPieces
16. SALD.forwardKlGronwallResidualExponentDropScalar
17. SALD.forwardKlGronwallResidualExponentDropIntegral

sourceGaps : List String (explicit)

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

Ordered data items

1. the source theorem names the inverse slowdown but does not isolate s(0)=0, S=s(T), or t(s(T))=T as a separate endpoint lemma
2. the proof applies Gronwall without separately proving continuity or interval-integrability for a(t) and b(t)
3. the residual exponent drop still needs theorem-specific proof that int_t^T dot{s}(u)*C_LSI(u) du is nonnegative and that b(t) is nonnegative/integrable

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 forwardKlGronwallSideConditionContract :
    ForwardKlGronwallSideConditionContract where
  sourceBlock := saldForwardKlGronwallSource
  theoremStatement := saldForwardKlSource
  endpointScheduleIdentities := "The final bound is stated at t=T and t=0; the Lean route must provide the endpoint-schedule interface s(0)=0, S=s(T), t(s(T))=T, and tilde_pi_{s(t)}=pi_t on [0,T]."
  terminalKlIdentification := "The Gronwall output K(T) is rewritten as KL(rho_S||pi_T) using S=s(T) and tilde_pi_{s(T)}=pi_T."
  initialKlIdentification := "The initial term K(0) is rewritten as KL(rho_0||pi_0) using s(0)=0 and tilde_pi_{s(0)}=pi_0."
  coefficientRegularity := "a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t) must satisfy the continuity or interval-integrability hypotheses required by lem:gronwall."
  signFactsForResidualDrop := "The residual-exponent simplification uses C_LSI(u)>=0 and dot{s}(u)>0, so -int_t^T dot{s}(u)*C_LSI(u) du <= 0."
  exponentSplitAlgebra := "Split exp(-int a) into exp(-int dot{s}*C_LSI)*exp(int (1/2)*dot{s}^(-1)*alpha^(-1)) for the initial term, and use SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces to assemble the LSI/alpha-piece interval-integrability hypotheses before applying the reusable Gronwall congruence."
  residualExponentBound := "For the residual integral, bound exp(-int_t^T a(u)du) by exp(int_t^T (1/2)*dot{s}(u)^(-1)*alpha^(-1)du) by dropping the nonpositive LSI contribution."
  dependencies := [
    "sald.forward_kl.moving_target_dependency_chain",
    "sald.forward_kl.endpoint_schedule_identities",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.kl_derivative",
    "sald.forward_kl.dv_energy_bound",
    "sald.gronwall.integrating_factor",
    "SALD.gronwallIntervalIntegralAdditivityScalar",
    "SALD.gronwallExpProductRewriteIntervalIntegral",
    "SALD.gronwallExpProductRewriteIntegralCongr",
    "SALD.forwardKlGronwallCoeffIntervalIntegrable",
    "SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable",
    "SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces",
    "SALD.forwardKlGronwallCoeffIntegralSub",
    "SALD.forwardKlGronwallInitialExponentSplitScalar",
    "SALD.forwardKlGronwallInitialExponentSplitOfPieces",
    "SALD.forwardKlGronwallResidualExponentDropScalar",
    "SALD.forwardKlGronwallResidualExponentDropIntegral"
  ]
  sourceGaps := [
    "the source theorem names the inverse slowdown but does not isolate s(0)=0, S=s(T), or t(s(T))=T as a separate endpoint lemma",
    "the proof applies Gronwall without separately proving continuity or interval-integrability for a(t) and b(t)",
    "the residual exponent drop still needs theorem-specific proof that int_t^T dot{s}(u)*C_LSI(u) du is nonnegative and that b(t) is nonnegative/integrable"
  ]
  status := ProofStatus.obligation