AutoSamplingTheory.SALD.cycle26ForwardKlUpperPacket

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 cycle26ForwardKlUpperPacket : 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 theorem-specific DV finite-log-mgf/common-space witness for Z=alpha*||v_t||^2 as the next lower target, while preserving the existing derivative -> LSI -> DV -> Gronwall chain and the cycle-22 Gronwall coefficient side-condition work.

sourceLabels : List String (explicit)

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

Ordered data items

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

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use main_body.tex:218-248 and appendix.tex:73-79, 164-252 from the original source root; sald_version_2.tex remains excluded.
2. Keep the theorem statement fixed: finite E_alpha0(pi_t,v_t), alpha in (0,alpha0], the transport velocity v_t of pi_t, and the terminal KL display in main_body.tex:243-246 are not changed.
3. Preserve the DV instantiation exactly: nu=rho_{s(t)}, mu=pi_t, Z=alpha*||v_t||^2, with the source coefficient alpha^(-1) and the downstream Gronwall coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1).
4. Treat lem:dv_variation as source-cited, the alpha0-to-alpha finite-log-mgf bridge as a local obligation, and LSI-to-KL/FI, KL derivative, schedule calculus, coefficient regularity, and full Gronwall as separate obligations.

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 derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, PI-to-LSI, path-space comparison, or the general moving-target theorem.
3. Do not add finite-log-mgf, absolute-continuity, common-space, endpoint, positivity, differentiability, or integrability assumptions silently to the theorem statement.
4. Do not import or mark an SLT entropy-duality theorem formalized; SLT remains a reference pattern until a local port builds.
5. Do not reopen the cycle-22 Gronwall coefficient assembly except as a dependency of the final theorem display.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.forwardKlDvFiniteLogMgfWitnessContract / SALD.forwardKlDvFiniteLogMgfWitnessObligation / sald.forward_kl.dv_finite_log_mgf_witness.
2. First lower sub-slice: expose the common state space, absolute-continuity relationship, measurability of ||v_t||^2, and finite log-mgf needed to apply lem:dv_variation with Z=alpha*||v_t||^2.
3. Use SALD.forwardKlDvAlphaMonotonicityContract only for the alpha0-to-alpha finite-log-mgf bridge; if the monotonicity/order backend is blocked, record that backend as the lower obligation rather than adding a theorem assumption.
4. Preserve positive-alpha scaling when dividing the DV inequality by alpha and keep the downstream coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1) unchanged.
5. Leave LSI density-test, KL derivative, endpoint schedule identities, Gronwall side conditions, residual exponent drop, and full Gronwall in their existing obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle26ForwardKlUpperPacket while retaining cycle-14, cycle-18, and cycle-22 packets.
2. SALD.forwardKlProofDag routes ASTIS.SALD.forward_KL.dv_finite_log_mgf_witness through SALD.cycle26ForwardKlUpperPacket before the DV-energy block.
3. SALD.forwardKlDvFiniteLogMgfWitnessObligation remains an obligation and depends on SALD.forwardKlDvAlphaMonotonicityContract plus the source-cited DV interface; no theorem assumption is added.
4. The conversion window, proof-obligation ledger, and SLT audit classify cycle 26 as upper workflow/source-dependency refinement, not as a proof of DV or thm:forward-KL.
5. SALD_original.jsonl indexes thm:forward-KL, def:alpha-complexity, lem:dv_variation, eq:LSI-KL-FI, and lem:gronwall while excluding sald_version_2.tex.
6. 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 cycle26ForwardKlUpperPacket : ForwardKlUpperPacket where
  objective := "Return to continuous thm:forward-KL and select the theorem-specific DV finite-log-mgf/common-space witness for Z=alpha*||v_t||^2 as the next lower target, while preserving the existing derivative -> LSI -> DV -> Gronwall chain and the cycle-22 Gronwall coefficient side-condition work."
  sourceLabels := [
    "thm:forward-KL",
    "def:alpha-complexity",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "lem:gronwall",
    "eq:SALD",
    "eq:FP-eq"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:218-248 and appendix.tex:73-79, 164-252 from the original source root; sald_version_2.tex remains excluded.",
    "Keep the theorem statement fixed: finite E_alpha0(pi_t,v_t), alpha in (0,alpha0], the transport velocity v_t of pi_t, and the terminal KL display in main_body.tex:243-246 are not changed.",
    "Preserve the DV instantiation exactly: nu=rho_{s(t)}, mu=pi_t, Z=alpha*||v_t||^2, with the source coefficient alpha^(-1) and the downstream Gronwall coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1).",
    "Treat lem:dv_variation as source-cited, the alpha0-to-alpha finite-log-mgf bridge as a local obligation, and LSI-to-KL/FI, KL derivative, schedule calculus, coefficient regularity, and full Gronwall as separate obligations."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL in this packet.",
    "Do not replace the paper route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, PI-to-LSI, path-space comparison, or the general moving-target theorem.",
    "Do not add finite-log-mgf, absolute-continuity, common-space, endpoint, positivity, differentiability, or integrability assumptions silently to the theorem statement.",
    "Do not import or mark an SLT entropy-duality theorem formalized; SLT remains a reference pattern until a local port builds.",
    "Do not reopen the cycle-22 Gronwall coefficient assembly except as a dependency of the final theorem display."
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlDvFiniteLogMgfWitnessContract / SALD.forwardKlDvFiniteLogMgfWitnessObligation / sald.forward_kl.dv_finite_log_mgf_witness.",
    "First lower sub-slice: expose the common state space, absolute-continuity relationship, measurability of ||v_t||^2, and finite log-mgf needed to apply lem:dv_variation with Z=alpha*||v_t||^2.",
    "Use SALD.forwardKlDvAlphaMonotonicityContract only for the alpha0-to-alpha finite-log-mgf bridge; if the monotonicity/order backend is blocked, record that backend as the lower obligation rather than adding a theorem assumption.",
    "Preserve positive-alpha scaling when dividing the DV inequality by alpha and keep the downstream coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1) unchanged.",
    "Leave LSI density-test, KL derivative, endpoint schedule identities, Gronwall side conditions, residual exponent drop, and full Gronwall in their existing obligations."
  ]
  reviewerChecklist := [
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle26ForwardKlUpperPacket while retaining cycle-14, cycle-18, and cycle-22 packets.",
    "SALD.forwardKlProofDag routes ASTIS.SALD.forward_KL.dv_finite_log_mgf_witness through SALD.cycle26ForwardKlUpperPacket before the DV-energy block.",
    "SALD.forwardKlDvFiniteLogMgfWitnessObligation remains an obligation and depends on SALD.forwardKlDvAlphaMonotonicityContract plus the source-cited DV interface; no theorem assumption is added.",
    "The conversion window, proof-obligation ledger, and SLT audit classify cycle 26 as upper workflow/source-dependency refinement, not as a proof of DV or thm:forward-KL.",
    "SALD_original.jsonl indexes thm:forward-KL, def:alpha-complexity, lem:dv_variation, eq:LSI-KL-FI, 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 middle packet for the continuous forward-KL DV witness.

This converts the upper-selected finite-log-mgf/common-space target into a
lower-ready source-to-Lean map.  It does not prove the Donsker--Varadhan
formula, the exponential-moment monotonicity bridge, or `thm:forward-KL`.
-/