AutoSamplingTheory.SALD.cycle18ForwardKlUpperPacket

Data definition / provenance and workflow record

Meaning and type

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

def cycle18ForwardKlUpperPacket : ForwardKlUpperPacket

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.

objective : String (explicit)

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

Return to continuous thm:forward-KL and select the final Gronwall/DV/LSI dependency chain as the next faithful lower target, reusing the cycle-17 scalar exponent algebra only as local bookkeeping inside sald.forward_kl.gronwall_side_conditions.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL
2. eq:SALD
3. eq:FP-eq
4. eq:LSI-KL-FI
5. def:alpha-complexity
6. lem:dv_variation
7. lem:gronwall

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use main_body.tex:238-247 and appendix.tex:164-252 from the original source root, with sald_version_2.tex excluded.
2. Keep the theorem statement fixed: LSI constants C_LSI(t)>=0, finite alpha0-complexity for the transport velocity v_t, alpha in (0,alpha0], and the two-term terminal KL display in main_body.tex:243-246.
3. Preserve the source route derivative -> LSI -> DV -> Gronwall and the coefficients 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).
4. Treat the cycle-17 scalar Gronwall lemmas and cycle-18 adjacent-interval bridge as partial local algebra only; theorem-specific interval-integrability, coefficient regularity, endpoint rewrites, DV finite-log-mgf, LSI-to-KL/FI, and KL derivative remain obligations or source-cited facts.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not restate or prove thm:forward-KL in this packet.
2. Do not replace the paper route with Pinsker, Talagrand, Girsanov, path-space comparison, PI-to-LSI, or a generalized moving-target theorem.
3. Do not add endpoint, positivity, density, boundary, finite-log-mgf, absolute-continuity, differentiability, or interval-integrability assumptions silently to the theorem statement.
4. Do not mark lem:gronwall, lem:dv_variation, eq:LSI-KL-FI, the KL derivative, or the moving-target dependency chain formalized.

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. Refine only the final Gronwall side-condition ledger: endpoint K(0)/K(T) rewrites, coefficient regularity for a(t), b(t), exponent split, residual LSI exponent drop, and how the cycle-17 scalar Real.exp helpers fit after adjacent-interval additivity.
3. Keep the DV slice as SALD.forwardKlDvFiniteLogMgfWitnessContract and the LSI slice as SALD.saldLsiKlFiDensityTestContract; do not prove or rewrite those backends in the same lower attempt.
4. If interval-integral additivity or residual exponent monotonicity is not ready, refine the named obligation instead of changing the theorem display.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract remains contractOnly and still lists the forward-KL moving-target, derivative, DV, coefficient-chain, Gronwall-side-condition, and Gronwall application obligations.
2. SALD.forwardKlProofDag routes thm:forward-KL through moving_target_dependencies, coefficient_chain_audit, dv_energy, and gronwall_side_conditions, with cycle-17 scalar Gronwall helpers and the cycle-18 adjacent-interval bridge recorded only as local dependencies.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle18ForwardKlUpperPacket without removing SALD.cycle14ForwardKlUpperPacket or SALD.cycle14ForwardKlMiddleContract.
4. The source index contains thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall, and sald_version_2.tex remains excluded.
5. No fake proof closure appears and no analytic dependency is promoted beyond its current obligation/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 cycle18ForwardKlUpperPacket : ForwardKlUpperPacket where
  objective := "Return to continuous thm:forward-KL and select the final Gronwall/DV/LSI dependency chain as the next faithful lower target, reusing the cycle-17 scalar exponent algebra only as local bookkeeping inside sald.forward_kl.gronwall_side_conditions."
  sourceLabels := [
    "thm:forward-KL",
    "eq:SALD",
    "eq:FP-eq",
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:238-247 and appendix.tex:164-252 from the original source root, with sald_version_2.tex excluded.",
    "Keep the theorem statement fixed: LSI constants C_LSI(t)>=0, finite alpha0-complexity for the transport velocity v_t, alpha in (0,alpha0], and the two-term terminal KL display in main_body.tex:243-246.",
    "Preserve the source route derivative -> LSI -> DV -> Gronwall and the coefficients 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).",
    "Treat the cycle-17 scalar Gronwall lemmas and cycle-18 adjacent-interval bridge as partial local algebra only; theorem-specific interval-integrability, coefficient regularity, endpoint rewrites, DV finite-log-mgf, LSI-to-KL/FI, and KL derivative remain obligations or source-cited facts."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL in this packet.",
    "Do not replace the paper route with Pinsker, Talagrand, Girsanov, path-space comparison, PI-to-LSI, or a generalized moving-target theorem.",
    "Do not add endpoint, positivity, density, boundary, finite-log-mgf, absolute-continuity, differentiability, or interval-integrability assumptions silently to the theorem statement.",
    "Do not mark lem:gronwall, lem:dv_variation, eq:LSI-KL-FI, the KL derivative, or the moving-target dependency chain formalized."
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.",
    "Refine only the final Gronwall side-condition ledger: endpoint K(0)/K(T) rewrites, coefficient regularity for a(t), b(t), exponent split, residual LSI exponent drop, and how the cycle-17 scalar Real.exp helpers fit after adjacent-interval additivity.",
    "Keep the DV slice as SALD.forwardKlDvFiniteLogMgfWitnessContract and the LSI slice as SALD.saldLsiKlFiDensityTestContract; do not prove or rewrite those backends in the same lower attempt.",
    "If interval-integral additivity or residual exponent monotonicity is not ready, refine the named obligation instead of changing the theorem display."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract remains contractOnly and still lists the forward-KL moving-target, derivative, DV, coefficient-chain, Gronwall-side-condition, and Gronwall application obligations.",
    "SALD.forwardKlProofDag routes thm:forward-KL through moving_target_dependencies, coefficient_chain_audit, dv_energy, and gronwall_side_conditions, with cycle-17 scalar Gronwall helpers and the cycle-18 adjacent-interval bridge recorded only as local dependencies.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle18ForwardKlUpperPacket without removing SALD.cycle14ForwardKlUpperPacket or SALD.cycle14ForwardKlMiddleContract.",
    "The source index contains thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall, and sald_version_2.tex remains excluded.",
    "No fake proof closure appears and no analytic dependency is promoted beyond its current obligation/source-cited status."
  ]
  status := ProofStatus.obligation

/-- Cycle-18 middle packet for the continuous forward-KL Gronwall side conditions.

This refines the upper packet into a lower-ready source-to-Lean map for the
last Gronwall display of `thm:forward-KL`.  It records how the accepted
cycle-17 scalar Gronwall algebra can be reused only after the interval-integral
side conditions have produced the required scalar equalities.
-/