AutoSamplingTheory.SALD.cycle19DiscreteForwardKlUpperPacket

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

Keep thm:forward-KL-discrete fixed and select the accumulated-error bridge as the next lower target: endpoint rewrites after the EM interpolation, the linear-slowdown exponent split, the residual exponent bound, and the A_alpha/barGamma/barDelta collection from appendix.tex:557-590 to main_body.tex:309-323.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL-discrete
2. proof:thm:forward-KL-discrete:gronwall
3. proof:thm:forward-KL-discrete:accumulated-error
4. proof:thm:forward-KL-discrete:coefficient-chain
5. lem:gronwall
6. def:alpha-complexity
7. eq:frozen_interp_terminal_disc_prop_additive_final

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use main_body.tex:299-323 and appendix.tex:526-592 from the original source root, with sald_version_2.tex excluded.
2. Preserve the source theorem statement, the linear slowdown t(s)=s/r with r>=1, the appendix Gronwall coefficients a(t)=dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t) and b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t)+2*dot{s}(t)*eta*Delta(t), and the main-body constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.
3. Treat EM endpoint laws, stitched-interval regularity, coefficient integrability, residual-exponent monotonicity, barGamma/barDelta integral identifications, and Gronwall as obligations or source-cited facts until local Lean proofs replace them.
4. Classify the blocked lower scalar bridge as local real/integral algebra plus source-contract gaps; do not import or mark any SLT result formalized for this packet.

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-discrete in this packet.
2. Do not reopen the conditional Fokker--Planck, frozen one-step Gamma/Delta, LSI, or DV velocity subproofs except as dependencies of the accumulated-error bridge.
3. Do not alter Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, r, the source step-size condition, or the theorem's open alpha range.
4. Do not hide endpoint rewrites, residual-exponent monotonicity, or A_alpha/Gamma/Delta integral collection as a new theorem assumption.
5. Do not replace the source route EM interval inequalities -> Gronwall -> linear-slowdown collection with a path-space, Girsanov, Pinsker, Talagrand, or different entropy route.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.
2. Preferred first lower sub-slice: SALD.discreteForwardKlResidualExponentBoundObligation, proving only the residual exponent drop and full-interval Gamma bound used inside the accumulated-error bridge.
3. Keep the appendix Gronwall display from appendix.tex:557-590 separate from the main-body theorem display in main_body.tex:309-323; bridge them by explicit endpoint, exponent, and integral-collection steps.
4. If endpoint law matching, stitched interval regularity, coefficient integrability, or interval-integral monotonicity is blocked, record the precise source-contract gap rather than weakening the theorem statement.
5. Do not bundle the one-step frozen defect, DV witness, Gronwall accumulation, residual exponent bound, and final accumulated-error collection 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.cycle19_upper_packet before the linear-slowdown, residual-exponent, and accumulated-error blocks.
2. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle19DiscreteForwardKlUpperPacket while retaining the cycle-15 EM packets and all existing discrete obligations.
3. SALD.discreteForwardKlAccumulatedErrorBridgeContract still uses appendix.tex:557-590 and main_body.tex:309-323, with the source a(t), b(t), barGamma, and barDelta constants unchanged.
4. The conversion window and proof-obligation ledger classify the cycle-19 packet as workflow/obligation data, not a proof of thm:forward-KL-discrete.
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 cycle19DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket where
  objective := "Keep thm:forward-KL-discrete fixed and select the accumulated-error bridge as the next lower target: endpoint rewrites after the EM interpolation, the linear-slowdown exponent split, the residual exponent bound, and the A_alpha/barGamma/barDelta collection from appendix.tex:557-590 to main_body.tex:309-323."
  sourceLabels := [
    "thm:forward-KL-discrete",
    "proof:thm:forward-KL-discrete:gronwall",
    "proof:thm:forward-KL-discrete:accumulated-error",
    "proof:thm:forward-KL-discrete:coefficient-chain",
    "lem:gronwall",
    "def:alpha-complexity",
    "eq:frozen_interp_terminal_disc_prop_additive_final"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:299-323 and appendix.tex:526-592 from the original source root, with sald_version_2.tex excluded.",
    "Preserve the source theorem statement, the linear slowdown t(s)=s/r with r>=1, the appendix Gronwall coefficients a(t)=dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t) and b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t)+2*dot{s}(t)*eta*Delta(t), and the main-body constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.",
    "Treat EM endpoint laws, stitched-interval regularity, coefficient integrability, residual-exponent monotonicity, barGamma/barDelta integral identifications, and Gronwall as obligations or source-cited facts until local Lean proofs replace them.",
    "Classify the blocked lower scalar bridge as local real/integral algebra plus source-contract gaps; do not import or mark any SLT result formalized for this packet."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL-discrete in this packet.",
    "Do not reopen the conditional Fokker--Planck, frozen one-step Gamma/Delta, LSI, or DV velocity subproofs except as dependencies of the accumulated-error bridge.",
    "Do not alter Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, r, the source step-size condition, or the theorem's open alpha range.",
    "Do not hide endpoint rewrites, residual-exponent monotonicity, or A_alpha/Gamma/Delta integral collection as a new theorem assumption.",
    "Do not replace the source route EM interval inequalities -> Gronwall -> linear-slowdown collection with a path-space, Girsanov, Pinsker, Talagrand, or different entropy route."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.",
    "Preferred first lower sub-slice: SALD.discreteForwardKlResidualExponentBoundObligation, proving only the residual exponent drop and full-interval Gamma bound used inside the accumulated-error bridge.",
    "Keep the appendix Gronwall display from appendix.tex:557-590 separate from the main-body theorem display in main_body.tex:309-323; bridge them by explicit endpoint, exponent, and integral-collection steps.",
    "If endpoint law matching, stitched interval regularity, coefficient integrability, or interval-integral monotonicity is blocked, record the precise source-contract gap rather than weakening the theorem statement.",
    "Do not bundle the one-step frozen defect, DV witness, Gronwall accumulation, residual exponent bound, and final accumulated-error collection into one opaque assumption."
  ]
  reviewerChecklist := [
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle19_upper_packet before the linear-slowdown, residual-exponent, and accumulated-error blocks.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle19DiscreteForwardKlUpperPacket while retaining the cycle-15 EM packets and all existing discrete obligations.",
    "SALD.discreteForwardKlAccumulatedErrorBridgeContract still uses appendix.tex:557-590 and main_body.tex:309-323, with the source a(t), b(t), barGamma, and barDelta constants unchanged.",
    "The conversion window and proof-obligation ledger classify the cycle-19 packet as workflow/obligation data, not a proof of thm:forward-KL-discrete.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-19 middle packet for the discrete forward-KL accumulated-error bridge.

This translates the upper-selected accumulated-error target into a lower-ready
source-to-Lean map.  It keeps the final scalar bridge separate from the EM
interpolation, one-step frozen defect, DV velocity estimate, and Gronwall
accumulation backends.
-/