AutoSamplingTheory.SALD.cycle20GeneralVaSaldUpperPacket

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 cycle20GeneralVaSaldUpperPacket : 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 discrete general Gronwall side-condition/display bridge as the next lower target: stitched endpoint laws, constant-schedule coefficient rewrites, coefficient regularity, and exact matching of appendix.tex:1586-1600 to the theorem display appendix.tex:1316-1347.

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. eq:SALD_general_EM
6. lem:frozen_delta_cross_lip
7. lem:gronwall

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use appendix.tex:1313-1603 for the discrete general theorem, with appendix.tex:724-951 and main_body.tex:359-395 only as fixed upstream guided/general dependencies; sald_version_2.tex remains out of scope.
2. Preserve the exact theorem-display coefficients: (sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t), 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1), 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t), and b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t).
3. Keep the source route interval EM derivative -> residual/frozen split -> DV/LSI -> s-to-t time change -> lem:gronwall; continuous general VA-SALD and unified VA-SALD remain dependencies, not alternate proof routes.
4. Treat endpoint stitching, constant inverse-schedule algebra, coefficient integrability, piecewise differentiability of K(t), 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 restate or prove thm:general-moving-target-SALD-discrete in this packet.
2. Do not reopen the frozen-delta lemma, residual DV finite-log-mgf witness, LSI-to-KL/FI bridge, or KL derivative proof except as dependencies of the final Gronwall side-condition ledger.
3. Do not turn the discrete guided specialization into a direct VA-SALD proof; it remains the source replacement c<-u after the general theorem.
4. Do not simplify away the doubled residual coefficient, the Gamma/Delta terms, alpha, alpha', eta, sigma_eta, or the constant-schedule hypothesis.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.generalMovingTargetDiscreteGronwallSideConditionContract / SALD.generalMovingTargetDiscreteGronwallSideConditionObligation / sald.general_moving_target_discrete.gronwall_side_conditions.
2. Refine one lower sub-slice only: endpoint stitching for K(0)/K(T), constant-schedule coefficient rewrites, coefficient regularity for a(t), b(t), or exact Gronwall-display matching.
3. Preserve appendix.tex:1586-1597 and theorem display appendix.tex:1316-1347 verbatim at the contract level; bridge them by explicit endpoint, schedule, and coefficient lemmas.
4. If stitched EM regularity, endpoint laws, interval-integrability, or schedule algebra is blocked, record the precise source-contract gap rather than adding theorem hypotheses.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.generalVaSaldDiscreteProofDag contains ASTIS.SALD.general_moving_target_discrete.cycle20_upper_packet before the gronwall_side_conditions block.
2. SALD.saldDependenciesForLabel "thm:general-moving-target-SALD-discrete" includes SALD.cycle20GeneralVaSaldUpperPacket while retaining the existing discrete EM, frozen-delta, DV, derivative, and Gronwall obligations.
3. SALD.generalVaSaldDiscreteContract remains contractOnly and the named gronwall-side-condition obligation remains an obligation.
4. The conversion window, proof-obligation ledger, SLT audit, and source index classify this as workflow/local algebra work and keep sald_version_2.tex excluded.
5. No analytic dependency is marked formalized and no fake proof closure is introduced.

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 cycle20GeneralVaSaldUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Return to the guided/general VA-SALD path and select the discrete general Gronwall side-condition/display bridge as the next lower target: stitched endpoint laws, constant-schedule coefficient rewrites, coefficient regularity, and exact matching of appendix.tex:1586-1600 to the theorem display appendix.tex:1316-1347."
  sourceLabels := [
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete",
    "eq:SALD_general_EM",
    "lem:frozen_delta_cross_lip",
    "lem:gronwall"
  ]
  modeDiscipline := [
    "faithfulPaper: use appendix.tex:1313-1603 for the discrete general theorem, with appendix.tex:724-951 and main_body.tex:359-395 only as fixed upstream guided/general dependencies; sald_version_2.tex remains out of scope.",
    "Preserve the exact theorem-display coefficients: (sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t), 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1), 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t), and b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t).",
    "Keep the source route interval EM derivative -> residual/frozen split -> DV/LSI -> s-to-t time change -> lem:gronwall; continuous general VA-SALD and unified VA-SALD remain dependencies, not alternate proof routes.",
    "Treat endpoint stitching, constant inverse-schedule algebra, coefficient integrability, piecewise differentiability of K(t), and Gronwall as obligations until compiled Lean proofs replace them."
  ]
  nonGoals := [
    "Do not restate or prove thm:general-moving-target-SALD-discrete in this packet.",
    "Do not reopen the frozen-delta lemma, residual DV finite-log-mgf witness, LSI-to-KL/FI bridge, or KL derivative proof except as dependencies of the final Gronwall side-condition ledger.",
    "Do not turn the discrete guided specialization into a direct VA-SALD proof; it remains the source replacement c<-u after the general theorem.",
    "Do not simplify away the doubled residual coefficient, the Gamma/Delta terms, alpha, alpha', eta, sigma_eta, or the constant-schedule hypothesis."
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteGronwallSideConditionContract / SALD.generalMovingTargetDiscreteGronwallSideConditionObligation / sald.general_moving_target_discrete.gronwall_side_conditions.",
    "Refine one lower sub-slice only: endpoint stitching for K(0)/K(T), constant-schedule coefficient rewrites, coefficient regularity for a(t), b(t), or exact Gronwall-display matching.",
    "Preserve appendix.tex:1586-1597 and theorem display appendix.tex:1316-1347 verbatim at the contract level; bridge them by explicit endpoint, schedule, and coefficient lemmas.",
    "If stitched EM regularity, endpoint laws, interval-integrability, or schedule algebra is blocked, record the precise source-contract gap rather than adding theorem hypotheses."
  ]
  reviewerChecklist := [
    "SALD.generalVaSaldDiscreteProofDag contains ASTIS.SALD.general_moving_target_discrete.cycle20_upper_packet before the gronwall_side_conditions block.",
    "SALD.saldDependenciesForLabel \"thm:general-moving-target-SALD-discrete\" includes SALD.cycle20GeneralVaSaldUpperPacket while retaining the existing discrete EM, frozen-delta, DV, derivative, and Gronwall obligations.",
    "SALD.generalVaSaldDiscreteContract remains contractOnly and the named gronwall-side-condition obligation remains an obligation.",
    "The conversion window, proof-obligation ledger, SLT audit, and source index classify this as workflow/local algebra work and keep sald_version_2.tex excluded.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-20 middle packet for the discrete general VA-SALD Gronwall bridge.

This translates the upper-selected target into a lower-ready source-to-Lean map
for `sald.general_moving_target_discrete.gronwall_side_conditions`.  It keeps
the theorem statement fixed and separates endpoint stitching, constant-schedule
coefficient rewrites, Gronwall regularity, and display matching from the
upstream EM, frozen-delta, DV, LSI, and derivative obligations.
-/