AutoSamplingTheory.SALD.cycle57GuidedGeneralSkeletonUpperPacket

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 cycle57GuidedGeneralSkeletonUpperPacket : 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 57 upper: previous cycle 56 passed reviewer and build gate, so no recovery is needed; Phase 1 is stable for the forward-KL and discrete forward-KL routes but not yet stable enough for broad cited-theory backfill until the guided residual and continuous general moving-target route is rechecked; the single lower packet that best reduces risk is sald.general_moving_target.kl_derivative over appendix.tex:765-884.

sourceLabels : List String (explicit)

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

Ordered data items

1. prop:guided_path_residual
2. proof:prop:guided_path_residual
3. thm:general-moving-target-SALD
4. eq:general_moving_target_SALD
5. eq:general_moving_target_FP
6. proof:thm:general-moving-target-SALD:derivative
7. proof:thm:general-moving-target-SALD:residual-dv
8. proof:thm:general-moving-target-SALD:dv-gronwall
9. proof:thm:general-moving-target-SALD:pure-contraction
10. proof:thm:unified-forward-KL
11. eq:LSI-KL-FI
12. lem:dv_variation
13. lem:gronwall
14. 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 56 did not fail and needs no recovery; the route is ready to advance from discrete forward-KL recovery back to guided/general theorem skeleton closure.
2. Global phase judgment: do not begin broad cited-theory backfill yet; only after prop:guided_path_residual and thm:general-moving-target-SALD are rechecked against appendix.tex:619-951 should one narrow backend at a time be selected.
3. Global phase judgment: the largest current proof risk is the continuous general Fokker-Planck/KL derivative backend, because it feeds the residual Young/LSI/DV/Gronwall chain and later unified/discrete general reuse.
4. Five-backend check 1, Gronwall: SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and SALD.gronwallAnalyticObligation keep endpoint-safe differentiability, FTC, coefficient regularity, and exponent side conditions explicit.
5. Five-backend check 2, DV: dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, and SALD.generalMovingTargetDvPositiveAlphaScalingContract keep common-space, absolute-continuity, finite-KL, finite-log-mgf, measurable residual test, and positive-alpha scaling 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, entropy identity, finite KL/FI, and Fisher chain-rule obligations explicit.
7. Five-backend check 4, continuous derivative: SALD.forwardKlDerivativeCandidateContract and SALD.generalMovingTargetDerivativeCandidateContract keep the Fokker-Planck/KL derivative identities source-cited or obligation-level, with density, mass, boundary, transport, sigma, and schedule side conditions explicit.
8. Five-backend check 5, EM interpolation: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, and sald.general_moving_target_discrete.em_interpolation_fp remain downstream endpoint/conditional-law Fokker-Planck interfaces and are not imported into the continuous theorem statement.
9. FaithfulPaper Phase 1: use appendix.tex:619-951 only for this guided/general route; 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 prop:guided_path_residual, thm:general-moving-target-SALD, or thm:unified-forward-KL.
2. Do not promote SALD.guidedResidualContract, SALD.generalVaSaldContract, or any slow analytic interface above contractOnly/sourceCited/obligation.
3. Do not replace the source route by a direct VA-SALD proof, path-space comparison, Girsanov, Pinsker, Talagrand, PI, or SLT-based proof.
4. Do not start systematic measure-theory or SDE backfill in this upper cycle; keep any missing analytic fact as a precise source-cited interface or obligation.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle should synchronize this cycle-57 upper route with conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and the guided/general proof DAG.
2. Lower should target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative over appendix.tex:765-884.
3. First lower sub-slice: appendix.tex:765-812, exposing law regularity, mass conservation, the general moving-target Fokker-Planck equation, KL differentiation under the integral, and integration-by-parts side conditions.
4. Second lower sub-slice: appendix.tex:813-864, exposing target transport by v_t, rescaled transport of pi_{t(s)}, residual m_t=v_t-c_t, and Young with epsilon=2*dot t(s)/sigma_{t(s)}^2.
5. Third lower sub-slice: appendix.tex:865-884, preserving the LSI handoff and s-to-t schedule/sigma side conditions without adding them to the theorem statement.
6. If the derivative backend is blocked, refine the named obligation with the exact density, boundary, common-space, finite-quantity, sigma-positivity, or schedule gap; do not weaken the source theorem.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle57GuidedGeneralSkeletonObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle57_upper_route after the cycle-52 guided/general route and before downstream unified/discrete reuse.
3. SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-57 packet, obligation, DAG node, and selected lower-packet node.
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. 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 cycle57GuidedGeneralSkeletonUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Cycle 57 upper: previous cycle 56 passed reviewer and build gate, so no recovery is needed; Phase 1 is stable for the forward-KL and discrete forward-KL routes but not yet stable enough for broad cited-theory backfill until the guided residual and continuous general moving-target route is rechecked; the single lower packet that best reduces risk is sald.general_moving_target.kl_derivative over appendix.tex:765-884."
  sourceLabels := [
    "prop:guided_path_residual",
    "proof:prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "eq:general_moving_target_SALD",
    "eq:general_moving_target_FP",
    "proof:thm:general-moving-target-SALD:derivative",
    "proof:thm:general-moving-target-SALD:residual-dv",
    "proof:thm:general-moving-target-SALD:dv-gronwall",
    "proof:thm:general-moving-target-SALD:pure-contraction",
    "proof:thm:unified-forward-KL",
    "eq:LSI-KL-FI",
    "lem:dv_variation",
    "lem:gronwall",
    "def:alpha-complexity"
  ]
  modeDiscipline := [
    "Global phase judgment: cycle 56 did not fail and needs no recovery; the route is ready to advance from discrete forward-KL recovery back to guided/general theorem skeleton closure.",
    "Global phase judgment: do not begin broad cited-theory backfill yet; only after prop:guided_path_residual and thm:general-moving-target-SALD are rechecked against appendix.tex:619-951 should one narrow backend at a time be selected.",
    "Global phase judgment: the largest current proof risk is the continuous general Fokker-Planck/KL derivative backend, because it feeds the residual Young/LSI/DV/Gronwall chain and later unified/discrete general reuse.",
    "Five-backend check 1, Gronwall: SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and SALD.gronwallAnalyticObligation keep endpoint-safe differentiability, FTC, coefficient regularity, and exponent side conditions explicit.",
    "Five-backend check 2, DV: dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, and SALD.generalMovingTargetDvPositiveAlphaScalingContract keep common-space, absolute-continuity, finite-KL, finite-log-mgf, measurable residual test, and positive-alpha scaling 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, entropy identity, finite KL/FI, and Fisher chain-rule obligations explicit.",
    "Five-backend check 4, continuous derivative: SALD.forwardKlDerivativeCandidateContract and SALD.generalMovingTargetDerivativeCandidateContract keep the Fokker-Planck/KL derivative identities source-cited or obligation-level, with density, mass, boundary, transport, sigma, and schedule side conditions explicit.",
    "Five-backend check 5, EM interpolation: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, and sald.general_moving_target_discrete.em_interpolation_fp remain downstream endpoint/conditional-law Fokker-Planck interfaces and are not imported into the continuous theorem statement.",
    "FaithfulPaper Phase 1: use appendix.tex:619-951 only for this guided/general route; sald_version_2.tex remains excluded."
  ]
  nonGoals := [
    "Do not restate prop:guided_path_residual, thm:general-moving-target-SALD, or thm:unified-forward-KL.",
    "Do not promote SALD.guidedResidualContract, SALD.generalVaSaldContract, or any slow analytic interface above contractOnly/sourceCited/obligation.",
    "Do not replace the source route by a direct VA-SALD proof, path-space comparison, Girsanov, Pinsker, Talagrand, PI, or SLT-based proof.",
    "Do not start systematic measure-theory or SDE backfill in this upper cycle; keep any missing analytic fact as a precise source-cited interface or obligation."
  ]
  lowerPacket := [
    "Middle should synchronize this cycle-57 upper route with conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and the guided/general proof DAG.",
    "Lower should target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative over appendix.tex:765-884.",
    "First lower sub-slice: appendix.tex:765-812, exposing law regularity, mass conservation, the general moving-target Fokker-Planck equation, KL differentiation under the integral, and integration-by-parts side conditions.",
    "Second lower sub-slice: appendix.tex:813-864, exposing target transport by v_t, rescaled transport of pi_{t(s)}, residual m_t=v_t-c_t, and Young with epsilon=2*dot t(s)/sigma_{t(s)}^2.",
    "Third lower sub-slice: appendix.tex:865-884, preserving the LSI handoff and s-to-t schedule/sigma side conditions without adding them to the theorem statement.",
    "If the derivative backend is blocked, refine the named obligation with the exact density, boundary, common-space, finite-quantity, sigma-positivity, or schedule gap; do not weaken the source theorem."
  ]
  reviewerChecklist := [
    "SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle57GuidedGeneralSkeletonObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle57_upper_route after the cycle-52 guided/general route and before downstream unified/discrete reuse.",
    "SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-57 packet, obligation, DAG node, and selected lower-packet node.",
    "The five slow analytic interfaces remain source-cited or obligation-level; no theorem statement, source constant, source label, or external reuse status changes.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-57 obligation for the upper guided/general route recheck. -/