AutoSamplingTheory.SALD.cycle32DvVariationMiddleAuditContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle32DvVariationMiddleAuditContract : FirstAppendixMiddleAuditContract

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.

sourceIndexPath : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

research-wiki/source-index/SALD_original.jsonl

focusLabels : 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

sourceReadWindows : List String (explicit)

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

Ordered data items

1. appendix.tex:73-79
2. Mathlib MeasureTheory/Measure/Tilted.lean: tilted-measure infrastructure only
3. Mathlib InformationTheory/KullbackLeibler/Basic.lean: KL infrastructure only

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:73 states mu and nu are probability distributions on the same space; map to dvVariationalFormulaInterface.probabilityMeasures and SALD.saldDvFiniteLogMgfContract.commonSpaceInterface.
2. appendix.tex:75-77 states the Boucheron Corollary 4.15 equality over finite-log-mgf tests; map to probability.dv_variational_formula and keep sourceCited.
3. The one-sided SALD use is the algebraic consequence of an admissible-test upper bound E_nu[Z]-logMgf <= KL; map the algebra only to AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar.

leanStepMap : List String (explicit)

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

Ordered data items

1. dvVariationalFormulaInterface saldDvVariationSource records the cited equality and finite-log-mgf predicate.
2. AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar compiles the rearrangement expectation - logMgf <= kl -> expectation <= kl + logMgf.
3. No local Mathlib theorem was found that closes the full DV variational equality in the current v4.29.1 checkout; Measure.tilted and InformationTheory.klDiv are future backend candidates only.

citedResultMap : List String (explicit)

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

Ordered data items

1. Boucheron, Lugosi, and Massart, Concentration Inequalities, Corollary 4.15, cited at appendix.tex:73.
2. SLT entropy_duality remains reference-only and is not imported or marked formalized.

obligationMap : List String (explicit)

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

Ordered data items

1. probability.dv_variational_formula remains source-cited.
2. sald.dv_variation.finite_log_mgf_interface still owes common-space, measurability, finite-log-mgf, and alpha-complexity witnesses for theorem-specific SALD tests.
3. forward-KL, discrete forward-KL, general moving-target, and general discrete theorem blocks still owe their own DV instantiation side conditions.

lowerPacket : List String (explicit)

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

Ordered data items

1. Do not search broad SDE/Sampling libraries in this cycle.
2. If continuing DV, target only a precise theorem statement around Mathlib klDiv/tilted measures or a finite-log-mgf witness sublemma; do not introduce axioms.
3. Use AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar only after a cited or formal DV bound supplies expectation - logMgf <= KL.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.dvContract and saldStatusForLabel "lem:dv_variation" stay sourceCited.
2. The new theorem is a scalar Real rearrangement only and does not claim the DV equality.
3. No SLT theorem is imported or marked formalized.
4. 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 cycle32DvVariationMiddleAuditContract : FirstAppendixMiddleAuditContract where
  sourceIndexPath := "research-wiki/source-index/SALD_original.jsonl"
  focusLabels := [
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "thm:forward-KL",
    "thm:forward-KL-discrete"
  ]
  sourceReadWindows := [
    "appendix.tex:73-79",
    "Mathlib MeasureTheory/Measure/Tilted.lean: tilted-measure infrastructure only",
    "Mathlib InformationTheory/KullbackLeibler/Basic.lean: KL infrastructure only"
  ]
  sourceStepMap := [
    "appendix.tex:73 states mu and nu are probability distributions on the same space; map to dvVariationalFormulaInterface.probabilityMeasures and SALD.saldDvFiniteLogMgfContract.commonSpaceInterface.",
    "appendix.tex:75-77 states the Boucheron Corollary 4.15 equality over finite-log-mgf tests; map to probability.dv_variational_formula and keep sourceCited.",
    "The one-sided SALD use is the algebraic consequence of an admissible-test upper bound E_nu[Z]-logMgf <= KL; map the algebra only to AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar."
  ]
  leanStepMap := [
    "dvVariationalFormulaInterface saldDvVariationSource records the cited equality and finite-log-mgf predicate.",
    "AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar compiles the rearrangement expectation - logMgf <= kl -> expectation <= kl + logMgf.",
    "No local Mathlib theorem was found that closes the full DV variational equality in the current v4.29.1 checkout; Measure.tilted and InformationTheory.klDiv are future backend candidates only."
  ]
  citedResultMap := [
    "Boucheron, Lugosi, and Massart, Concentration Inequalities, Corollary 4.15, cited at appendix.tex:73.",
    "SLT entropy_duality remains reference-only and is not imported or marked formalized."
  ]
  obligationMap := [
    "probability.dv_variational_formula remains source-cited.",
    "sald.dv_variation.finite_log_mgf_interface still owes common-space, measurability, finite-log-mgf, and alpha-complexity witnesses for theorem-specific SALD tests.",
    "forward-KL, discrete forward-KL, general moving-target, and general discrete theorem blocks still owe their own DV instantiation side conditions."
  ]
  lowerPacket := [
    "Do not search broad SDE/Sampling libraries in this cycle.",
    "If continuing DV, target only a precise theorem statement around Mathlib klDiv/tilted measures or a finite-log-mgf witness sublemma; do not introduce axioms.",
    "Use AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar only after a cited or formal DV bound supplies expectation - logMgf <= KL."
  ]
  reviewerChecklist := [
    "SALD.dvContract and saldStatusForLabel \"lem:dv_variation\" stay sourceCited.",
    "The new theorem is a scalar Real rearrangement only and does not claim the DV equality.",
    "No SLT theorem is imported or marked formalized.",
    "python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation