AutoSamplingTheory.SALD.cycle45ForwardKlSkeletonUpperPacket

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

Main skeleton sprint 2: wire the five source-cited analytic interfaces into the faithful proof skeleton for thm:forward-KL, matching main_body.tex:238-247 and appendix.tex:164-252 without changing constants, theorem statements, or source labels.

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
8. proof:thm:forward-KL:derivative
9. proof:thm:forward-KL:dv-energy
10. proof:thm:forward-KL:gronwall

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:238-247 theorem display and appendix.tex:164-252 proof; sald_version_2.tex remains out of scope.
2. Before 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, and EM interpolation Fokker-Planck for downstream discrete reuse.
3. The continuous theorem route is derivative -> LSI -> inverse time change -> DV -> Gronwall, with K(t), a(t), b(t), the factor 1/2, and both final exponent displays unchanged.
4. All missing density, boundary, finite-KL/FI, finite-log-mgf, endpoint, positivity, and coefficient-regularity facts remain named obligations rather than hidden theorem assumptions.

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 or promote SALD.continuousSaldContract above contractOnly.
2. Do not prove or replace the Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, or EM interpolation analytic backends in this upper packet.
3. Do not introduce a different entropy method, a different slowdown normalization, or a merged one-exponential theorem display.
4. Do not start systematic SLT or measure-theory backfill before the theorem skeleton route is accepted.

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 the new cycle-45 forward-KL route wrapper.
2. Lower should target exactly one remaining named backend already on the route: sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, sald.forward_kl.dv_finite_log_mgf_witness, or sald.forward_kl.gronwall_side_conditions.
3. If the backend is too large, sharpen that interface with source-cited common-space, absolute-continuity, finite quantity, endpoint, positivity, and regularity witnesses instead of changing the theorem statement.
4. Keep the discrete EM interpolation backend visible as a sibling slow interface for theorem-route stability, but do not spend this cycle on discrete coefficient or accumulated-error work.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle45ForwardKlSkeletonObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route before the lower derivative, DV, and Gronwall nodes.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes the cycle-45 packet, obligation, and DAG block.
4. No analytic dependency is marked formalized, no source theorem statement or constant changes, and no fake proof closure 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 cycle45ForwardKlSkeletonUpperPacket : ForwardKlUpperPacket where
  objective := "Main skeleton sprint 2: wire the five source-cited analytic interfaces into the faithful proof skeleton for thm:forward-KL, matching main_body.tex:238-247 and appendix.tex:164-252 without changing constants, theorem statements, or source labels."
  sourceLabels := [
    "thm:forward-KL",
    "eq:SALD",
    "eq:FP-eq",
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall",
    "proof:thm:forward-KL:derivative",
    "proof:thm:forward-KL:dv-energy",
    "proof:thm:forward-KL:gronwall"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only the original main_body.tex:238-247 theorem display and appendix.tex:164-252 proof; sald_version_2.tex remains out of scope.",
    "Before 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, and EM interpolation Fokker-Planck for downstream discrete reuse.",
    "The continuous theorem route is derivative -> LSI -> inverse time change -> DV -> Gronwall, with K(t), a(t), b(t), the factor 1/2, and both final exponent displays unchanged.",
    "All missing density, boundary, finite-KL/FI, finite-log-mgf, endpoint, positivity, and coefficient-regularity facts remain named obligations rather than hidden theorem assumptions."
  ]
  nonGoals := [
    "Do not restate thm:forward-KL or promote SALD.continuousSaldContract above contractOnly.",
    "Do not prove or replace the Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, or EM interpolation analytic backends in this upper packet.",
    "Do not introduce a different entropy method, a different slowdown normalization, or a merged one-exponential theorem display.",
    "Do not start systematic SLT or measure-theory backfill before the theorem skeleton route is accepted."
  ]
  lowerPacket := [
    "Middle should synchronize the conversion window and proof-obligation row for the new cycle-45 forward-KL route wrapper.",
    "Lower should target exactly one remaining named backend already on the route: sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, sald.forward_kl.dv_finite_log_mgf_witness, or sald.forward_kl.gronwall_side_conditions.",
    "If the backend is too large, sharpen that interface with source-cited common-space, absolute-continuity, finite quantity, endpoint, positivity, and regularity witnesses instead of changing the theorem statement.",
    "Keep the discrete EM interpolation backend visible as a sibling slow interface for theorem-route stability, but do not spend this cycle on discrete coefficient or accumulated-error work."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle45ForwardKlSkeletonObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route before the lower derivative, DV, and Gronwall nodes.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes the cycle-45 packet, obligation, and DAG block.",
    "No analytic dependency is marked formalized, no source theorem statement or constant changes, and no fake proof closure is introduced.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

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