AutoSamplingTheory.SALD.cycle47GuidedGeneralSkeletonUpperPacket

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 cycle47GuidedGeneralSkeletonUpperPacket : 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 4: wire prop:guided_path_residual and thm:general-moving-target-SALD to the already named analytic interfaces, matching appendix.tex:619-951 without changing the paper proposition, theorem statement, constants, or source labels.

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: use only appendix.tex:619-951 and the original main_body.tex guided/unified references; sald_version_2.tex remains out of scope.
2. Before lower work, the five slow backends are checked as explicit interfaces: Gronwall endpoint calculus, DV common-space/finite-log-mgf, LSI/KL/FI density-test, continuous Fokker-Planck/KL derivative, and EM interpolation Fokker-Planck for downstream discrete reuse.
3. The source route is guided normalizer derivative -> centered residual identity -> general moving-target KL derivative -> LSI -> residual DV -> Gronwall -> theorem display -> pure contraction; the unified theorem remains only the one-line c_t<-u_t specialization.
4. All missing density, boundary, positivity, finite-KL/FI, finite-log-mgf, endpoint, coefficient-regularity, and divergence-linearity facts remain named obligations rather than hidden theorem assumptions.

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, guided normalizer, or divergence/integration-by-parts analytic backends in this upper packet.
3. Do not replace the paper route with a direct VA-SALD proof, path-space comparison, Girsanov, Pinsker, Talagrand, or PI-based argument.
4. Do not start systematic SLT or measure-theory backfill before the guided/general theorem-level route is stable.

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 this cycle-47 guided/general theorem wrapper.
2. Lower should target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative after the route wrapper is accepted.
3. The lower sub-slice should preserve appendix.tex:765-884: KL differentiation, the general VA-SALD Fokker-Planck equation, target transport by v_t, the residual m_t=v_t-c_t, Young with epsilon=2*dot{t}(s)/sigma_{t(s)}^2, LSI, and time change.
4. If that backend is too large, sharpen the source-cited or obligation interface with density/law regularity, integration-by-parts, transport, finite KL/FI, sigma and schedule positivity, and inverse-schedule hypotheses instead of changing the 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 the cycle-47 theorem-route obligations while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle47_theorem_skeleton_route before the lower guided residual and general moving-target nodes.
3. SALD.saldDependenciesForLabel entries for prop:guided_path_residual and thm:general-moving-target-SALD include the cycle-47 packet, obligations, and DAG nodes.
4. No analytic backend status is promoted, no source theorem statement or source constant changes, and no alternate proof route is introduced.
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 cycle47GuidedGeneralSkeletonUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Main skeleton sprint 4: wire prop:guided_path_residual and thm:general-moving-target-SALD to the already named analytic interfaces, matching appendix.tex:619-951 without changing the paper proposition, theorem statement, constants, or source labels."
  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: use only appendix.tex:619-951 and the original main_body.tex guided/unified references; sald_version_2.tex remains out of scope.",
    "Before lower work, the five slow backends are checked as explicit interfaces: Gronwall endpoint calculus, DV common-space/finite-log-mgf, LSI/KL/FI density-test, continuous Fokker-Planck/KL derivative, and EM interpolation Fokker-Planck for downstream discrete reuse.",
    "The source route is guided normalizer derivative -> centered residual identity -> general moving-target KL derivative -> LSI -> residual DV -> Gronwall -> theorem display -> pure contraction; the unified theorem remains only the one-line c_t<-u_t specialization.",
    "All missing density, boundary, positivity, finite-KL/FI, finite-log-mgf, endpoint, coefficient-regularity, and divergence-linearity facts remain named obligations rather than hidden theorem assumptions."
  ]
  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, guided normalizer, or divergence/integration-by-parts analytic backends in this upper packet.",
    "Do not replace the paper route with a direct VA-SALD proof, path-space comparison, Girsanov, Pinsker, Talagrand, or PI-based argument.",
    "Do not start systematic SLT or measure-theory backfill before the guided/general theorem-level route is stable."
  ]
  lowerPacket := [
    "Middle should synchronize the conversion window and proof-obligation row for this cycle-47 guided/general theorem wrapper.",
    "Lower should target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative after the route wrapper is accepted.",
    "The lower sub-slice should preserve appendix.tex:765-884: KL differentiation, the general VA-SALD Fokker-Planck equation, target transport by v_t, the residual m_t=v_t-c_t, Young with epsilon=2*dot{t}(s)/sigma_{t(s)}^2, LSI, and time change.",
    "If that backend is too large, sharpen the source-cited or obligation interface with density/law regularity, integration-by-parts, transport, finite KL/FI, sigma and schedule positivity, and inverse-schedule hypotheses instead of changing the theorem statement."
  ]
  reviewerChecklist := [
    "SALD.guidedResidualContract and SALD.generalVaSaldContract list the cycle-47 theorem-route obligations while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle47_theorem_skeleton_route before the lower guided residual and general moving-target nodes.",
    "SALD.saldDependenciesForLabel entries for prop:guided_path_residual and thm:general-moving-target-SALD include the cycle-47 packet, obligations, and DAG nodes.",
    "No analytic backend status is promoted, no source theorem statement or source constant changes, and no 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-47 obligation tying the guided residual and continuous general
moving-target theorem skeleton to the already named analytic interfaces. -/