AutoSamplingTheory.SALD.cycle12GeneralVaSaldUpperPacket

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 cycle12GeneralVaSaldUpperPacket : 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 isolate the residual-field Donsker--Varadhan finite-log-mgf witness for m_t, including the unified specialization m_t=w_t and the discrete EM-interpolation reuse.

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. def:alpha-complexity

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 and appendix.tex:724-951 plus appendix.tex:1544-1603, with sald_version_2.tex excluded.
2. Preserve m_t=v_t-c_t, the unified specialization c_t<-u_t and m_t=w_t, and the discrete residual coefficient 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1).
3. Treat DV, alpha0-to-alpha finite-log-mgf monotonicity, common-space/absolute-continuity, EM interpolation laws, and Gronwall as obligations or source-cited facts 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, thm:unified-forward-KL, or thm:general-moving-target-SALD-discrete.
2. Do not replace the source residual DV step with Pinsker, Talagrand, path-space, Girsanov, or a direct VA-SALD proof.
3. Do not add finite-log-mgf, measurability, absolute-continuity, endpoint, or schedule hypotheses silently to theorem statements.
4. Do not simplify away the sigma-weighted or doubled discrete residual coefficients.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, or their named obligations.
2. For the continuous theorem, refine alpha0-to-alpha monotonicity for Z=alpha*||m_t||^2, common-space/absolute-continuity, measurability, or positive-alpha scaling.
3. For the unified theorem, only check the specialization bridge m_t=w_t after c_t<-u_t; do not introduce a separate direct proof.
4. For the discrete theorem, keep nu=hat rho_s, mu=tilde pi_s, and the coefficient 2*sigma_eta^(-2)*dot t(s)^2 before time change.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.generalVaSaldContract and SALD.unifiedForwardKlContract list SALD.generalMovingTargetDvFiniteLogMgfWitnessObligation before the residual DV-energy obligation.
2. SALD.generalVaSaldDiscreteContract lists SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessObligation before SALD.generalMovingTargetDiscreteDvMEnergyObligation.
3. SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag contain residual DV witness blocks before the DV-energy blocks.
4. The conversion window, proof-obligation ledger, SLT audit, and source index remain synchronized and sald_version_2.tex remains 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 cycle12GeneralVaSaldUpperPacket : GeneralVaSaldUpperPacket where
  objective := "Keep the guided/general VA-SALD theorem statements fixed and isolate the residual-field Donsker--Varadhan finite-log-mgf witness for m_t, including the unified specialization m_t=w_t and the discrete EM-interpolation reuse."
  sourceLabels := [
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete",
    "lem:dv_variation",
    "def:alpha-complexity"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:359-395 and appendix.tex:724-951 plus appendix.tex:1544-1603, with sald_version_2.tex excluded.",
    "Preserve m_t=v_t-c_t, the unified specialization c_t<-u_t and m_t=w_t, and the discrete residual coefficient 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1).",
    "Treat DV, alpha0-to-alpha finite-log-mgf monotonicity, common-space/absolute-continuity, EM interpolation laws, and Gronwall as obligations or source-cited facts until compiled Lean proofs replace them."
  ]
  nonGoals := [
    "Do not restate or prove thm:general-moving-target-SALD, thm:unified-forward-KL, or thm:general-moving-target-SALD-discrete.",
    "Do not replace the source residual DV step with Pinsker, Talagrand, path-space, Girsanov, or a direct VA-SALD proof.",
    "Do not add finite-log-mgf, measurability, absolute-continuity, endpoint, or schedule hypotheses silently to theorem statements.",
    "Do not simplify away the sigma-weighted or doubled discrete residual coefficients."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, or their named obligations.",
    "For the continuous theorem, refine alpha0-to-alpha monotonicity for Z=alpha*||m_t||^2, common-space/absolute-continuity, measurability, or positive-alpha scaling.",
    "For the unified theorem, only check the specialization bridge m_t=w_t after c_t<-u_t; do not introduce a separate direct proof.",
    "For the discrete theorem, keep nu=hat rho_s, mu=tilde pi_s, and the coefficient 2*sigma_eta^(-2)*dot t(s)^2 before time change."
  ]
  reviewerChecklist := [
    "SALD.generalVaSaldContract and SALD.unifiedForwardKlContract list SALD.generalMovingTargetDvFiniteLogMgfWitnessObligation before the residual DV-energy obligation.",
    "SALD.generalVaSaldDiscreteContract lists SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessObligation before SALD.generalMovingTargetDiscreteDvMEnergyObligation.",
    "SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag contain residual DV witness blocks before the DV-energy blocks.",
    "The conversion window, proof-obligation ledger, SLT audit, and source index remain synchronized and sald_version_2.tex remains excluded.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation