AutoSamplingTheory.SALD.cycle48UnifiedDiscreteSkeletonUpperPacket

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.GeneralVaSaldUpperPacket. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle48UnifiedDiscreteSkeletonUpperPacket : GeneralVaSaldUpperPacket

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 5: wire thm:unified-forward-KL and thm:general-moving-target-SALD-discrete through the continuous/general theorem skeletons and the five explicit source-cited analytic interfaces, preserving all source statements, constants, and labels.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:unified-forward-KL
2. eq:residual-term
3. eq:poisson-eq
4. eq:SALD_Ito
5. proof:thm:unified-forward-KL
6. prop:guided_path_residual
7. thm:general-moving-target-SALD
8. thm:general-moving-target-SALD-discrete
9. eq:SALD_general_EM
10. eq:general_moving_target_SALD_frozen_interp
11. eq:general_discrete_delta_def
12. lem:frozen_delta_cross_lip
13. lem:dv_variation
14. lem:gronwall
15. eq:LSI-KL-FI
16. def:alpha-complexity

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1: use only main_body.tex, appendix.tex, and iteration_complexity.tex from the original SALD paper; sald_version_2.tex remains out of scope.
2. Before lower work, all five slow analytic backends must stay explicit: Gronwall endpoint calculus, DV common-space/finite-log-mgf, LSI/KL/FI density-test, continuous Fokker-Planck/KL derivative, and EM endpoint/conditional-law Fokker-Planck.
3. The unified theorem route is only the paper specialization c_t <- u_t after the transport bridge from prop:guided_path_residual and eq:poisson-eq; no direct VA-SALD KL proof is introduced.
4. The discrete general theorem route is EM interpolation -> frozen-delta -> KL derivative/LSI -> residual DV -> Gronwall/stitching -> guided specialization, with doubled residual-energy and Gamma/Delta coefficients unchanged.
5. All missing density, boundary, endpoint, absolute-continuity, finite-KL/FI, finite-log-mgf, conditional-law, coefficient-regularity, and divergence-linearity facts remain named obligations.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not restate thm:unified-forward-KL or thm:general-moving-target-SALD-discrete, and do not promote SALD.unifiedForwardKlContract or SALD.generalVaSaldDiscreteContract above contractOnly.
2. Do not prove or replace Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, EM conditional-FP, frozen-delta, or guided residual analytic backends in this upper packet.
3. Do not add a path-space, Girsanov, Pinsker, Talagrand, PI, or direct theorem proof route.
4. Do not import or mark an SLT theorem formalized; local SLT material may only guide a later narrow backend audit after this route wrapper is accepted.
5. Do not run a broad source-index rebaseline except for the acceptance gate.

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 rows for SALD.cycle48UnifiedDiscreteSkeletonUpperPacket and SALD.cycle48UnifiedDiscreteSkeletonObligation.
2. Lower should target exactly one backend after the route wrapper is accepted: prefer SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.
3. First lower sub-slice: expose appendix.tex:1354-1387 EM endpoint, conditional-law density, and Fokker-Planck interfaces needed before differentiating KL(hat rho_s||tilde pi_s).
4. Second lower sub-slice: preserve appendix.tex:1469-1511 frozen/residual algebra and the two sigma_eta^2/8 Young shares already isolated by the cycle-28 middle/lower packets.
5. If the backend is too large, sharpen only the source-cited interface with common-space, absolute-continuity, finite-quantity, endpoint, conditional-law, and stitched-interval hypotheses; do not change the theorem statement.
6. Only after this skeleton route is stable should lower backfill a narrow measure-theory detail, guided by local SLT material as reference-only and without importing SLT as a dependency.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle48UnifiedDiscreteSkeletonObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag expose cycle-48 route nodes for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete.
3. SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-48 packet, obligation, and DAG route nodes.
4. The five slow analytic interfaces remain source-cited or obligation-level; no theorem statement, source constant, source label, or external reuse status changes.
5. No axiom, sorry, admit, Prop := True, := trivial, hidden assumption, or alternate proof route is introduced.
6. 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 cycle48UnifiedDiscreteSkeletonUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Main skeleton sprint 5: wire thm:unified-forward-KL and thm:general-moving-target-SALD-discrete through the continuous/general theorem skeletons and the five explicit source-cited analytic interfaces, preserving all source statements, constants, and labels."
  sourceLabels := [
    "thm:unified-forward-KL",
    "eq:residual-term",
    "eq:poisson-eq",
    "eq:SALD_Ito",
    "proof:thm:unified-forward-KL",
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:general-moving-target-SALD-discrete",
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "lem:frozen_delta_cross_lip",
    "lem:dv_variation",
    "lem:gronwall",
    "eq:LSI-KL-FI",
    "def:alpha-complexity"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only main_body.tex, appendix.tex, and iteration_complexity.tex from the original SALD paper; sald_version_2.tex remains out of scope.",
    "Before lower work, all five slow analytic backends must stay explicit: Gronwall endpoint calculus, DV common-space/finite-log-mgf, LSI/KL/FI density-test, continuous Fokker-Planck/KL derivative, and EM endpoint/conditional-law Fokker-Planck.",
    "The unified theorem route is only the paper specialization c_t <- u_t after the transport bridge from prop:guided_path_residual and eq:poisson-eq; no direct VA-SALD KL proof is introduced.",
    "The discrete general theorem route is EM interpolation -> frozen-delta -> KL derivative/LSI -> residual DV -> Gronwall/stitching -> guided specialization, with doubled residual-energy and Gamma/Delta coefficients unchanged.",
    "All missing density, boundary, endpoint, absolute-continuity, finite-KL/FI, finite-log-mgf, conditional-law, coefficient-regularity, and divergence-linearity facts remain named obligations."
  ]
  nonGoals := [
    "Do not restate thm:unified-forward-KL or thm:general-moving-target-SALD-discrete, and do not promote SALD.unifiedForwardKlContract or SALD.generalVaSaldDiscreteContract above contractOnly.",
    "Do not prove or replace Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, EM conditional-FP, frozen-delta, or guided residual analytic backends in this upper packet.",
    "Do not add a path-space, Girsanov, Pinsker, Talagrand, PI, or direct theorem proof route.",
    "Do not import or mark an SLT theorem formalized; local SLT material may only guide a later narrow backend audit after this route wrapper is accepted.",
    "Do not run a broad source-index rebaseline except for the acceptance gate."
  ]
  lowerPacket := [
    "Middle should synchronize the conversion window and proof-obligation rows for SALD.cycle48UnifiedDiscreteSkeletonUpperPacket and SALD.cycle48UnifiedDiscreteSkeletonObligation.",
    "Lower should target exactly one backend after the route wrapper is accepted: prefer SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.",
    "First lower sub-slice: expose appendix.tex:1354-1387 EM endpoint, conditional-law density, and Fokker-Planck interfaces needed before differentiating KL(hat rho_s||tilde pi_s).",
    "Second lower sub-slice: preserve appendix.tex:1469-1511 frozen/residual algebra and the two sigma_eta^2/8 Young shares already isolated by the cycle-28 middle/lower packets.",
    "If the backend is too large, sharpen only the source-cited interface with common-space, absolute-continuity, finite-quantity, endpoint, conditional-law, and stitched-interval hypotheses; do not change the theorem statement.",
    "Only after this skeleton route is stable should lower backfill a narrow measure-theory detail, guided by local SLT material as reference-only and without importing SLT as a dependency."
  ]
  reviewerChecklist := [
    "SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle48UnifiedDiscreteSkeletonObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag expose cycle-48 route nodes for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete.",
    "SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-48 packet, obligation, and DAG route nodes.",
    "The five slow analytic interfaces remain source-cited or obligation-level; no theorem statement, source constant, source label, or external reuse status changes.",
    "No axiom, sorry, admit, Prop := True, := trivial, hidden assumption, or 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-48 obligation tying the unified and discrete general theorem
skeletons to the already named continuous/general and EM analytic interfaces. -/