AutoSamplingTheory.SALD.cycle18ForwardKlMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle18ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract

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.saldForwardKlSource — audited data reference, not expanded and not a compiled dependency edge

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

dvSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlGronwallSource — 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-18 upper target into a lower-ready map for sald.forward_kl.gronwall_side_conditions, with the final Gronwall endpoint, exponent-splitting, residual-exponent, and scalar-helper bridge kept separate from DV, LSI, KL-derivative, and schedule backends.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:238-247 fixes the theorem statement, inverse slowdown notation, C_LSI(t)>=0, alpha in (0,alpha0], and the two-exponential terminal display; no new theorem hypotheses are introduced.
2. appendix.tex:210-228 supplies the LSI/time-change side of the coefficient a(t), but the LSI-to-KL/FI density-test proof and inverse-schedule calculus remain separate obligations.
3. appendix.tex:230-241 supplies the DV side of the coefficient a(t) and b(t) through Z=alpha*||v_t||^2; finite-log-mgf and common-space facts remain in the DV witness obligation.
4. appendix.tex:244-248 applies lem:gronwall with 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).
5. appendix.tex:249-252 splits the initial exponent into the LSI contraction factor and alpha factor, then drops only the nonpositive LSI contribution from the residual exponent.
6. appendix.tex:63-69 supplies the reusable scalar exponent pattern; cycle-17 formalized the Real additive/exponential algebra, cycle 18 added the adjacent-interval integral bridge, and cycle 21 adds the outer-integral congruence wrapper once adjacent interval-integrability is available.

leanStepMap : List String (explicit)

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

Ordered data items

1. The theorem statement remains SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract; this packet changes neither.
2. Endpoint rewrites K(T)=KL(rho_S||pi_T) and K(0)=KL(rho_0||pi_0) remain routed through SALD.forwardKlEndpointScheduleContract and sald.forward_kl.endpoint_schedule_identities.
3. The final Gronwall side conditions are routed through SALD.forwardKlGronwallSideConditionContract and SALD.forwardKlGronwallSideConditionObligation.
4. The initial exponent split should first produce interval-integral equalities for the two coefficient pieces; the reusable Gronwall interval steps are SALD.gronwallExpProductRewriteIntervalIntegral and SALD.gronwallExpProductRewriteIntegralCongr, which call the cycle-17 scalar helpers after adjacent interval-integrability is available.
5. The residual exponent drop needs sign facts C_LSI(u)>=0 and dot{s}(u)>0 plus interval-integral monotonicity; it is not supplied by the cycle-17 scalar helper lemmas.
6. Coefficient regularity for a(t), b(t) remains the local interface required before lem:gronwall can be instantiated.

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 Cor. 4.15 or a future local entropy-duality port; this packet does not import or formalize it.
2. eq:LSI-KL-FI remains the local density-test obligation using phi=sqrt(rho/pi), with coefficient 1/(2*C_LSI) unchanged.
3. lem:gronwall remains the local real-analysis obligation; the cycle-17 scalar helper lemmas and cycle-18 interval bridge are only substeps of the exponent rewrite.
4. No SLT theorem is used for endpoint rewrites, coefficient regularity, exponent splitting, or residual exponent monotonicity.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.gronwall_side_conditions
2. sald.forward_kl.endpoint_schedule_identities
3. sald.forward_kl.coefficient_chain_audit
4. sald.forward_kl.gronwall_application
5. sald.gronwall.exponent_rewrite
6. sald.gronwall.integrating_factor
7. SALD.gronwallExponentRewriteObligation
8. SALD.forwardKlGronwallSideConditionObligation
9. SALD.forwardKlDvFiniteLogMgfWitnessObligation
10. SALD.lsiKlFiDensityTestObligation

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.
2. Preferred sub-slice: bridge interval-integral additivity/orientation to the cycle-17 scalar helpers for the reusable exponent split, then record theorem-specific interval-integrability and residual-exponent monotonicity obligations separately.
3. Do not change SALD.forwardKlDvFiniteLogMgfWitnessContract, SALD.saldLsiKlFiDensityTestContract, SALD.continuousForwardKlStatementContract, or the source theorem display.
4. Do not mark endpoint rewrites, coefficient regularity, residual exponent drop, DV, LSI-to-KL/FI, KL derivative, schedule, or full Gronwall formalized unless a compiled local proof is added.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlProofDag lists SALD.cycle18ForwardKlMiddleContract inside the Gronwall side-condition block and keeps the cycle-17 scalar helpers plus SALD.gronwallExpProductRewriteIntervalIntegral and SALD.gronwallExpProductRewriteIntegralCongr as local dependencies only.
2. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle18ForwardKlMiddleContract while retaining cycle-14 upper/middle and cycle-18 upper dependencies.
3. The conversion window and proof-obligation ledger record this packet as source-to-Lean synchronization, not a proof of thm:forward-KL.
4. SALD_original.jsonl still indexes thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall while excluding sald_version_2.tex.
5. No fake proof closure appears and no analytic dependency is promoted.

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 cycle18ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Translate the cycle-18 upper target into a lower-ready map for sald.forward_kl.gronwall_side_conditions, with the final Gronwall endpoint, exponent-splitting, residual-exponent, and scalar-helper bridge kept separate from DV, LSI, KL-derivative, and schedule backends."
  sourceStepMap := [
    "main_body.tex:238-247 fixes the theorem statement, inverse slowdown notation, C_LSI(t)>=0, alpha in (0,alpha0], and the two-exponential terminal display; no new theorem hypotheses are introduced.",
    "appendix.tex:210-228 supplies the LSI/time-change side of the coefficient a(t), but the LSI-to-KL/FI density-test proof and inverse-schedule calculus remain separate obligations.",
    "appendix.tex:230-241 supplies the DV side of the coefficient a(t) and b(t) through Z=alpha*||v_t||^2; finite-log-mgf and common-space facts remain in the DV witness obligation.",
    "appendix.tex:244-248 applies lem:gronwall with 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).",
    "appendix.tex:249-252 splits the initial exponent into the LSI contraction factor and alpha factor, then drops only the nonpositive LSI contribution from the residual exponent.",
    "appendix.tex:63-69 supplies the reusable scalar exponent pattern; cycle-17 formalized the Real additive/exponential algebra, cycle 18 added the adjacent-interval integral bridge, and cycle 21 adds the outer-integral congruence wrapper once adjacent interval-integrability is available."
  ]
  leanStepMap := [
    "The theorem statement remains SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract; this packet changes neither.",
    "Endpoint rewrites K(T)=KL(rho_S||pi_T) and K(0)=KL(rho_0||pi_0) remain routed through SALD.forwardKlEndpointScheduleContract and sald.forward_kl.endpoint_schedule_identities.",
    "The final Gronwall side conditions are routed through SALD.forwardKlGronwallSideConditionContract and SALD.forwardKlGronwallSideConditionObligation.",
    "The initial exponent split should first produce interval-integral equalities for the two coefficient pieces; the reusable Gronwall interval steps are SALD.gronwallExpProductRewriteIntervalIntegral and SALD.gronwallExpProductRewriteIntegralCongr, which call the cycle-17 scalar helpers after adjacent interval-integrability is available.",
    "The residual exponent drop needs sign facts C_LSI(u)>=0 and dot{s}(u)>0 plus interval-integral monotonicity; it is not supplied by the cycle-17 scalar helper lemmas.",
    "Coefficient regularity for a(t), b(t) remains the local interface required before lem:gronwall can be instantiated."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through Boucheron Cor. 4.15 or a future local entropy-duality port; this packet does not import or formalize it.",
    "eq:LSI-KL-FI remains the local density-test obligation using phi=sqrt(rho/pi), with coefficient 1/(2*C_LSI) unchanged.",
    "lem:gronwall remains the local real-analysis obligation; the cycle-17 scalar helper lemmas and cycle-18 interval bridge are only substeps of the exponent rewrite.",
    "No SLT theorem is used for endpoint rewrites, coefficient regularity, exponent splitting, or residual exponent monotonicity."
  ]
  obligations := [
    "sald.forward_kl.gronwall_side_conditions",
    "sald.forward_kl.endpoint_schedule_identities",
    "sald.forward_kl.coefficient_chain_audit",
    "sald.forward_kl.gronwall_application",
    "sald.gronwall.exponent_rewrite",
    "sald.gronwall.integrating_factor",
    "SALD.gronwallExponentRewriteObligation",
    "SALD.forwardKlGronwallSideConditionObligation",
    "SALD.forwardKlDvFiniteLogMgfWitnessObligation",
    "SALD.lsiKlFiDensityTestObligation"
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.",
    "Preferred sub-slice: bridge interval-integral additivity/orientation to the cycle-17 scalar helpers for the reusable exponent split, then record theorem-specific interval-integrability and residual-exponent monotonicity obligations separately.",
    "Do not change SALD.forwardKlDvFiniteLogMgfWitnessContract, SALD.saldLsiKlFiDensityTestContract, SALD.continuousForwardKlStatementContract, or the source theorem display.",
    "Do not mark endpoint rewrites, coefficient regularity, residual exponent drop, DV, LSI-to-KL/FI, KL derivative, schedule, or full Gronwall formalized unless a compiled local proof is added."
  ]
  reviewerChecklist := [
    "SALD.forwardKlProofDag lists SALD.cycle18ForwardKlMiddleContract inside the Gronwall side-condition block and keeps the cycle-17 scalar helpers plus SALD.gronwallExpProductRewriteIntervalIntegral and SALD.gronwallExpProductRewriteIntegralCongr as local dependencies only.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle18ForwardKlMiddleContract while retaining cycle-14 upper/middle and cycle-18 upper dependencies.",
    "The conversion window and proof-obligation ledger record this packet as source-to-Lean synchronization, not a proof of thm:forward-KL.",
    "SALD_original.jsonl still indexes thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall while excluding sald_version_2.tex.",
    "No fake proof closure appears and no analytic dependency is promoted."
  ]
  status := ProofStatus.obligation

/-- Cycle-22 upper packet for the continuous forward-KL Gronwall side conditions.

This packet follows the cycle-21 Gronwall outer-integral congruence refinement.
It selects only the theorem-specific coefficient regularity and interval-
integrability bridge needed before the compiled Gronwall exponent sublemmas can
be used inside the continuous forward-KL display.  It does not change
`thm:forward-KL` or promote DV, LSI, the KL derivative, endpoint rewrites, or
the full Gronwall lemma.
-/