AutoSamplingTheory.SALD.cycle37DvVariationUpperPacket

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.FirstAppendixVocabularyPacket. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle37DvVariationUpperPacket : FirstAppendixVocabularyPacket

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.

Proof-closure priority check before assigning lower work: (1) lem:gronwall was advanced in cycle 36 but remains an obligation pending the endpoint-safe differentiability/derivative-witness bridge; (2) cycle 37 therefore selects lem:dv_variation; (3) eq:LSI-KL-FI, (4) the forward-KL Fokker-Planck/KL derivative identity, and (5) the EM interpolation Fokker-Planck backend remain later proof-closure targets.

sourceLabels : List String (explicit)

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

Ordered data items

1. lem:gronwall
2. lem:dv_variation
3. eq:LSI-KL-FI
4. thm:forward-KL
5. thm:forward-KL-discrete

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1: reproduce exactly appendix.tex:73-79 and its cited Boucheron Corollary 4.15 dependency; sald_version_2.tex remains excluded.
2. Keep the paper statement fixed: mu and nu are probability distributions on the same space, the supremum ranges over real random variables Z with log E_mu[exp Z] < +infty, and the display is KL(nu||mu)=sup_Z(E_nu[Z]-log E_mu[exp Z]).
3. If a local Mathlib proof is too large, keep probability.dv_variational_formula source-cited and expose a Mathlib-shaped theorem interface with explicit common-space, absolute-continuity, measurability, finite-KL, and finite-log-mgf hypotheses.
4. Do not spend this cycle on source-index rebaseline unless a reviewer finds a blocking source-anchor defect; the current anchor is appendix.tex:73-79 from the original paper.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not mark SALD.dvContract, probability.dv_variational_formula, or saldStatusForLabel "lem:dv_variation" formalized unless a compiled Lean theorem replaces the source-cited result.
2. Do not replace Donsker--Varadhan with Pinsker, Talagrand, LSI, Girsanov, path-space comparison, or a theorem-specific Cauchy-only bound.
3. Do not add new finite-mgf, absolute-continuity, smoothness, boundedness, or state-space assumptions to thm:forward-KL or any downstream theorem statement.
4. Do not reopen LSI/KL/FI, forward-KL derivative, EM interpolation, PI velocity-norm, guided, general VA-SALD, unified, or accumulated-error proof search in this upper packet.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle must keep two-way Lean/Markdown/LaTeX synchronization for appendix.tex:73-79, AutoSamplingTheory/Probability.lean, AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and research-wiki/cited-results/SLT_reuse_audit.md.
2. First lower target: one declaration/interface only, centered on dvVariationalFormulaInterface saldDvVariationSource and probability.dv_variational_formula; either prove a genuinely local Mathlib-backed sublemma or refine the source-cited theorem interface without changing its status.
3. Use the local Mathlib audit as the starting point: InformationTheory.KullbackLeibler.Basic supplies klDiv infrastructure and MeasureTheory.Measure.Tilted supplies tilted-measure/log-likelihood infrastructure, but no ready entropy-duality theorem matching appendix.tex:73-79 has been found.
4. Keep the compiled scalar bridges AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar and AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar as post-DV order lemmas only; do not present them as a proof of the variational equality.
5. Downstream SALD applications must continue to depend explicitly on theorem-specific common-space, absolute-continuity, measurability, finite-log-mgf, alpha0-to-alpha monotonicity, and positive-alpha scaling obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.dvContract remains ProofStatus.sourceCited and includes the cycle 37 workflow obligation only as assignment data.
2. SALD.saldDependenciesForLabel "lem:dv_variation" names the cycle 37 packet and keeps the cycle 32 scalar bridges as post-DV consequences, not theorem closures.
3. The conversion window, proof-obligation ledger, and SLT audit classify cycle 37 as source-cited DV equality/proof-target sharpening, with no SLT import and no claim that the Boucheron supremum formula is formalized.
4. No axiom, sorry, admit, Prop := True, := trivial, hidden theorem assumption, source-file drift, or alternate entropy route is introduced.
5. The mandatory gate 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 cycle37DvVariationUpperPacket : FirstAppendixVocabularyPacket where
  objective := "Proof-closure priority check before assigning lower work: (1) lem:gronwall was advanced in cycle 36 but remains an obligation pending the endpoint-safe differentiability/derivative-witness bridge; (2) cycle 37 therefore selects lem:dv_variation; (3) eq:LSI-KL-FI, (4) the forward-KL Fokker-Planck/KL derivative identity, and (5) the EM interpolation Fokker-Planck backend remain later proof-closure targets."
  sourceLabels := [
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "thm:forward-KL",
    "thm:forward-KL-discrete"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: reproduce exactly appendix.tex:73-79 and its cited Boucheron Corollary 4.15 dependency; sald_version_2.tex remains excluded.",
    "Keep the paper statement fixed: mu and nu are probability distributions on the same space, the supremum ranges over real random variables Z with log E_mu[exp Z] < +infty, and the display is KL(nu||mu)=sup_Z(E_nu[Z]-log E_mu[exp Z]).",
    "If a local Mathlib proof is too large, keep probability.dv_variational_formula source-cited and expose a Mathlib-shaped theorem interface with explicit common-space, absolute-continuity, measurability, finite-KL, and finite-log-mgf hypotheses.",
    "Do not spend this cycle on source-index rebaseline unless a reviewer finds a blocking source-anchor defect; the current anchor is appendix.tex:73-79 from the original paper."
  ]
  nonGoals := [
    "Do not mark SALD.dvContract, probability.dv_variational_formula, or saldStatusForLabel \"lem:dv_variation\" formalized unless a compiled Lean theorem replaces the source-cited result.",
    "Do not replace Donsker--Varadhan with Pinsker, Talagrand, LSI, Girsanov, path-space comparison, or a theorem-specific Cauchy-only bound.",
    "Do not add new finite-mgf, absolute-continuity, smoothness, boundedness, or state-space assumptions to thm:forward-KL or any downstream theorem statement.",
    "Do not reopen LSI/KL/FI, forward-KL derivative, EM interpolation, PI velocity-norm, guided, general VA-SALD, unified, or accumulated-error proof search in this upper packet."
  ]
  lowerPacket := [
    "Middle must keep two-way Lean/Markdown/LaTeX synchronization for appendix.tex:73-79, AutoSamplingTheory/Probability.lean, AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, proof-obligations/ASTIS-SALD-001.md, and research-wiki/cited-results/SLT_reuse_audit.md.",
    "First lower target: one declaration/interface only, centered on dvVariationalFormulaInterface saldDvVariationSource and probability.dv_variational_formula; either prove a genuinely local Mathlib-backed sublemma or refine the source-cited theorem interface without changing its status.",
    "Use the local Mathlib audit as the starting point: InformationTheory.KullbackLeibler.Basic supplies klDiv infrastructure and MeasureTheory.Measure.Tilted supplies tilted-measure/log-likelihood infrastructure, but no ready entropy-duality theorem matching appendix.tex:73-79 has been found.",
    "Keep the compiled scalar bridges AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar and AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar as post-DV order lemmas only; do not present them as a proof of the variational equality.",
    "Downstream SALD applications must continue to depend explicitly on theorem-specific common-space, absolute-continuity, measurability, finite-log-mgf, alpha0-to-alpha monotonicity, and positive-alpha scaling obligations."
  ]
  reviewerChecklist := [
    "SALD.dvContract remains ProofStatus.sourceCited and includes the cycle 37 workflow obligation only as assignment data.",
    "SALD.saldDependenciesForLabel \"lem:dv_variation\" names the cycle 37 packet and keeps the cycle 32 scalar bridges as post-DV consequences, not theorem closures.",
    "The conversion window, proof-obligation ledger, and SLT audit classify cycle 37 as source-cited DV equality/proof-target sharpening, with no SLT import and no claim that the Boucheron supremum formula is formalized.",
    "No axiom, sorry, admit, Prop := True, := trivial, hidden theorem assumption, source-file drift, or alternate entropy route is introduced.",
    "The mandatory gate python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-37 upper workflow obligation for the cited DV interface target. -/