AutoSamplingTheory.SALD.cycle63UnifiedDiscreteGeneralSkeletonUpperPacket

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

Cycle 63 upper: cycle 62 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough to rewire thm:unified-forward-KL and thm:general-moving-target-SALD-discrete through the continuous/general skeletons and then begin exactly one narrow measure-theory backfill; the single lower packet is a paired Measure.map endpoint-law helper for the discrete general EM interpolation over appendix.tex:1354-1387.

sourceLabels : List String (explicit)

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

Ordered data items

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

modeDiscipline : List String (explicit)

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

Ordered data items

1. Global phase judgment: cycle 62 did not fail and needs no recovery; it accepted the guided residual / continuous general route and the appendix.tex:813-835 scaled residual scalar handoff while keeping all theorem statuses and slow analytic interfaces below formalized.
2. Global phase judgment: Phase 1 theorem-skeleton translation is stable enough for this unified/discrete-general route refresh and one narrow endpoint-law measure backfill, but still not for broad cited-theory, disintegration, Fokker-Planck, or reusable API reorganization.
3. Global phase judgment: the lower packet that best reduces remaining proof risk is the discrete general EM endpoint/common-space layer, narrowed to a paired pushforward-law equality from componentwise a.e. endpoint identities and marginal extraction from that joint law; this supports later stitched-law and conditional-law work without touching the theorem statement.
4. Five-backend check 1, Gronwall: SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, SALD.generalMovingTargetGronwallSideConditionContract, and SALD.generalMovingTargetDiscreteGronwallSideConditionContract keep endpoint-safe differentiability/FTC, interval integrability, coefficient regularity, endpoint rewrites, exponent splitting, and display matching explicit.
5. Five-backend check 2, DV: dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, and SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract keep common-space, absolute-continuity, finite KL/log-likelihood, selected-test measurability, finite log-mgf, and positive-alpha scaling witnesses explicit.
6. Five-backend check 3, LSI/KL/FI: SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi keep density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain-rule assumptions explicit.
7. Five-backend check 4, continuous Fokker-Planck/KL derivative: SALD.forwardKlDerivativeCandidateContract, SALD.generalMovingTargetDerivativeCandidateContract, SALD.cycle62GuidedGeneralScaledResidualLowerObligation, and sald.general_moving_target.kl_derivative keep mass conservation, KL differentiation, Fokker-Planck substitution, integration by parts, target transport, residual scaling, LSI, and schedule side conditions explicit.
8. Five-backend check 5, EM interpolation Fokker-Planck: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation, AutoSamplingTheory.lawMapEqOfAEEq, and sald.general_moving_target_discrete.em_interpolation_fp expose endpoint laws, common-space Measure.map bookkeeping, conditional drift, density/absolute-continuity, weak conditional Fokker-Planck, Laplacian splitting, and stitched-interval side conditions without promoting the backend.
9. The theorem route remains paper ordered: forward-KL through cycle 60, discrete forward-KL through cycle 61, guided residual and continuous general through cycle 62, unified forward-KL as the c_t<-u_t specialization using prop:guided_path_residual and eq:poisson-eq, and discrete general moving-target through general EM, frozen-delta, derivative/LSI, residual DV, constant-schedule Gronwall, and theorem-display stitching.
10. FaithfulPaper Phase 1: use original main_body.tex:359-395, appendix.tex:949-951, and appendix.tex:1313-1603; sald_version_2.tex remains excluded.

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, thm:general-moving-target-SALD, or thm:general-moving-target-SALD-discrete.
2. Do not change sigma_eta factors, doubled residual coefficients, Gamma/Delta terms, alpha ranges, constant inverse-schedule assumptions, endpoint laws, source labels, or theorem displays.
3. Do not promote Gronwall, DV, LSI/KL/FI, continuous Fokker-Planck/KL differentiation, EM conditional Fokker-Planck, conditional laws, theorem contracts, or SLT reuse status above their current sourceCited/obligation/contractOnly level.
4. Do not replace the source derivative -> LSI -> DV -> Gronwall route, the correction-field specialization, or the paper EM/frozen-delta route by a direct VA-SALD, path-space, Girsanov, Pinsker, Talagrand, PI, or broad SLT proof.
5. Do not start a broad measure-theory or SDE port; the permitted backfill is exactly one endpoint-law Measure.map helper.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle should synchronize this cycle-63 upper route with conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, SALD.generalVaSaldProofDag, and SALD.generalVaSaldDiscreteProofDag.
2. Lower should keep the narrow measure-theory backfill at paired endpoint Measure.map bookkeeping: AutoSamplingTheory.lawMapProdEqOfAEEq for the joint law, AutoSamplingTheory.lawMapProdFst/Snd for marginal extraction, then record it under SALD.cycle63UnifiedDiscreteGeneralMeasureBackfillObligation / sald.general_moving_target_discrete.cycle63_joint_endpoint_law_backfill.
3. Source slice: appendix.tex:1354-1387, endpoint/common-space bookkeeping for the general EM interpolation before conditional drift and weak Fokker-Planck are used.
4. Use local SLT material only as a style guide for Measure.map and a.e. equality patterns, especially SLT/SmallBallProb.lean and SLT/GaussianMeasure.lean; no SLT theorem is imported or marked as a SALD backend.
5. The paired pushforward and marginal helpers may be used later to keep two endpoint representatives on one common probability space, but they do not prove Brownian construction, regular conditional drift, density/AC, weak Fokker-Planck, KL differentiation, or stitched Gronwall regularity.

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.cycle63UnifiedDiscreteGeneralSkeletonObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag include SALD.cycle63UnifiedDiscreteGeneralDag with ASTIS.SALD.unified_discrete_general.cycle63_upper_route and ASTIS.SALD.general_moving_target_discrete.cycle63_joint_endpoint_law_backfill.
3. SALD.saldDependenciesForLabel for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete includes the cycle-63 packet, obligation, DAG, and paired Measure.map backfill.
4. AutoSamplingTheory.lawMapProdEqOfAEEq and AutoSamplingTheory.lawMapProdFst/Snd compile as local measure helpers, but the EM interpolation Fokker-Planck backend and theorem statuses remain below formalized.
5. The conversion window, proof-obligation ledger, and SLT reuse audit record the global phase judgment, five-backend check, theorem route, lower packet, and no-SLT-import status.
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 cycle63UnifiedDiscreteGeneralSkeletonUpperPacket :
    GeneralVaSaldUpperPacket where
  objective := "Cycle 63 upper: cycle 62 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough to rewire thm:unified-forward-KL and thm:general-moving-target-SALD-discrete through the continuous/general skeletons and then begin exactly one narrow measure-theory backfill; the single lower packet is a paired Measure.map endpoint-law helper for the discrete general EM interpolation over appendix.tex:1354-1387."
  sourceLabels := [
    "thm:unified-forward-KL",
    "proof:thm:unified-forward-KL",
    "eq:residual-term",
    "eq:poisson-eq",
    "eq:SALD_Ito",
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:general-moving-target-SALD-discrete",
    "eq:general_moving_target_KL_bound_discrete",
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "proof:thm:general-moving-target-SALD-discrete:em-endpoints",
    "proof:thm:general-moving-target-SALD-discrete:derivative",
    "proof:thm:general-moving-target-SALD-discrete:gronwall",
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "def:alpha-complexity"
  ]
  modeDiscipline := [
    "Global phase judgment: cycle 62 did not fail and needs no recovery; it accepted the guided residual / continuous general route and the appendix.tex:813-835 scaled residual scalar handoff while keeping all theorem statuses and slow analytic interfaces below formalized.",
    "Global phase judgment: Phase 1 theorem-skeleton translation is stable enough for this unified/discrete-general route refresh and one narrow endpoint-law measure backfill, but still not for broad cited-theory, disintegration, Fokker-Planck, or reusable API reorganization.",
    "Global phase judgment: the lower packet that best reduces remaining proof risk is the discrete general EM endpoint/common-space layer, narrowed to a paired pushforward-law equality from componentwise a.e. endpoint identities and marginal extraction from that joint law; this supports later stitched-law and conditional-law work without touching the theorem statement.",
    "Five-backend check 1, Gronwall: SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, SALD.generalMovingTargetGronwallSideConditionContract, and SALD.generalMovingTargetDiscreteGronwallSideConditionContract keep endpoint-safe differentiability/FTC, interval integrability, coefficient regularity, endpoint rewrites, exponent splitting, and display matching explicit.",
    "Five-backend check 2, DV: dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, and SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract keep common-space, absolute-continuity, finite KL/log-likelihood, selected-test measurability, finite log-mgf, and positive-alpha scaling witnesses explicit.",
    "Five-backend check 3, LSI/KL/FI: SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi keep density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain-rule assumptions explicit.",
    "Five-backend check 4, continuous Fokker-Planck/KL derivative: SALD.forwardKlDerivativeCandidateContract, SALD.generalMovingTargetDerivativeCandidateContract, SALD.cycle62GuidedGeneralScaledResidualLowerObligation, and sald.general_moving_target.kl_derivative keep mass conservation, KL differentiation, Fokker-Planck substitution, integration by parts, target transport, residual scaling, LSI, and schedule side conditions explicit.",
    "Five-backend check 5, EM interpolation Fokker-Planck: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation, AutoSamplingTheory.lawMapEqOfAEEq, and sald.general_moving_target_discrete.em_interpolation_fp expose endpoint laws, common-space Measure.map bookkeeping, conditional drift, density/absolute-continuity, weak conditional Fokker-Planck, Laplacian splitting, and stitched-interval side conditions without promoting the backend.",
    "The theorem route remains paper ordered: forward-KL through cycle 60, discrete forward-KL through cycle 61, guided residual and continuous general through cycle 62, unified forward-KL as the c_t<-u_t specialization using prop:guided_path_residual and eq:poisson-eq, and discrete general moving-target through general EM, frozen-delta, derivative/LSI, residual DV, constant-schedule Gronwall, and theorem-display stitching.",
    "FaithfulPaper Phase 1: use original main_body.tex:359-395, appendix.tex:949-951, and appendix.tex:1313-1603; sald_version_2.tex remains excluded."
  ]
  nonGoals := [
    "Do not restate thm:unified-forward-KL, thm:general-moving-target-SALD, or thm:general-moving-target-SALD-discrete.",
    "Do not change sigma_eta factors, doubled residual coefficients, Gamma/Delta terms, alpha ranges, constant inverse-schedule assumptions, endpoint laws, source labels, or theorem displays.",
    "Do not promote Gronwall, DV, LSI/KL/FI, continuous Fokker-Planck/KL differentiation, EM conditional Fokker-Planck, conditional laws, theorem contracts, or SLT reuse status above their current sourceCited/obligation/contractOnly level.",
    "Do not replace the source derivative -> LSI -> DV -> Gronwall route, the correction-field specialization, or the paper EM/frozen-delta route by a direct VA-SALD, path-space, Girsanov, Pinsker, Talagrand, PI, or broad SLT proof.",
    "Do not start a broad measure-theory or SDE port; the permitted backfill is exactly one endpoint-law Measure.map helper."
  ]
  lowerPacket := [
    "Middle should synchronize this cycle-63 upper route with conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, SALD.generalVaSaldProofDag, and SALD.generalVaSaldDiscreteProofDag.",
    "Lower should keep the narrow measure-theory backfill at paired endpoint Measure.map bookkeeping: AutoSamplingTheory.lawMapProdEqOfAEEq for the joint law, AutoSamplingTheory.lawMapProdFst/Snd for marginal extraction, then record it under SALD.cycle63UnifiedDiscreteGeneralMeasureBackfillObligation / sald.general_moving_target_discrete.cycle63_joint_endpoint_law_backfill.",
    "Source slice: appendix.tex:1354-1387, endpoint/common-space bookkeeping for the general EM interpolation before conditional drift and weak Fokker-Planck are used.",
    "Use local SLT material only as a style guide for Measure.map and a.e. equality patterns, especially SLT/SmallBallProb.lean and SLT/GaussianMeasure.lean; no SLT theorem is imported or marked as a SALD backend.",
    "The paired pushforward and marginal helpers may be used later to keep two endpoint representatives on one common probability space, but they do not prove Brownian construction, regular conditional drift, density/AC, weak Fokker-Planck, KL differentiation, or stitched Gronwall regularity."
  ]
  reviewerChecklist := [
    "SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle63UnifiedDiscreteGeneralSkeletonObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag include SALD.cycle63UnifiedDiscreteGeneralDag with ASTIS.SALD.unified_discrete_general.cycle63_upper_route and ASTIS.SALD.general_moving_target_discrete.cycle63_joint_endpoint_law_backfill.",
    "SALD.saldDependenciesForLabel for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete includes the cycle-63 packet, obligation, DAG, and paired Measure.map backfill.",
    "AutoSamplingTheory.lawMapProdEqOfAEEq and AutoSamplingTheory.lawMapProdFst/Snd compile as local measure helpers, but the EM interpolation Fokker-Planck backend and theorem statuses remain below formalized.",
    "The conversion window, proof-obligation ledger, and SLT reuse audit record the global phase judgment, five-backend check, theorem route, lower packet, and no-SLT-import status.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-63 upper obligation for the unified/discrete general route refresh. -/