AutoSamplingTheory.SALD.cycle23DiscreteForwardKlUpperPacket

Data definition / provenance and workflow record

Meaning and type

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

def cycle23DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket

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.

Rebaseline thm:forward-KL-discrete across the Euler-Maruyama interpolation, one-step frozen score defect, and accumulated-error bridge, then choose the coefficient-chain audit as the single lower target for this cycle.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL-discrete
2. eq:frozen_interp_terminal_disc_prop_additive_final
3. lem:frozen_delta_cross_lip_sald
4. proof:thm:forward-KL-discrete:em-interpolation
5. proof:thm:forward-KL-discrete:one-step-defects
6. proof:thm:forward-KL-discrete:accumulated-error
7. lem:dv_variation
8. lem:gronwall

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use only main_body.tex:273-323 and appendix.tex:260-592 from the original source root, with sald_version_2.tex excluded.
2. Preserve the source theorem statement, linear slowdown t(s)=s/r, step-size condition 4*eta^2*L_{pi,space}^2<1/2, alpha ranges, Gamma/Delta definitions, and barGamma/barDelta accumulated constants.
3. Keep the proof route EM interval laws -> conditional Fokker-Planck -> frozen defect and Young/LSI -> DV velocity -> time change -> Gronwall -> linear-slowdown collection.
4. Treat EM Fokker-Planck, omitted SALD frozen-defect proof, LSI-to-KL/FI, DV, Gronwall, endpoint stitching, coefficient integrability, and interval-integral monotonicity as obligations or source-cited facts until local Lean proofs replace them.
5. Middle must keep AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, research-wiki/source-index/SALD_original.jsonl, and the cited TeX windows synchronized in both directions.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not prove or restate thm:forward-KL-discrete in this packet.
2. Do not reopen the continuous forward-KL theorem except as an inherited dependency.
3. Do not replace the paper's one-step frozen-defect route with a path-space, Girsanov, Pinsker, Talagrand, or alternative entropy route.
4. Do not change Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, r, or the source Lipschitz and exponential-moment assumptions.
5. Do not promote lem:dv_variation, lem:gronwall, eq:LSI-KL-FI, the EM Fokker-Planck backend, or the omitted frozen-defect proof beyond their current statuses.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.discreteForwardKlCoefficientChainAuditContract / SALD.discreteForwardKlCoefficientChainObligation / sald.discrete_forward_kl.coefficient_chain_audit.
2. First lower sub-slice: audit appendix.tex:454-553, including the two 1/4*FI cross-term bounds, LSI conversion, DV coefficient dot{t}(s)^2*alpha^(-1), and the time-change rewrite to dot{s}(t)^(-1)*alpha^(-1).
3. Second sub-slice only if the first is stable: connect appendix.tex:557-590 to main_body.tex:309-323 through endpoint stitching, residual exponent drop, and full-interval A_alpha, barGamma, and barDelta collection.
4. Keep EM endpoint laws, conditional Fokker-Planck, frozen Gamma/Delta lemma, DV witness, and Gronwall as named dependencies; if one is missing, refine the corresponding ProofObligation instead of adding a theorem hypothesis.
5. Do not bundle the EM interpolation, one-step defect, Gronwall accumulation, and final theorem display into one opaque assumption.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle23_upper_packet before the coefficient-chain audit block.
2. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle23DiscreteForwardKlUpperPacket while retaining the cycle-15 and cycle-19 packets.
3. The conversion window and proof-obligation ledger cite main_body.tex:273-323 and appendix.tex:260-592, and the source index still excludes sald_version_2.tex.
4. SALD.discreteForwardKlCoefficientChainAuditContract preserves the source coefficients T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.
5. No analytic dependency is marked formalized and no fake proof closure is introduced.

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 cycle23DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket where
  objective := "Rebaseline thm:forward-KL-discrete across the Euler-Maruyama interpolation, one-step frozen score defect, and accumulated-error bridge, then choose the coefficient-chain audit as the single lower target for this cycle."
  sourceLabels := [
    "thm:forward-KL-discrete",
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:frozen_delta_cross_lip_sald",
    "proof:thm:forward-KL-discrete:em-interpolation",
    "proof:thm:forward-KL-discrete:one-step-defects",
    "proof:thm:forward-KL-discrete:accumulated-error",
    "lem:dv_variation",
    "lem:gronwall"
  ]
  modeDiscipline := [
    "faithfulPaper: use only main_body.tex:273-323 and appendix.tex:260-592 from the original source root, with sald_version_2.tex excluded.",
    "Preserve the source theorem statement, linear slowdown t(s)=s/r, step-size condition 4*eta^2*L_{pi,space}^2<1/2, alpha ranges, Gamma/Delta definitions, and barGamma/barDelta accumulated constants.",
    "Keep the proof route EM interval laws -> conditional Fokker-Planck -> frozen defect and Young/LSI -> DV velocity -> time change -> Gronwall -> linear-slowdown collection.",
    "Treat EM Fokker-Planck, omitted SALD frozen-defect proof, LSI-to-KL/FI, DV, Gronwall, endpoint stitching, coefficient integrability, and interval-integral monotonicity as obligations or source-cited facts until local Lean proofs replace them.",
    "Middle must keep AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, research-wiki/source-index/SALD_original.jsonl, and the cited TeX windows synchronized in both directions."
  ]
  nonGoals := [
    "Do not prove or restate thm:forward-KL-discrete in this packet.",
    "Do not reopen the continuous forward-KL theorem except as an inherited dependency.",
    "Do not replace the paper's one-step frozen-defect route with a path-space, Girsanov, Pinsker, Talagrand, or alternative entropy route.",
    "Do not change Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, r, or the source Lipschitz and exponential-moment assumptions.",
    "Do not promote lem:dv_variation, lem:gronwall, eq:LSI-KL-FI, the EM Fokker-Planck backend, or the omitted frozen-defect proof beyond their current statuses."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.discreteForwardKlCoefficientChainAuditContract / SALD.discreteForwardKlCoefficientChainObligation / sald.discrete_forward_kl.coefficient_chain_audit.",
    "First lower sub-slice: audit appendix.tex:454-553, including the two 1/4*FI cross-term bounds, LSI conversion, DV coefficient dot{t}(s)^2*alpha^(-1), and the time-change rewrite to dot{s}(t)^(-1)*alpha^(-1).",
    "Second sub-slice only if the first is stable: connect appendix.tex:557-590 to main_body.tex:309-323 through endpoint stitching, residual exponent drop, and full-interval A_alpha, barGamma, and barDelta collection.",
    "Keep EM endpoint laws, conditional Fokker-Planck, frozen Gamma/Delta lemma, DV witness, and Gronwall as named dependencies; if one is missing, refine the corresponding ProofObligation instead of adding a theorem hypothesis.",
    "Do not bundle the EM interpolation, one-step defect, Gronwall accumulation, and final theorem display into one opaque assumption."
  ]
  reviewerChecklist := [
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle23_upper_packet before the coefficient-chain audit block.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle23DiscreteForwardKlUpperPacket while retaining the cycle-15 and cycle-19 packets.",
    "The conversion window and proof-obligation ledger cite main_body.tex:273-323 and appendix.tex:260-592, and the source index still excludes sald_version_2.tex.",
    "SALD.discreteForwardKlCoefficientChainAuditContract preserves the source coefficients T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-23 middle packet for the discrete forward-KL coefficient chain.

This translates the upper-selected coefficient audit into a lower-ready
source-to-Lean map.  It keeps the first lower slice on appendix lines 454-553
and leaves the endpoint/accumulated-error bridge as a separate follow-on slice.
-/