AutoSamplingTheory.SALD.cycle60ForwardKlSkeletonUpperPacket

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 cycle60ForwardKlSkeletonUpperPacket : 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 60 upper: after the accepted cycle-59 reviewer/build gate, wire the source-cited analytic interfaces into the faithful continuous thm:forward-KL proof skeleton, matching main_body.tex:238-247 and appendix.tex:164-252 without changing constants, theorem status, proof order, 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. lem:gronwall
7. lem:dv_variation
8. eq:LSI-KL-FI
9. eq:SALD
10. eq:FP-eq
11. def:alpha-complexity
12. 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. Global phase judgment: cycle 59 passed reviewer and build, so no failed previous cycle must be recovered before cycle 60 work.
2. Global phase judgment: Phase 1 theorem-skeleton translation is stable enough for focused theorem-level interface wiring, but not for broad cited-theory or reusable API backfill.
3. Global phase judgment: the single lower packet that best reduces remaining continuous forward-KL risk is SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.
4. Five-backend check: Gronwall has endpoint-safe differentiability/FTC and coefficient-side-condition contracts; DV has common-space, absolute-continuity, finite-KL, finite-log-mgf, measurability, and positive-alpha interfaces; LSI/KL/FI has density, zero-set, admissible-test, entropy-identity, and Fisher-chain interfaces; the continuous Fokker-Planck/KL derivative has mass-conservation, boundary, target-transport, and time-change interfaces; EM interpolation FP remains a downstream discrete sibling backend.
5. Route thm:forward-KL in the paper order derivative/Fokker-Planck -> LSI/KL/FI -> inverse schedule -> DV velocity energy -> Gronwall, preserving both 1/2 coefficients, alpha in (0,alpha0], dot{s}(t)^(-1), and the theorem's two exponent displays.
6. Keep the six theorem-route order from the cycle-59 ledger visible: forward-KL, discrete forward-KL, guided residual, general moving-target, unified forward-KL, and discrete general moving-target.

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 change source constants, merge exponent factors, alter the alpha range, add hidden endpoint/density/regularity assumptions, or use sald_version_2.tex.
4. Do not start broad SLT, concentration, disintegration, measure-theory, or SDE backfill before this theorem route is reviewed cleanly.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle should synchronize this cycle-60 upper route with conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and the thm:forward-KL proof DAG.
2. Lower should target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.
3. First sub-slice: appendix.tex:168-185 mass conservation, KL differentiation under the integral, SALD Fokker-Planck substitution, boundary/no-flux integration by parts, and the -FI identification.
4. Second sub-slice: appendix.tex:187-208 slowed-target transport velocity, target integration by parts, Cauchy-Schwarz/Young with the exact 1/2 share, and the L2 velocity term.
5. Third sub-slice: appendix.tex:218-228 inverse-schedule chain rule, slowed-velocity square scaling, and dot{s}(t)*dot t(s(t))^2 = dot{s}(t)^(-1).
6. Leave LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent side conditions, and EM interpolation as separate named interfaces unless their exact analytic backends compile locally.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle60ForwardKlSkeletonObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle60_post_cycle59_route and ASTIS.SALD.forward_KL.cycle60_lower_packet.kl_derivative after the cycle-59 and cycle-55 route nodes.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle60ForwardKlSkeletonUpperPacket, SALD.cycle60ForwardKlSkeletonObligation, and the cycle-60 DAG nodes.
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 cycle60ForwardKlSkeletonUpperPacket : ForwardKlUpperPacket where
  objective := "Cycle 60 upper: after the accepted cycle-59 reviewer/build gate, wire the source-cited analytic interfaces into the faithful continuous thm:forward-KL proof skeleton, matching main_body.tex:238-247 and appendix.tex:164-252 without changing constants, theorem status, proof order, 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",
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "eq:SALD",
    "eq:FP-eq",
    "def:alpha-complexity",
    "proof:thm:forward-KL-discrete:conditional-fp"
  ]
  modeDiscipline := [
    "Global phase judgment: cycle 59 passed reviewer and build, so no failed previous cycle must be recovered before cycle 60 work.",
    "Global phase judgment: Phase 1 theorem-skeleton translation is stable enough for focused theorem-level interface wiring, but not for broad cited-theory or reusable API backfill.",
    "Global phase judgment: the single lower packet that best reduces remaining continuous forward-KL risk is SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.",
    "Five-backend check: Gronwall has endpoint-safe differentiability/FTC and coefficient-side-condition contracts; DV has common-space, absolute-continuity, finite-KL, finite-log-mgf, measurability, and positive-alpha interfaces; LSI/KL/FI has density, zero-set, admissible-test, entropy-identity, and Fisher-chain interfaces; the continuous Fokker-Planck/KL derivative has mass-conservation, boundary, target-transport, and time-change interfaces; EM interpolation FP remains a downstream discrete sibling backend.",
    "Route thm:forward-KL in the paper order derivative/Fokker-Planck -> LSI/KL/FI -> inverse schedule -> DV velocity energy -> Gronwall, preserving both 1/2 coefficients, alpha in (0,alpha0], dot{s}(t)^(-1), and the theorem's two exponent displays.",
    "Keep the six theorem-route order from the cycle-59 ledger visible: forward-KL, discrete forward-KL, guided residual, general moving-target, unified forward-KL, and discrete general moving-target."
  ]
  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 change source constants, merge exponent factors, alter the alpha range, add hidden endpoint/density/regularity assumptions, or use sald_version_2.tex.",
    "Do not start broad SLT, concentration, disintegration, measure-theory, or SDE backfill before this theorem route is reviewed cleanly."
  ]
  lowerPacket := [
    "Middle should synchronize this cycle-60 upper route with conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and the thm:forward-KL proof DAG.",
    "Lower should target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.",
    "First sub-slice: appendix.tex:168-185 mass conservation, KL differentiation under the integral, SALD Fokker-Planck substitution, boundary/no-flux integration by parts, and the -FI identification.",
    "Second sub-slice: appendix.tex:187-208 slowed-target transport velocity, target integration by parts, Cauchy-Schwarz/Young with the exact 1/2 share, and the L2 velocity term.",
    "Third sub-slice: appendix.tex:218-228 inverse-schedule chain rule, slowed-velocity square scaling, and dot{s}(t)*dot t(s(t))^2 = dot{s}(t)^(-1).",
    "Leave LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent side conditions, and EM interpolation as separate named interfaces unless their exact analytic backends compile locally."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle60ForwardKlSkeletonObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle60_post_cycle59_route and ASTIS.SALD.forward_KL.cycle60_lower_packet.kl_derivative after the cycle-59 and cycle-55 route nodes.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle60ForwardKlSkeletonUpperPacket, SALD.cycle60ForwardKlSkeletonObligation, and the cycle-60 DAG nodes.",
    "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-60 upper obligation tying the accepted cycle-59 analytic ledger back
to the focused continuous forward-KL theorem route. -/