AutoSamplingTheory.SALD.cycle22ForwardKlMiddleContract

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 cycle22ForwardKlMiddleContract :
    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-22 upper target into a lower-ready map for sald.forward_kl.gronwall_side_conditions: prove or isolate theorem-specific regularity and adjacent interval-integrability for the LSI and alpha pieces of a(t), and for b(t), before applying SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:210-217 supplies the nonnegative LSI part of a(t), namely dot{s}(t)*C_LSI(t), after the LSI-to-KL/FI bridge.
2. appendix.tex:218-228 supplies the inverse-schedule rewrite that turns the velocity coefficient into dot{s}(t)^(-1).
3. appendix.tex:230-241 supplies the DV alpha contribution (1/2)*dot{s}(t)^(-1)*alpha^(-1) to a(t) and the source b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t).
4. appendix.tex:244-248 applies lem:gronwall to K(t)=KL(rho_{s(t)}||pi_t) with exactly those a(t) and b(t); continuity or interval-integrability is implicit in the paper and must be exposed locally.
5. appendix.tex:249-250 splits the initial exponent into the LSI contraction factor and alpha factor; the compiled outer-integral congruence is applicable only after adjacent interval-integrability and orientation hypotheses are available.
6. appendix.tex:248-252 drops the LSI part from the residual exponential using C_LSI(u)>=0 and dot{s}(u)>0; this remains an internal paper step plus interval-integral monotonicity obligation.

leanStepMap : List String (explicit)

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

Ordered data items

1. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract unchanged.
2. Route the lower target through SALD.forwardKlGronwallSideConditionContract and SALD.forwardKlGronwallSideConditionObligation, not a new theorem statement.
3. Treat a(t) as the difference of the LSI coefficient and alpha coefficient; lower work may expose integrability for the pieces before assembling the Gronwall coefficient.
4. Treat b(t) as a product of dot{s}(t)^(-1) and E_alpha(pi_t,v_t); finite-log-mgf and measurability still come from the DV witness and alpha-complexity obligations.
5. Use SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces only for the exponent-congruence substep after the LSI and alpha coefficient pieces have adjacent interval-integrability; it delegates to SALD.gronwallExpProductRewriteIntegralCongr.
6. Keep endpoint rewrites K(0)/K(T), residual-exponent monotonicity, DV, LSI-to-KL/FI, the KL derivative, and full Gronwall as separate obligations unless a compiled proof is added.

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; cycle 22 only records its coefficient output.
2. eq:LSI-KL-FI remains the local density-test obligation that supplies the LSI contraction coefficient.
3. lem:gronwall remains the local real-analysis obligation; SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces and SALD.gronwallExpProductRewriteIntegralCongr are only compiled sublemmas for the final exponent algebra.
4. No SLT theorem is imported or marked formalized for coefficient regularity, adjacent interval-integrability, endpoint rewrites, 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.coefficient_chain_audit
3. sald.forward_kl.endpoint_schedule_identities
4. sald.forward_kl.dv_finite_log_mgf_witness
5. sald.forward_kl.kl_derivative
6. probability.lsi_to_kl_fi
7. sald.gronwall.exponent_rewrite
8. sald.gronwall.integrating_factor
9. SALD.forwardKlGronwallSideConditionObligation
10. SALD.forwardKlGronwallApplicationObligation
11. SALD.forwardKlDvFiniteLogMgfWitnessObligation
12. 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. First prove or refine only the coefficient regularity and adjacent interval-integrability needed for dot{s}(t)*C_LSI(t), (1/2)*dot{s}(t)^(-1)*alpha^(-1), and b(t); the a(t) interval-integrability is assembled by SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable.
3. After those hypotheses are exposed, connect the theorem-specific exponent split to SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces without changing the signs, endpoint limits, or source coefficients.
4. Leave endpoint K(0)/K(T) rewrites, residual exponent drop, DV finite-log-mgf, LSI density-test, KL derivative, and full Gronwall in their existing obligations unless a separate compiled 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.cycle22ForwardKlMiddleContract in the Gronwall side-condition block.
2. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle22ForwardKlMiddleContract while retaining cycle-14 and cycle-18 packets.
3. The conversion window, proof-obligation ledger, and SLT audit identify cycle 22 middle as source-to-Lean synchronization for coefficient regularity, 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 beyond obligation or source-cited status.

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 cycle22ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Translate the cycle-22 upper target into a lower-ready map for sald.forward_kl.gronwall_side_conditions: prove or isolate theorem-specific regularity and adjacent interval-integrability for the LSI and alpha pieces of a(t), and for b(t), before applying SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces."
  sourceStepMap := [
    "appendix.tex:210-217 supplies the nonnegative LSI part of a(t), namely dot{s}(t)*C_LSI(t), after the LSI-to-KL/FI bridge.",
    "appendix.tex:218-228 supplies the inverse-schedule rewrite that turns the velocity coefficient into dot{s}(t)^(-1).",
    "appendix.tex:230-241 supplies the DV alpha contribution (1/2)*dot{s}(t)^(-1)*alpha^(-1) to a(t) and the source b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t).",
    "appendix.tex:244-248 applies lem:gronwall to K(t)=KL(rho_{s(t)}||pi_t) with exactly those a(t) and b(t); continuity or interval-integrability is implicit in the paper and must be exposed locally.",
    "appendix.tex:249-250 splits the initial exponent into the LSI contraction factor and alpha factor; the compiled outer-integral congruence is applicable only after adjacent interval-integrability and orientation hypotheses are available.",
    "appendix.tex:248-252 drops the LSI part from the residual exponential using C_LSI(u)>=0 and dot{s}(u)>0; this remains an internal paper step plus interval-integral monotonicity obligation."
  ]
  leanStepMap := [
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract unchanged.",
    "Route the lower target through SALD.forwardKlGronwallSideConditionContract and SALD.forwardKlGronwallSideConditionObligation, not a new theorem statement.",
    "Treat a(t) as the difference of the LSI coefficient and alpha coefficient; lower work may expose integrability for the pieces before assembling the Gronwall coefficient.",
    "Treat b(t) as a product of dot{s}(t)^(-1) and E_alpha(pi_t,v_t); finite-log-mgf and measurability still come from the DV witness and alpha-complexity obligations.",
    "Use SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces only for the exponent-congruence substep after the LSI and alpha coefficient pieces have adjacent interval-integrability; it delegates to SALD.gronwallExpProductRewriteIntegralCongr.",
    "Keep endpoint rewrites K(0)/K(T), residual-exponent monotonicity, DV, LSI-to-KL/FI, the KL derivative, and full Gronwall as separate obligations unless a compiled proof is added."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through Boucheron Cor. 4.15 or a future local entropy-duality port; cycle 22 only records its coefficient output.",
    "eq:LSI-KL-FI remains the local density-test obligation that supplies the LSI contraction coefficient.",
    "lem:gronwall remains the local real-analysis obligation; SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces and SALD.gronwallExpProductRewriteIntegralCongr are only compiled sublemmas for the final exponent algebra.",
    "No SLT theorem is imported or marked formalized for coefficient regularity, adjacent interval-integrability, endpoint rewrites, or residual-exponent monotonicity."
  ]
  obligations := [
    "sald.forward_kl.gronwall_side_conditions",
    "sald.forward_kl.coefficient_chain_audit",
    "sald.forward_kl.endpoint_schedule_identities",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.kl_derivative",
    "probability.lsi_to_kl_fi",
    "sald.gronwall.exponent_rewrite",
    "sald.gronwall.integrating_factor",
    "SALD.forwardKlGronwallSideConditionObligation",
    "SALD.forwardKlGronwallApplicationObligation",
    "SALD.forwardKlDvFiniteLogMgfWitnessObligation",
    "SALD.lsiKlFiDensityTestObligation"
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.",
    "First prove or refine only the coefficient regularity and adjacent interval-integrability needed for dot{s}(t)*C_LSI(t), (1/2)*dot{s}(t)^(-1)*alpha^(-1), and b(t); the a(t) interval-integrability is assembled by SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable.",
    "After those hypotheses are exposed, connect the theorem-specific exponent split to SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces without changing the signs, endpoint limits, or source coefficients.",
    "Leave endpoint K(0)/K(T) rewrites, residual exponent drop, DV finite-log-mgf, LSI density-test, KL derivative, and full Gronwall in their existing obligations unless a separate compiled proof is added."
  ]
  reviewerChecklist := [
    "SALD.forwardKlProofDag lists SALD.cycle22ForwardKlMiddleContract in the Gronwall side-condition block.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle22ForwardKlMiddleContract while retaining cycle-14 and cycle-18 packets.",
    "The conversion window, proof-obligation ledger, and SLT audit identify cycle 22 middle as source-to-Lean synchronization for coefficient regularity, 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 beyond obligation or source-cited status."
  ]
  status := ProofStatus.obligation

/-- Cycle-26 upper packet for the continuous forward-KL DV witness.

This returns to `thm:forward-KL` after the first-appendix cycle-25 PI work and
selects only the theorem-specific Donsker--Varadhan finite-log-mgf/common-space
witness as the next lower target.  It preserves the existing Gronwall
coefficient work from cycle 22 as a dependency and does not promote DV,
LSI-to-KL/FI, the KL derivative, or Gronwall to formalized status.
-/