AutoSamplingTheory.SALD.cycle50ForwardKlSkeletonUpperPacket

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

Cycle 50 upper: consume the cycle-49 analytic-readiness audit and re-wire the faithful thm:forward-KL skeleton through the five source-cited analytic interfaces, 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. proof:thm:forward-KL
3. proof:thm:forward-KL:derivative
4. proof:thm:forward-KL:dv-energy
5. proof:thm:forward-KL:gronwall
6. eq:LSI-KL-FI
7. lem:dv_variation
8. lem:gronwall
9. def:alpha-complexity
10. proof:thm:forward-KL-discrete:conditional-fp

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 statement and appendix.tex:164-252 proof; sald_version_2.tex remains excluded.
2. The five slow backends are checked before lower work: endpoint-safe Gronwall, common-space DV with finite log-mgf, LSI/KL/FI density-test and Fisher chain rule, continuous KL derivative/Fokker--Planck, and downstream EM interpolation Fokker--Planck.
3. The continuous theorem route remains derivative -> LSI -> inverse schedule time change -> DV velocity energy -> Gronwall, with K(t), a(t), b(t), the 1/2 factors, alpha range, and both final exponent displays unchanged.
4. Endpoint, density, absolute-continuity, finite-KL/FI, finite-log-mgf, boundary, coefficient-regularity, and interval-integrability facts are named obligations, not hidden hypotheses of thm:forward-KL.

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, change SALD.continuousForwardKlStatementContract, or promote SALD.continuousSaldContract above contractOnly.
2. Do not prove or replace Gronwall, DV, LSI/KL/FI, the continuous Fokker--Planck/KL derivative, or the EM interpolation backend in this upper packet.
3. Do not merge the two source exponent factors, change the coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1), or replace the paper route with another entropy method.
4. Do not start broad SLT, concentration, or SDE backfill before this theorem-route wiring remains synchronized in Lean and Markdown.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle should synchronize this cycle-50 upper route with conversion-windows/ASTIS-SALD-001.md and proof-obligations/ASTIS-SALD-001.md.
2. If lower proof-producing work resumes on continuous forward-KL, target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.
3. The first lower sub-slice is the source KL derivative interface: law/density regularity, mass conservation, SALD Fokker--Planck, integration by parts, target transport, and inverse-schedule calculus.
4. Keep DV, LSI/KL/FI, Gronwall side conditions, endpoint schedule identities, and EM interpolation as separate named obligations unless an exact compiled proof is added.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle50ForwardKlSkeletonObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle50_theorem_skeleton_route and still routes through the cycle-45 theorem wrapper and cycle-49 readiness audit.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes the cycle-50 upper packet, obligation, and DAG block.
4. All five slow analytic backends remain ProofStatus.obligation or ProofStatus.sourceCited unless their full analytic dependencies build locally.
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 cycle50ForwardKlSkeletonUpperPacket : ForwardKlUpperPacket where
  objective := "Cycle 50 upper: consume the cycle-49 analytic-readiness audit and re-wire the faithful thm:forward-KL skeleton through the five source-cited analytic interfaces, matching main_body.tex:238-247 and appendix.tex:164-252 without changing constants, theorem statements, or source labels."
  sourceLabels := [
    "thm:forward-KL",
    "proof:thm:forward-KL",
    "proof:thm:forward-KL:derivative",
    "proof:thm:forward-KL:dv-energy",
    "proof:thm:forward-KL:gronwall",
    "eq:LSI-KL-FI",
    "lem:dv_variation",
    "lem:gronwall",
    "def:alpha-complexity",
    "proof:thm:forward-KL-discrete:conditional-fp"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only the original main_body.tex:238-247 statement and appendix.tex:164-252 proof; sald_version_2.tex remains excluded.",
    "The five slow backends are checked before lower work: endpoint-safe Gronwall, common-space DV with finite log-mgf, LSI/KL/FI density-test and Fisher chain rule, continuous KL derivative/Fokker--Planck, and downstream EM interpolation Fokker--Planck.",
    "The continuous theorem route remains derivative -> LSI -> inverse schedule time change -> DV velocity energy -> Gronwall, with K(t), a(t), b(t), the 1/2 factors, alpha range, and both final exponent displays unchanged.",
    "Endpoint, density, absolute-continuity, finite-KL/FI, finite-log-mgf, boundary, coefficient-regularity, and interval-integrability facts are named obligations, not hidden hypotheses of thm:forward-KL."
  ]
  nonGoals := [
    "Do not restate thm:forward-KL, change SALD.continuousForwardKlStatementContract, or promote SALD.continuousSaldContract above contractOnly.",
    "Do not prove or replace Gronwall, DV, LSI/KL/FI, the continuous Fokker--Planck/KL derivative, or the EM interpolation backend in this upper packet.",
    "Do not merge the two source exponent factors, change the coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1), or replace the paper route with another entropy method.",
    "Do not start broad SLT, concentration, or SDE backfill before this theorem-route wiring remains synchronized in Lean and Markdown."
  ]
  lowerPacket := [
    "Middle should synchronize this cycle-50 upper route with conversion-windows/ASTIS-SALD-001.md and proof-obligations/ASTIS-SALD-001.md.",
    "If lower proof-producing work resumes on continuous forward-KL, target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.",
    "The first lower sub-slice is the source KL derivative interface: law/density regularity, mass conservation, SALD Fokker--Planck, integration by parts, target transport, and inverse-schedule calculus.",
    "Keep DV, LSI/KL/FI, Gronwall side conditions, endpoint schedule identities, and EM interpolation as separate named obligations unless an exact compiled proof is added."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle50ForwardKlSkeletonObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle50_theorem_skeleton_route and still routes through the cycle-45 theorem wrapper and cycle-49 readiness audit.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes the cycle-50 upper packet, obligation, and DAG block.",
    "All five slow analytic backends remain ProofStatus.obligation or ProofStatus.sourceCited unless their full analytic dependencies build locally.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-50 obligation tying the post-readiness audit back to `thm:forward-KL`. -/