AutoSamplingTheory.SALD.cycle16GeneralVaSaldUpperPacket

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

Keep the guided/general VA-SALD theorem statements fixed and select the unified transport-velocity bridge from prop:guided_path_residual plus eq:poisson-eq as the next lower target.

sourceLabels : List String (explicit)

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

Ordered data items

1. prop:guided_path_residual
2. eq:poisson-eq
3. eq:SALD_Ito
4. thm:general-moving-target-SALD
5. thm:unified-forward-KL
6. thm:general-moving-target-SALD-discrete

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use main_body.tex:359-395, appendix.tex:619-704, appendix.tex:724-951, and appendix.tex:1603 for source correspondence; sald_version_2.tex remains out of scope.
2. Preserve the signs in partial_t pi_t+div(pi_t*u_t)=-pi_t*(g_t-E_pi_t[g_t]) and div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]), so the cancellation yields u_t+w_t as the transport velocity for pi_t.
3. Keep thm:unified-forward-KL as the source specialization of thm:general-moving-target-SALD with c_t<-u_t, v_t=u_t+w_t, and m_t=w_t; do not introduce a direct VA-SALD proof route.
4. Leave the continuous sigma-weighted coefficients and the discrete doubled residual coefficients under their existing obligations.

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.
2. Do not solve existence, uniqueness, regularity, or boundary conditions for the correction field w_t unless a compiled backend is explicitly supplied.
3. Do not replace the correction-field transport bridge with Girsanov, Pinsker, Talagrand, or path-space reasoning.
4. Do not add correction-field, density, finite-log-mgf, endpoint, or schedule assumptions silently to any theorem statement.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: sald.unified_forward_kl.transport_velocity_bridge, using SALD.unifiedForwardKlSpecializationContract as the line ledger.
2. Show only the source algebra from main_body.tex:359-368: combine the centered residual identity with div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]) to obtain partial_t pi_t+div(pi_t*(u_t+w_t))=0.
3. After the transport bridge, record the general-theorem specialization v_t=u_t+w_t, c_t=u_t, and m_t=w_t; stop before DV, Gronwall, or discrete EM proof search.
4. If the transport proof backend is not ready, refine SALD.unifiedForwardKlTransportBridgeObligation rather than strengthening the theorem assumptions.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.unifiedForwardKlTransportBridgeObligation is present, sourced to main_body.tex:359-368, and remains an obligation.
2. SALD.unifiedForwardKlSpecializationObligation depends on sald.unified_forward_kl.transport_velocity_bridge and still follows appendix.tex:949-951.
3. SALD.saldDependenciesForLabel "thm:unified-forward-KL" includes SALD.cycle16GeneralVaSaldUpperPacket and sald.unified_forward_kl.transport_velocity_bridge.
4. The conversion window, proof-obligation ledger, SLT audit, source index, and dialogue handoff are synchronized, with 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 cycle16GeneralVaSaldUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Keep the guided/general VA-SALD theorem statements fixed and select the unified transport-velocity bridge from prop:guided_path_residual plus eq:poisson-eq as the next lower target."
  sourceLabels := [
    "prop:guided_path_residual",
    "eq:poisson-eq",
    "eq:SALD_Ito",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:359-395, appendix.tex:619-704, appendix.tex:724-951, and appendix.tex:1603 for source correspondence; sald_version_2.tex remains out of scope.",
    "Preserve the signs in partial_t pi_t+div(pi_t*u_t)=-pi_t*(g_t-E_pi_t[g_t]) and div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]), so the cancellation yields u_t+w_t as the transport velocity for pi_t.",
    "Keep thm:unified-forward-KL as the source specialization of thm:general-moving-target-SALD with c_t<-u_t, v_t=u_t+w_t, and m_t=w_t; do not introduce a direct VA-SALD proof route.",
    "Leave the continuous sigma-weighted coefficients and the discrete doubled residual coefficients under their existing obligations."
  ]
  nonGoals := [
    "Do not prove or restate thm:general-moving-target-SALD, thm:unified-forward-KL, or thm:general-moving-target-SALD-discrete.",
    "Do not solve existence, uniqueness, regularity, or boundary conditions for the correction field w_t unless a compiled backend is explicitly supplied.",
    "Do not replace the correction-field transport bridge with Girsanov, Pinsker, Talagrand, or path-space reasoning.",
    "Do not add correction-field, density, finite-log-mgf, endpoint, or schedule assumptions silently to any theorem statement."
  ]
  lowerPacket := [
    "Target exactly one interface: sald.unified_forward_kl.transport_velocity_bridge, using SALD.unifiedForwardKlSpecializationContract as the line ledger.",
    "Show only the source algebra from main_body.tex:359-368: combine the centered residual identity with div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]) to obtain partial_t pi_t+div(pi_t*(u_t+w_t))=0.",
    "After the transport bridge, record the general-theorem specialization v_t=u_t+w_t, c_t=u_t, and m_t=w_t; stop before DV, Gronwall, or discrete EM proof search.",
    "If the transport proof backend is not ready, refine SALD.unifiedForwardKlTransportBridgeObligation rather than strengthening the theorem assumptions."
  ]
  reviewerChecklist := [
    "SALD.unifiedForwardKlTransportBridgeObligation is present, sourced to main_body.tex:359-368, and remains an obligation.",
    "SALD.unifiedForwardKlSpecializationObligation depends on sald.unified_forward_kl.transport_velocity_bridge and still follows appendix.tex:949-951.",
    "SALD.saldDependenciesForLabel \"thm:unified-forward-KL\" includes SALD.cycle16GeneralVaSaldUpperPacket and sald.unified_forward_kl.transport_velocity_bridge.",
    "The conversion window, proof-obligation ledger, SLT audit, source index, and dialogue handoff are synchronized, with sald_version_2.tex excluded.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-20 upper packet returning to the guided/general VA-SALD path.

The selected lower target is the final Gronwall/display bridge for
`thm:general-moving-target-SALD-discrete`.  This packet is workflow data only:
it keeps the theorem statement, the continuous general theorem, and the unified
specialization fixed, and it does not promote any analytic dependency.
-/