AutoSamplingTheory.SALD.cycle27DiscreteForwardKlUpperPacket

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 cycle27DiscreteForwardKlUpperPacket : 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 collection slice after the coefficient-chain audit: endpoint rewrites, the linear-slowdown exponent split, 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. eq:frozen_interp_terminal_disc_prop_additive_final
6. lem:gronwall
7. def:alpha-complexity

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:299-323 and appendix.tex:557-590 from the original source root, with sald_version_2.tex excluded.
2. Preserve the theorem statement, linear slowdown t(s)=s/r, r>=1, alpha ranges, the step-size condition, Gamma, Delta, barGamma, barDelta, and the constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.
3. Treat endpoint laws, stitched-interval regularity, coefficient integrability, residual-exponent monotonicity, full-interval Gamma/Delta identifications, and Gronwall as obligations or source-cited facts until local Lean proofs replace them.
4. Use the already-separated coefficient-chain audit only as a dependency; do not reopen the frozen-defect, LSI, DV, or time-change coefficient subproofs in this upper packet.
5. Require middle to keep AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and research-wiki/source-index/SALD_original.jsonl synchronized against these exact source windows.

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 introduce a new theorem-level smoothness, sign, integrability, or endpoint assumption; record missing facts as obligations.
3. Do not change the source a(t), b(t), Gamma/Delta, barGamma/barDelta, alpha, alpha', eta, r, or the theorem's exponential factors.
4. Do not replace the source route Gronwall output -> linear slowdown -> residual exponent bound -> integral collection with another entropy or path-space argument.
5. Do not mark lem:gronwall, interval-integral monotonicity, EM endpoint stitching, or the accumulated-error bridge as formalized.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.
2. First lower sub-slice: endpointBridge plus alphaComplexityCollection and deltaAccumulation in SALD.discreteForwardKlAccumulatedErrorBridgeContract, using appendix.tex:557-590 and main_body.tex:309-323.
3. Use SALD.discreteForwardKlResidualExponentBoundScalar and SALD.discreteForwardKlResidualExpBoundScalar only as existing scalar cores; the remaining interval-integral monotonicity and barGamma identification stay obligations if not proved.
4. Keep sald.discrete_forward_kl.coefficient_chain_audit as a dependency and reviewer ledger for constants, not as the lower target for this cycle.
5. If endpoint matching, stitched regularity, or full-interval A_alpha/barDelta collection is blocked, refine sald.discrete_forward_kl.accumulated_error_bridge or a named sibling obligation instead of adding assumptions.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle27DiscreteForwardKlUpperPacket and sald.discrete_forward_kl.cycle27_accumulated_collection_upper while retaining cycle-15, cycle-19, and cycle-23 packets.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle27_upper_accumulated_collection linked to the accumulated-error bridge and coefficient-chain audit.
3. SALD.discreteForwardKlAccumulatedErrorBridgeContract still preserves endpointBridge, initialExponentSplit, residualExponentBound, alphaComplexityCollection, gammaAccumulation, and deltaAccumulation as separate fields.
4. The conversion window and proof-obligation ledger cite appendix.tex:557-590 and main_body.tex:309-323 for this packet, and source-index refresh keeps sald_version_2.tex excluded.
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 cycle27DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket where
  objective := "Keep thm:forward-KL-discrete fixed and select the accumulated-error collection slice after the coefficient-chain audit: endpoint rewrites, the linear-slowdown exponent split, 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",
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:gronwall",
    "def:alpha-complexity"
  ]
  modeDiscipline := [
    "faithfulPaper: use only main_body.tex:299-323 and appendix.tex:557-590 from the original source root, with sald_version_2.tex excluded.",
    "Preserve the theorem statement, linear slowdown t(s)=s/r, r>=1, alpha ranges, the step-size condition, Gamma, Delta, barGamma, barDelta, and the constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.",
    "Treat endpoint laws, stitched-interval regularity, coefficient integrability, residual-exponent monotonicity, full-interval Gamma/Delta identifications, and Gronwall as obligations or source-cited facts until local Lean proofs replace them.",
    "Use the already-separated coefficient-chain audit only as a dependency; do not reopen the frozen-defect, LSI, DV, or time-change coefficient subproofs in this upper packet.",
    "Require middle to keep AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and research-wiki/source-index/SALD_original.jsonl synchronized against these exact source windows."
  ]
  nonGoals := [
    "Do not prove or restate thm:forward-KL-discrete in this packet.",
    "Do not introduce a new theorem-level smoothness, sign, integrability, or endpoint assumption; record missing facts as obligations.",
    "Do not change the source a(t), b(t), Gamma/Delta, barGamma/barDelta, alpha, alpha', eta, r, or the theorem's exponential factors.",
    "Do not replace the source route Gronwall output -> linear slowdown -> residual exponent bound -> integral collection with another entropy or path-space argument.",
    "Do not mark lem:gronwall, interval-integral monotonicity, EM endpoint stitching, or the accumulated-error bridge as formalized."
  ]
  lowerPacket := [
    "Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.",
    "First lower sub-slice: endpointBridge plus alphaComplexityCollection and deltaAccumulation in SALD.discreteForwardKlAccumulatedErrorBridgeContract, using appendix.tex:557-590 and main_body.tex:309-323.",
    "Use SALD.discreteForwardKlResidualExponentBoundScalar and SALD.discreteForwardKlResidualExpBoundScalar only as existing scalar cores; the remaining interval-integral monotonicity and barGamma identification stay obligations if not proved.",
    "Keep sald.discrete_forward_kl.coefficient_chain_audit as a dependency and reviewer ledger for constants, not as the lower target for this cycle.",
    "If endpoint matching, stitched regularity, or full-interval A_alpha/barDelta collection is blocked, refine sald.discrete_forward_kl.accumulated_error_bridge or a named sibling obligation instead of adding assumptions."
  ]
  reviewerChecklist := [
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle27DiscreteForwardKlUpperPacket and sald.discrete_forward_kl.cycle27_accumulated_collection_upper while retaining cycle-15, cycle-19, and cycle-23 packets.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle27_upper_accumulated_collection linked to the accumulated-error bridge and coefficient-chain audit.",
    "SALD.discreteForwardKlAccumulatedErrorBridgeContract still preserves endpointBridge, initialExponentSplit, residualExponentBound, alphaComplexityCollection, gammaAccumulation, and deltaAccumulation as separate fields.",
    "The conversion window and proof-obligation ledger cite appendix.tex:557-590 and main_body.tex:309-323 for this packet, and source-index refresh keeps sald_version_2.tex excluded.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-27 middle packet for the discrete forward-KL accumulated collection.

This translates the upper-selected accumulated-error slice into a lower-ready
source-to-Lean map.  It keeps the first lower target on endpoint matching plus
the `A_alpha` and `barDelta` additive collections, while leaving the residual
exponent and `barGamma` interval monotonicity as named dependencies.
-/