AutoSamplingTheory.SALD.cycle46DiscreteForwardKlSkeletonUpperPacket

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

Main skeleton sprint 3: wire the theorem-level analytic interfaces into thm:forward-KL-discrete, matching main_body.tex:299-323 and appendix.tex:260-592, with the source constants, theorem statement, and proof route unchanged.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL-discrete
2. thm:forward-KL
3. eq:frozen_interp_terminal_disc_prop_additive_final
4. lem:frozen_delta_cross_lip_sald
5. eq:discrete_delta_def
6. eq:KL-derivative-0-discrete
7. eq:KL-derivative-1-discrete
8. eq:KL-derivative-2-discrete
9. eq:KL-derivative-3-discrete
10. eq:frozen-cross-bound-discrete
11. eq:KL-derivative-5-discrete
12. eq:dv-v-term-discrete
13. eq:KL-derivative-6-discrete
14. eq:KL-derivative-7-discrete
15. lem:dv_variation
16. lem:gronwall
17. eq:LSI-KL-FI

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1: use only the original main_body.tex:299-323 statement and appendix.tex:260-592 proof; sald_version_2.tex remains out of scope.
2. Before assigning lower work, the five slow backends are checked as explicit interfaces: Gronwall endpoint calculus, DV common-space/finite-log-mgf, LSI/KL/FI density-test, continuous KL derivative/Fokker-Planck reuse, and EM interpolation endpoint/conditional-law Fokker-Planck.
3. The discrete theorem route is EM interpolation and endpoint laws -> conditional Fokker-Planck/KL derivative -> frozen score defect and LSI -> DV velocity bound -> time change -> Gronwall -> linear-slowdown accumulated-error collection.
4. The source constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'} are not changed.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not restate thm:forward-KL-discrete or promote SALD.discreteSaldContract above contractOnly.
2. Do not prove or replace the Gronwall, DV, LSI/KL/FI, continuous KL derivative, EM conditional-FP, frozen-defect, or stitched-interval analytic backends in this upper packet.
3. Do not replace the marginal KL proof with path-space or Girsanov analysis.
4. Do not start systematic measure-theory or SLT backfill before this theorem-level discrete route is stable.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle should synchronize the conversion window and proof-obligation row for this cycle-46 discrete theorem wrapper.
2. Lower should target exactly one named backend on the route, preferably SALD.discreteForwardKlEmInterpolationSideConditionContract / sald.discrete_forward_kl.em_conditional_fokker_planck or SALD.discreteForwardKlAccumulatedErrorBridgeContract / sald.discrete_forward_kl.accumulated_error_bridge.
3. If the selected backend is too large, sharpen the source-cited or obligation interface with common-space, absolute-continuity, endpoint, density, finite-quantity, coefficient-regularity, and stitched-interval hypotheses instead of changing the theorem statement.
4. Keep lem:frozen_delta_cross_lip_sald below formalized until the later general frozen-defect lemma is specialized with c=0 and sigma_eta(t)=sqrt(2).

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract lists SALD.cycle46DiscreteForwardKlSkeletonObligation while remaining contractOnly.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle46_theorem_skeleton_route before the lower EM, defect, DV, and Gronwall nodes.
3. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes the cycle-46 packet, obligation, DAG, and route node.
4. No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.
5. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

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 cycle46DiscreteForwardKlSkeletonUpperPacket :
    DiscreteForwardKlUpperPacket where
  objective := "Main skeleton sprint 3: wire the theorem-level analytic interfaces into thm:forward-KL-discrete, matching main_body.tex:299-323 and appendix.tex:260-592, with the source constants, theorem statement, and proof route unchanged."
  sourceLabels := [
    "thm:forward-KL-discrete",
    "thm:forward-KL",
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:frozen_delta_cross_lip_sald",
    "eq:discrete_delta_def",
    "eq:KL-derivative-0-discrete",
    "eq:KL-derivative-1-discrete",
    "eq:KL-derivative-2-discrete",
    "eq:KL-derivative-3-discrete",
    "eq:frozen-cross-bound-discrete",
    "eq:KL-derivative-5-discrete",
    "eq:dv-v-term-discrete",
    "eq:KL-derivative-6-discrete",
    "eq:KL-derivative-7-discrete",
    "lem:dv_variation",
    "lem:gronwall",
    "eq:LSI-KL-FI"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only the original main_body.tex:299-323 statement and appendix.tex:260-592 proof; sald_version_2.tex remains out of scope.",
    "Before assigning lower work, the five slow backends are checked as explicit interfaces: Gronwall endpoint calculus, DV common-space/finite-log-mgf, LSI/KL/FI density-test, continuous KL derivative/Fokker-Planck reuse, and EM interpolation endpoint/conditional-law Fokker-Planck.",
    "The discrete theorem route is EM interpolation and endpoint laws -> conditional Fokker-Planck/KL derivative -> frozen score defect and LSI -> DV velocity bound -> time change -> Gronwall -> linear-slowdown accumulated-error collection.",
    "The source constants T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'} are not changed."
  ]
  nonGoals := [
    "Do not restate thm:forward-KL-discrete or promote SALD.discreteSaldContract above contractOnly.",
    "Do not prove or replace the Gronwall, DV, LSI/KL/FI, continuous KL derivative, EM conditional-FP, frozen-defect, or stitched-interval analytic backends in this upper packet.",
    "Do not replace the marginal KL proof with path-space or Girsanov analysis.",
    "Do not start systematic measure-theory or SLT backfill before this theorem-level discrete route is stable."
  ]
  lowerPacket := [
    "Middle should synchronize the conversion window and proof-obligation row for this cycle-46 discrete theorem wrapper.",
    "Lower should target exactly one named backend on the route, preferably SALD.discreteForwardKlEmInterpolationSideConditionContract / sald.discrete_forward_kl.em_conditional_fokker_planck or SALD.discreteForwardKlAccumulatedErrorBridgeContract / sald.discrete_forward_kl.accumulated_error_bridge.",
    "If the selected backend is too large, sharpen the source-cited or obligation interface with common-space, absolute-continuity, endpoint, density, finite-quantity, coefficient-regularity, and stitched-interval hypotheses instead of changing the theorem statement.",
    "Keep lem:frozen_delta_cross_lip_sald below formalized until the later general frozen-defect lemma is specialized with c=0 and sigma_eta(t)=sqrt(2)."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract lists SALD.cycle46DiscreteForwardKlSkeletonObligation while remaining contractOnly.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle46_theorem_skeleton_route before the lower EM, defect, DV, and Gronwall nodes.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes the cycle-46 packet, obligation, DAG, and route node.",
    "No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-46 obligation tying the discrete forward-KL theorem skeleton to the
five source-cited analytic interfaces. -/