AutoSamplingTheory.SALD.cycle52GuidedGeneralSkeletonUpperPacket

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 cycle52GuidedGeneralSkeletonUpperPacket : 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 52 upper: after the cycle-50 continuous forward-KL route and cycle-51 discrete forward-KL route, close the guided residual and continuous general moving-target theorem skeleton by explicitly consuming the five source-cited analytic interfaces and the already named guided/general obligations over appendix.tex:619-951.

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. faithfulPaper Phase 1: preserve appendix.tex:619-951 exactly as a theorem-level route; sald_version_2.tex remains out of scope.
2. Five-backend check 1, Gronwall: SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and SALD.gronwallAnalyticObligation expose endpoint-safe differentiability, FTC, coefficient regularity, and exponent rewrite obligations.
3. Five-backend check 2, DV: dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, and SALD.generalMovingTargetDvPositiveAlphaScalingContract expose common-space, absolute-continuity, finite-KL, finite-log-mgf, measurability, and positive-alpha scaling.
4. Five-backend check 3, LSI/KL/FI: SALD.saldLsiKlFiDensityTestContract and SALD.lsiKlFiDensityTestObligation expose density, zero-set convention, admissible sqrt-density test, entropy identity, and Fisher chain-rule obligations.
5. 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, boundary, transport, finite KL/FI, sigma, and schedule side conditions explicit.
6. Five-backend check 5, EM interpolation: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, and SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation keep endpoint laws, conditional drift, conditional-law density, weak Fokker-Planck, and stitched interval interfaces explicit for downstream discrete reuse.

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 or thm:general-moving-target-SALD, and do not promote SALD.guidedResidualContract or SALD.generalVaSaldContract above contractOnly.
2. Do not prove or replace the Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, EM interpolation, guided normalizer, divergence-linearity, or integration-by-parts backends in this upper packet.
3. Do not introduce a direct VA-SALD proof, path-space comparison, Girsanov, Pinsker, Talagrand, PI, or SLT-based proof route.
4. Do not start systematic measure-theory or SDE backfill until the theorem-level guided/general route remains stable under review.

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 row for SALD.cycle52GuidedGeneralSkeletonUpperPacket / SALD.cycle52GuidedGeneralSkeletonObligation.
2. Preferred lower target: SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative over appendix.tex:765-884.
3. First lower sub-slice: expose the density/law, general Fokker-Planck, mass conservation, target transport velocity, and integration-by-parts interfaces needed before Young, LSI, DV, and Gronwall.
4. Alternative lower target: SALD.guidedResidualIdentityContract / sald.guided_path_residual.identity, only for the normalizer derivative, product/quotient differentiation, divergence cancellation, and mean-zero residual from appendix.tex:630-704.
5. If a backend is too large, sharpen the named source-cited or obligation interface with the missing regularity, common-space, absolute-continuity, finite-quantity, endpoint, or coefficient hypotheses instead of changing a theorem statement.

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.cycle52GuidedGeneralSkeletonObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle52_upper_route after the cycle-47 route and before the downstream unified/discrete reuse nodes.
3. SALD.saldDependenciesForLabel entries for prop:guided_path_residual and thm:general-moving-target-SALD include the cycle-52 packet, obligation, and DAG route 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 cycle52GuidedGeneralSkeletonUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Cycle 52 upper: after the cycle-50 continuous forward-KL route and cycle-51 discrete forward-KL route, close the guided residual and continuous general moving-target theorem skeleton by explicitly consuming the five source-cited analytic interfaces and the already named guided/general obligations over appendix.tex:619-951."
  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 := [
    "faithfulPaper Phase 1: preserve appendix.tex:619-951 exactly as a theorem-level route; sald_version_2.tex remains out of scope.",
    "Five-backend check 1, Gronwall: SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and SALD.gronwallAnalyticObligation expose endpoint-safe differentiability, FTC, coefficient regularity, and exponent rewrite obligations.",
    "Five-backend check 2, DV: dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, and SALD.generalMovingTargetDvPositiveAlphaScalingContract expose common-space, absolute-continuity, finite-KL, finite-log-mgf, measurability, and positive-alpha scaling.",
    "Five-backend check 3, LSI/KL/FI: SALD.saldLsiKlFiDensityTestContract and SALD.lsiKlFiDensityTestObligation expose density, zero-set convention, admissible sqrt-density test, entropy identity, and Fisher chain-rule obligations.",
    "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, boundary, transport, finite KL/FI, sigma, and schedule side conditions explicit.",
    "Five-backend check 5, EM interpolation: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, and SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation keep endpoint laws, conditional drift, conditional-law density, weak Fokker-Planck, and stitched interval interfaces explicit for downstream discrete reuse."
  ]
  nonGoals := [
    "Do not restate prop:guided_path_residual or thm:general-moving-target-SALD, and do not promote SALD.guidedResidualContract or SALD.generalVaSaldContract above contractOnly.",
    "Do not prove or replace the Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, EM interpolation, guided normalizer, divergence-linearity, or integration-by-parts backends in this upper packet.",
    "Do not introduce a direct VA-SALD proof, path-space comparison, Girsanov, Pinsker, Talagrand, PI, or SLT-based proof route.",
    "Do not start systematic measure-theory or SDE backfill until the theorem-level guided/general route remains stable under review."
  ]
  lowerPacket := [
    "Middle should synchronize the conversion window and proof-obligation row for SALD.cycle52GuidedGeneralSkeletonUpperPacket / SALD.cycle52GuidedGeneralSkeletonObligation.",
    "Preferred lower target: SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative over appendix.tex:765-884.",
    "First lower sub-slice: expose the density/law, general Fokker-Planck, mass conservation, target transport velocity, and integration-by-parts interfaces needed before Young, LSI, DV, and Gronwall.",
    "Alternative lower target: SALD.guidedResidualIdentityContract / sald.guided_path_residual.identity, only for the normalizer derivative, product/quotient differentiation, divergence cancellation, and mean-zero residual from appendix.tex:630-704.",
    "If a backend is too large, sharpen the named source-cited or obligation interface with the missing regularity, common-space, absolute-continuity, finite-quantity, endpoint, or coefficient hypotheses instead of changing a theorem statement."
  ]
  reviewerChecklist := [
    "SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle52GuidedGeneralSkeletonObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle52_upper_route after the cycle-47 route and before the downstream unified/discrete reuse nodes.",
    "SALD.saldDependenciesForLabel entries for prop:guided_path_residual and thm:general-moving-target-SALD include the cycle-52 packet, obligation, and DAG route 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-52 obligation tying the guided residual and continuous general
moving-target theorem route to the five explicit analytic backends. -/