AutoSamplingTheory.SALD.cycle22ForwardKlUpperPacket

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 cycle22ForwardKlUpperPacket : 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.

Keep continuous thm:forward-KL fixed and assign the next lower work to the theorem-specific Gronwall side-condition bridge: coefficient regularity and adjacent interval-integrability for the source a(t), b(t), and exponent pieces, reusing SALD.gronwallExpProductRewriteIntegralCongr only as a local algebra substep.

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, appendix.tex:210-252, and the Gronwall exponent-rewrite source window appendix.tex:63-69 from the original source root; sald_version_2.tex remains excluded.
2. Preserve the source theorem statement, the differential inequality after DV, the Gronwall 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), and the two-term display in main_body.tex:243-246.
3. Treat SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces and SALD.gronwallExpProductRewriteIntegralCongr as compiled local interval-integral algebra only. The theorem still owes piecewise coefficient regularity, endpoint rewrites, residual-exponent monotonicity, KL derivative, DV finite-log-mgf, LSI-to-KL/FI, and full Gronwall backends.

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 source route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, PI-to-LSI, the general moving-target theorem, or any alternate comparison method.
3. Do not add endpoint, positivity, density, boundary, finite-log-mgf, absolute-continuity, differentiability, continuity, 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, endpoint schedule identities, or residual-exponent drop 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. First lower sub-slice: expose the theorem-specific regularity and adjacent interval-integrability hypotheses for the LSI part dot{s}(t)*C_LSI(t), alpha part (1/2)*dot{s}(t)^(-1)*alpha^(-1), and b(t); SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable now assembles the a(t) interval-integrability from the two coefficient pieces.
3. Classify blockers explicitly: local-lemma for interval-integral additivity/congruence, source-contract-gap for coefficient regularity and endpoint schedule identities, and internal-paper-step for the residual LSI exponent drop.
4. Keep DV finite-log-mgf, LSI density-test, KL derivative, endpoint K(0)/K(T) rewrites, and the full Gronwall lemma 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 routes ASTIS.SALD.forward_KL.gronwall_side_conditions through SALD.cycle22ForwardKlUpperPacket while retaining cycle-14 and cycle-18 packets.
2. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle22ForwardKlUpperPacket and still lists the compiled Gronwall scalar/interval helpers plus the forward-KL coefficient assembly lemmas only as dependencies.
3. The conversion window and proof-obligation ledger identify cycle 22 as a faithful upper packet for coefficient regularity and interval-integrability, not as a proof of thm:forward-KL.
4. SALD_original.jsonl 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 cycle22ForwardKlUpperPacket : ForwardKlUpperPacket where
  objective := "Keep continuous thm:forward-KL fixed and assign the next lower work to the theorem-specific Gronwall side-condition bridge: coefficient regularity and adjacent interval-integrability for the source a(t), b(t), and exponent pieces, reusing SALD.gronwallExpProductRewriteIntegralCongr only as a local algebra substep."
  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, appendix.tex:210-252, and the Gronwall exponent-rewrite source window appendix.tex:63-69 from the original source root; sald_version_2.tex remains excluded.",
    "Preserve the source theorem statement, the differential inequality after DV, the Gronwall 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), and the two-term display in main_body.tex:243-246.",
    "Treat SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces and SALD.gronwallExpProductRewriteIntegralCongr as compiled local interval-integral algebra only. The theorem still owes piecewise coefficient regularity, endpoint rewrites, residual-exponent monotonicity, KL derivative, DV finite-log-mgf, LSI-to-KL/FI, and full Gronwall backends."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL in this packet.",
    "Do not replace the source route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, PI-to-LSI, the general moving-target theorem, or any alternate comparison method.",
    "Do not add endpoint, positivity, density, boundary, finite-log-mgf, absolute-continuity, differentiability, continuity, or interval-integrability assumptions silently to the theorem statement.",
    "Do not mark lem:gronwall, lem:dv_variation, eq:LSI-KL-FI, the KL derivative, endpoint schedule identities, or residual-exponent drop formalized."
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.",
    "First lower sub-slice: expose the theorem-specific regularity and adjacent interval-integrability hypotheses for the LSI part dot{s}(t)*C_LSI(t), alpha part (1/2)*dot{s}(t)^(-1)*alpha^(-1), and b(t); SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable now assembles the a(t) interval-integrability from the two coefficient pieces.",
    "Classify blockers explicitly: local-lemma for interval-integral additivity/congruence, source-contract-gap for coefficient regularity and endpoint schedule identities, and internal-paper-step for the residual LSI exponent drop.",
    "Keep DV finite-log-mgf, LSI density-test, KL derivative, endpoint K(0)/K(T) rewrites, and the full Gronwall lemma in their existing obligations unless a separate compiled proof is added."
  ]
  reviewerChecklist := [
    "SALD.forwardKlProofDag routes ASTIS.SALD.forward_KL.gronwall_side_conditions through SALD.cycle22ForwardKlUpperPacket while retaining cycle-14 and cycle-18 packets.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle22ForwardKlUpperPacket and still lists the compiled Gronwall scalar/interval helpers plus the forward-KL coefficient assembly lemmas only as dependencies.",
    "The conversion window and proof-obligation ledger identify cycle 22 as a faithful upper packet for coefficient regularity and interval-integrability, not as a proof of thm:forward-KL.",
    "SALD_original.jsonl 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-22 middle packet for the continuous forward-KL coefficient bridge.

This converts the upper coefficient-regularity objective into a lower-ready
source-to-Lean map.  The packet is deliberately narrower than the full
`thm:forward-KL` proof: it only audits the Gronwall coefficients and the
adjacent interval-integrability needed before the compiled exponent congruence
can be used in the theorem display.
-/