AutoSamplingTheory.SALD.cycle28GeneralVaSaldUpperPacket

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 cycle28GeneralVaSaldUpperPacket : 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 derivative side-condition bridge as the next lower target: EM endpoint laws, conditional-drift Fokker--Planck split, slowed transport velocity, frozen/residual algebra, the two sigma_eta^2/8 Young splits, LSI bookkeeping, residual DV witness handoff, and stitched time-change interfaces from appendix.tex:1354-1598.

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. eq:general_moving_target_SALD_frozen_interp
7. eq:general_discrete_delta_def
8. lem:frozen_delta_cross_lip
9. eq:LSI-KL-FI
10. lem:dv_variation

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use appendix.tex:1354-1598 for the discrete derivative route, appendix.tex:1313-1347 for the fixed theorem display, and appendix.tex:724-951 plus main_body.tex:359-395 only as upstream guided/general dependencies; sald_version_2.tex remains out of scope.
2. Preserve the source decomposition (sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s = delta_pi^VA + dot{t}(s)*m_{t(s)} and the two Young splits with sigma_eta^2/8 each.
3. Keep the resulting coefficients exactly: 2*sigma_eta^(-2)*dot{t}(s)^2 on the residual energy, 2*Gamma(t(s))*eta^2*alpha'^(-1) on KL, and 2*Delta(t(s))*eta as the additive frozen-delta term before time change.
4. Treat EM endpoint laws, conditional drift/disintegration, Fokker--Planck, integration by parts, LSI-to-KL/FI, residual DV finite-log-mgf, stitched time change, and later 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, thm:general-moving-target-SALD, or thm:unified-forward-KL in this packet.
2. Do not reopen the final Gronwall display bridge selected in cycle 20 except as a downstream dependency of the derivative inequality.
3. Do not replace the paper's EM interval derivative route with a path-space, Girsanov, Pinsker, Talagrand, or direct guided VA-SALD proof.
4. Do not simplify away the doubled residual coefficient, the Gamma/Delta terms, alpha, alpha', eta, sigma_eta, dot{t}, dot{s}, 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.generalMovingTargetDiscreteDerivativeSideConditionContract / SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation / sald.general_moving_target_discrete.derivative_side_conditions.
2. Preferred first lower sub-slice: appendix.tex:1469-1511, proving or refining only the frozen/residual algebra and Young coefficient bookkeeping that yields the residual coefficient 2*sigma_eta^(-2)*dot{t}(s)^2 and frozen coefficients 2*Gamma*eta^2*alpha'^(-1), 2*Delta*eta.
3. Keep endpoint laws, conditional Fokker--Planck, LSI-to-KL/FI, residual DV finite-log-mgf, s-to-t time change, and Gronwall as named dependencies unless a separate compiled proof handles exactly one of them.
4. If conditional drift, divergence/integration-by-parts, slowed transport velocity, or stitched regularity is blocked, refine the corresponding source-contract gap rather than adding assumptions to the theorem statement.

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.cycle28_upper_derivative_side_conditions before the derivative_side_conditions block.
2. SALD.saldDependenciesForLabel "thm:general-moving-target-SALD-discrete" includes SALD.cycle28GeneralVaSaldUpperPacket while retaining cycle-20 Gronwall and all existing EM, frozen-delta, DV, derivative, and Gronwall obligations.
3. SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation remains an obligation and preserves appendix.tex:1469-1511 source coefficients exactly.
4. The unified theorem remains only the source specialization c_t<-u_t after the correction-field transport bridge; no direct VA-SALD proof route is introduced.
5. The conversion window, proof-obligation ledger, SLT audit, 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 cycle28GeneralVaSaldUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Return to the guided/general VA-SALD path and select the discrete general derivative side-condition bridge as the next lower target: EM endpoint laws, conditional-drift Fokker--Planck split, slowed transport velocity, frozen/residual algebra, the two sigma_eta^2/8 Young splits, LSI bookkeeping, residual DV witness handoff, and stitched time-change interfaces from appendix.tex:1354-1598."
  sourceLabels := [
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete",
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "lem:frozen_delta_cross_lip",
    "eq:LSI-KL-FI",
    "lem:dv_variation"
  ]
  modeDiscipline := [
    "faithfulPaper: use appendix.tex:1354-1598 for the discrete derivative route, appendix.tex:1313-1347 for the fixed theorem display, and appendix.tex:724-951 plus main_body.tex:359-395 only as upstream guided/general dependencies; sald_version_2.tex remains out of scope.",
    "Preserve the source decomposition (sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s = delta_pi^VA + dot{t}(s)*m_{t(s)} and the two Young splits with sigma_eta^2/8 each.",
    "Keep the resulting coefficients exactly: 2*sigma_eta^(-2)*dot{t}(s)^2 on the residual energy, 2*Gamma(t(s))*eta^2*alpha'^(-1) on KL, and 2*Delta(t(s))*eta as the additive frozen-delta term before time change.",
    "Treat EM endpoint laws, conditional drift/disintegration, Fokker--Planck, integration by parts, LSI-to-KL/FI, residual DV finite-log-mgf, stitched time change, and later Gronwall as obligations until compiled Lean proofs replace them."
  ]
  nonGoals := [
    "Do not restate or prove thm:general-moving-target-SALD-discrete, thm:general-moving-target-SALD, or thm:unified-forward-KL in this packet.",
    "Do not reopen the final Gronwall display bridge selected in cycle 20 except as a downstream dependency of the derivative inequality.",
    "Do not replace the paper's EM interval derivative route with a path-space, Girsanov, Pinsker, Talagrand, or direct guided VA-SALD proof.",
    "Do not simplify away the doubled residual coefficient, the Gamma/Delta terms, alpha, alpha', eta, sigma_eta, dot{t}, dot{s}, or the constant-schedule hypothesis."
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation / sald.general_moving_target_discrete.derivative_side_conditions.",
    "Preferred first lower sub-slice: appendix.tex:1469-1511, proving or refining only the frozen/residual algebra and Young coefficient bookkeeping that yields the residual coefficient 2*sigma_eta^(-2)*dot{t}(s)^2 and frozen coefficients 2*Gamma*eta^2*alpha'^(-1), 2*Delta*eta.",
    "Keep endpoint laws, conditional Fokker--Planck, LSI-to-KL/FI, residual DV finite-log-mgf, s-to-t time change, and Gronwall as named dependencies unless a separate compiled proof handles exactly one of them.",
    "If conditional drift, divergence/integration-by-parts, slowed transport velocity, or stitched regularity is blocked, refine the corresponding source-contract gap rather than adding assumptions to the theorem statement."
  ]
  reviewerChecklist := [
    "SALD.generalVaSaldDiscreteProofDag contains ASTIS.SALD.general_moving_target_discrete.cycle28_upper_derivative_side_conditions before the derivative_side_conditions block.",
    "SALD.saldDependenciesForLabel \"thm:general-moving-target-SALD-discrete\" includes SALD.cycle28GeneralVaSaldUpperPacket while retaining cycle-20 Gronwall and all existing EM, frozen-delta, DV, derivative, and Gronwall obligations.",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation remains an obligation and preserves appendix.tex:1469-1511 source coefficients exactly.",
    "The unified theorem remains only the source specialization c_t<-u_t after the correction-field transport bridge; no direct VA-SALD proof route is introduced.",
    "The conversion window, proof-obligation ledger, SLT audit, source index, and dialogue handoff stay synchronized, sald_version_2.tex is excluded, and python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-28 middle packet for the discrete general VA-SALD derivative side.

This translates the upper-selected source slice `appendix.tex:1469-1511` into a
lower-ready source-to-Lean map.  It keeps the theorem display fixed and narrows
lower work to the frozen/residual decomposition plus the two Young coefficient
splits before LSI, DV, time change, or Gronwall proof search.
-/