AutoSamplingTheory.SALD.cycle24GeneralVaSaldUpperPacket

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

Return to the guided/general VA-SALD path and select the continuous general moving-target Gronwall endpoint/exponent/pure-contraction side-condition bridge as the next lower target: K(0)/K(T) endpoint rewrites, sigma-weighted coefficient regularity, exponent splitting, residual-exponent monotonicity, and the zero-residual alpha-complexity specialization in appendix.tex:909-945.

sourceLabels : List String (explicit)

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

Ordered data items

1. prop:guided_path_residual
2. thm:general-moving-target-SALD
3. thm:unified-forward-KL
4. thm:general-moving-target-SALD-discrete
5. lem:dv_variation
6. lem:gronwall
7. eq:LSI-KL-FI
8. def:alpha-complexity

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use appendix.tex:724-951 for the continuous general theorem, main_body.tex:359-395 for the unified specialization, and appendix.tex:1313-1603 only as downstream discrete reuse; sald_version_2.tex remains out of scope.
2. Preserve the exact continuous coefficients a(t)=(sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t).
3. Keep the source route derivative -> LSI -> residual DV -> Gronwall -> theorem display -> pure contraction; unified VA-SALD remains only the c_t<-u_t specialization with m_t=w_t.
4. Treat endpoint schedule identities, coefficient regularity, sign facts for dropping the LSI contribution, zero-residual alpha-complexity, DV, LSI, and Gronwall as obligations until compiled Lean proofs replace them.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not prove or restate thm:general-moving-target-SALD, thm:unified-forward-KL, or thm:general-moving-target-SALD-discrete in this packet.
2. Do not replace the sigma-weighted Gronwall route with the forward-KL proof, a discrete argument, Girsanov, Pinsker, Talagrand, or any path-space proof.
3. Do not add hidden endpoint, schedule, coefficient-integrability, density, boundary, finite-log-mgf, or sign assumptions to theorem statements.
4. Do not simplify away sigma_t, dot{s}(t), alpha, the residual alpha-complexity, the pure-contraction exponent factors, or the discrete doubled residual/Gamma/Delta coefficients.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.generalMovingTargetGronwallSideConditionContract / SALD.generalMovingTargetGronwallSideConditionObligation / sald.general_moving_target.gronwall_side_conditions.
2. First sub-slice for middle: classify appendix.tex:909-934 against theorem display appendix.tex:727-743, separating endpoint K(T)/K(0) rewrites, coefficient regularity for a(t), b(t), exponent split, and residual-exponent drop.
3. Alternative one-slice targets are endpoint schedule identities, theorem-specific interval-integrability of the sigma/LSI and alpha coefficient pieces, residual-exponent monotonicity, or appendix.tex:936-945 zero-residual alpha-complexity.
4. If any endpoint, regularity, sign, or alpha-complexity backend is blocked, refine the named proof obligation instead of strengthening the theorem or marking an analytic result formalized.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.generalVaSaldProofDag contains ASTIS.SALD.general_moving_target.cycle24_upper_packet before ASTIS.SALD.general_moving_target.gronwall_side_conditions.
2. SALD.saldDependenciesForLabel "thm:general-moving-target-SALD" and "thm:unified-forward-KL" include SALD.cycle24GeneralVaSaldUpperPacket while retaining the existing guided residual, DV, LSI, Gronwall, and transport-bridge obligations.
3. SALD.generalMovingTargetGronwallSideConditionObligation remains an obligation; no endpoint, coefficient regularity, residual exponent drop, pure-contraction, DV, LSI, or full Gronwall backend is promoted.
4. The unified theorem still follows only by setting c_t<-u_t with v_t=u_t+w_t and m_t=w_t; the discrete theorem remains under the cycle-20 Gronwall-side-condition packet.
5. The conversion window, proof-obligation ledger, source index, and dialogue handoff stay synchronized, sald_version_2.tex is excluded, and python3 tools/astis.py check passes.

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 cycle24GeneralVaSaldUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Return to the guided/general VA-SALD path and select the continuous general moving-target Gronwall endpoint/exponent/pure-contraction side-condition bridge as the next lower target: K(0)/K(T) endpoint rewrites, sigma-weighted coefficient regularity, exponent splitting, residual-exponent monotonicity, and the zero-residual alpha-complexity specialization in appendix.tex:909-945."
  sourceLabels := [
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete",
    "lem:dv_variation",
    "lem:gronwall",
    "eq:LSI-KL-FI",
    "def:alpha-complexity"
  ]
  modeDiscipline := [
    "faithfulPaper: use appendix.tex:724-951 for the continuous general theorem, main_body.tex:359-395 for the unified specialization, and appendix.tex:1313-1603 only as downstream discrete reuse; sald_version_2.tex remains out of scope.",
    "Preserve the exact continuous coefficients a(t)=(sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t).",
    "Keep the source route derivative -> LSI -> residual DV -> Gronwall -> theorem display -> pure contraction; unified VA-SALD remains only the c_t<-u_t specialization with m_t=w_t.",
    "Treat endpoint schedule identities, coefficient regularity, sign facts for dropping the LSI contribution, zero-residual alpha-complexity, DV, LSI, and Gronwall as obligations until compiled Lean proofs replace them."
  ]
  nonGoals := [
    "Do not prove or restate thm:general-moving-target-SALD, thm:unified-forward-KL, or thm:general-moving-target-SALD-discrete in this packet.",
    "Do not replace the sigma-weighted Gronwall route with the forward-KL proof, a discrete argument, Girsanov, Pinsker, Talagrand, or any path-space proof.",
    "Do not add hidden endpoint, schedule, coefficient-integrability, density, boundary, finite-log-mgf, or sign assumptions to theorem statements.",
    "Do not simplify away sigma_t, dot{s}(t), alpha, the residual alpha-complexity, the pure-contraction exponent factors, or the discrete doubled residual/Gamma/Delta coefficients."
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetGronwallSideConditionContract / SALD.generalMovingTargetGronwallSideConditionObligation / sald.general_moving_target.gronwall_side_conditions.",
    "First sub-slice for middle: classify appendix.tex:909-934 against theorem display appendix.tex:727-743, separating endpoint K(T)/K(0) rewrites, coefficient regularity for a(t), b(t), exponent split, and residual-exponent drop.",
    "Alternative one-slice targets are endpoint schedule identities, theorem-specific interval-integrability of the sigma/LSI and alpha coefficient pieces, residual-exponent monotonicity, or appendix.tex:936-945 zero-residual alpha-complexity.",
    "If any endpoint, regularity, sign, or alpha-complexity backend is blocked, refine the named proof obligation instead of strengthening the theorem or marking an analytic result formalized."
  ]
  reviewerChecklist := [
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.general_moving_target.cycle24_upper_packet before ASTIS.SALD.general_moving_target.gronwall_side_conditions.",
    "SALD.saldDependenciesForLabel \"thm:general-moving-target-SALD\" and \"thm:unified-forward-KL\" include SALD.cycle24GeneralVaSaldUpperPacket while retaining the existing guided residual, DV, LSI, Gronwall, and transport-bridge obligations.",
    "SALD.generalMovingTargetGronwallSideConditionObligation remains an obligation; no endpoint, coefficient regularity, residual exponent drop, pure-contraction, DV, LSI, or full Gronwall backend is promoted.",
    "The unified theorem still follows only by setting c_t<-u_t with v_t=u_t+w_t and m_t=w_t; the discrete theorem remains under the cycle-20 Gronwall-side-condition packet.",
    "The conversion window, proof-obligation ledger, source index, and dialogue handoff stay synchronized, sald_version_2.tex is excluded, and python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-24 middle packet for the continuous general VA-SALD Gronwall bridge.

This translates the upper-selected target into a lower-ready source-to-Lean map
for `sald.general_moving_target.gronwall_side_conditions`.  It keeps the
continuous general theorem, unified specialization, and downstream discrete
reuse fixed while separating endpoint rewrites, coefficient regularity,
exponent splitting, residual-exponent monotonicity, and pure-contraction
alpha-complexity from the upstream derivative, LSI, DV, and Gronwall
obligations.
-/