AutoSamplingTheory.SALD.cycle37DvVariationMiddleAuditContract

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 cycle37DvVariationMiddleAuditContract : 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 InformationTheory/KullbackLeibler/Basic.lean: klDiv and Gibbs nonnegativity
3. Mathlib MeasureTheory/Measure/LogLikelihoodRatio.lean: tilted-right log-likelihood integral identity
4. Mathlib MeasureTheory/Measure/Tilted.lean: exponential tilting and absolute continuity

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:73-74 fixes the common probability-space orientation KL(nu||mu); map to probability measures nu and mu plus hnu_mu : nu << mu for the one-sided backend.
2. appendix.tex:75-78 fixes the finite-log-mgf test class; map a selected test Z to hZ_nu, hexp_mu, and hllr hypotheses before applying the local one-sided theorem.
3. The full equality KL(nu||mu)=sup_Z(E_nu[Z]-log E_mu[exp Z]) remains Boucheron-source-cited through probability.dv_variational_formula.
4. The admissible-test upper bound E_nu[Z]-log E_mu[exp Z] <= KL(nu||mu) is now proved locally under explicit Mathlib hypotheses by exponential tilting.

leanStepMap : List String (explicit)

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

Ordered data items

1. AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight compiles the one-sided DV inequality using klDiv, mu.tilted Z, absolute continuity into the tilted law, Gibbs nonnegativity, and the tilted-right llr integral identity.
2. AutoSamplingTheory.dvVariationalTiltedRightOneSidedConsequence composes that tilted inequality with the scalar rearrangement to produce the paper-consumed form E_nu[Z] <= KL(nu||mu)+log E_mu[exp Z] under the same selected-test hypotheses.
3. AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar and AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar remain scalar/order bridges, now alongside the stronger Mathlib-backed one-sided theorem.
4. No local theorem proves the supremum identity or existence/optimality of maximizing tests; dvVariationalFormulaInterface saldDvVariationSource and probability.dv_variational_formula remain sourceCited.

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, still supplies the full variational equality.
2. Mathlib tilted-measure and KL lemmas supply only the admissible-test inequality under explicit integrability/absolute-continuity hypotheses.
3. 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 for the equality and supremum over all finite-log-mgf tests.
2. sald.dv_variation.finite_log_mgf_interface still owes theorem-specific common-space, absolute-continuity, measurability, finite-log-mgf, and finite-KL/log-likelihood integrability witnesses.
3. Downstream forward-KL and general-moving-target theorem blocks may use the one-sided theorem only after supplying their own selected-test hypotheses; no theorem statement receives new hidden assumptions.

lowerPacket : List String (explicit)

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

Ordered data items

1. If lower continues this DV slice, target exactly the theorem-instance witness layer: show how a SALD squared-velocity or residual test supplies hnu_mu, hZ_nu, hexp_mu, and hllr for AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight.
2. Do not claim the Boucheron supremum equality is formalized; keep dvVariationalFormulaInterface and probability.dv_variational_formula sourceCited.
3. Do not move to LSI/KL/FI, forward-KL derivative, or EM interpolation until the DV interface review accepts this one-sided backend classification.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight is a real theorem with no axiom/sorry/admit/fake closure.
2. SALD.dvContract and saldStatusForLabel "lem:dv_variation" remain sourceCited because the supremum equality is not proved.
3. Cycle 37 notes classify the new theorem as one-sided admissible-test inequality only, not Donsker--Varadhan equality.
4. No SLT theorem is imported or marked formalized, and no downstream SALD theorem assumptions are changed.

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 cycle37DvVariationMiddleAuditContract : 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 InformationTheory/KullbackLeibler/Basic.lean: klDiv and Gibbs nonnegativity",
    "Mathlib MeasureTheory/Measure/LogLikelihoodRatio.lean: tilted-right log-likelihood integral identity",
    "Mathlib MeasureTheory/Measure/Tilted.lean: exponential tilting and absolute continuity"
  ]
  sourceStepMap := [
    "appendix.tex:73-74 fixes the common probability-space orientation KL(nu||mu); map to probability measures nu and mu plus hnu_mu : nu << mu for the one-sided backend.",
    "appendix.tex:75-78 fixes the finite-log-mgf test class; map a selected test Z to hZ_nu, hexp_mu, and hllr hypotheses before applying the local one-sided theorem.",
    "The full equality KL(nu||mu)=sup_Z(E_nu[Z]-log E_mu[exp Z]) remains Boucheron-source-cited through probability.dv_variational_formula.",
    "The admissible-test upper bound E_nu[Z]-log E_mu[exp Z] <= KL(nu||mu) is now proved locally under explicit Mathlib hypotheses by exponential tilting."
  ]
  leanStepMap := [
    "AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight compiles the one-sided DV inequality using klDiv, mu.tilted Z, absolute continuity into the tilted law, Gibbs nonnegativity, and the tilted-right llr integral identity.",
    "AutoSamplingTheory.dvVariationalTiltedRightOneSidedConsequence composes that tilted inequality with the scalar rearrangement to produce the paper-consumed form E_nu[Z] <= KL(nu||mu)+log E_mu[exp Z] under the same selected-test hypotheses.",
    "AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar and AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar remain scalar/order bridges, now alongside the stronger Mathlib-backed one-sided theorem.",
    "No local theorem proves the supremum identity or existence/optimality of maximizing tests; dvVariationalFormulaInterface saldDvVariationSource and probability.dv_variational_formula remain sourceCited."
  ]
  citedResultMap := [
    "Boucheron, Lugosi, and Massart, Concentration Inequalities, Corollary 4.15, cited at appendix.tex:73, still supplies the full variational equality.",
    "Mathlib tilted-measure and KL lemmas supply only the admissible-test inequality under explicit integrability/absolute-continuity hypotheses.",
    "SLT entropy_duality remains reference-only and is not imported or marked formalized."
  ]
  obligationMap := [
    "probability.dv_variational_formula remains source-cited for the equality and supremum over all finite-log-mgf tests.",
    "sald.dv_variation.finite_log_mgf_interface still owes theorem-specific common-space, absolute-continuity, measurability, finite-log-mgf, and finite-KL/log-likelihood integrability witnesses.",
    "Downstream forward-KL and general-moving-target theorem blocks may use the one-sided theorem only after supplying their own selected-test hypotheses; no theorem statement receives new hidden assumptions."
  ]
  lowerPacket := [
    "If lower continues this DV slice, target exactly the theorem-instance witness layer: show how a SALD squared-velocity or residual test supplies hnu_mu, hZ_nu, hexp_mu, and hllr for AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight.",
    "Do not claim the Boucheron supremum equality is formalized; keep dvVariationalFormulaInterface and probability.dv_variational_formula sourceCited.",
    "Do not move to LSI/KL/FI, forward-KL derivative, or EM interpolation until the DV interface review accepts this one-sided backend classification."
  ]
  reviewerChecklist := [
    "AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight is a real theorem with no axiom/sorry/admit/fake closure.",
    "SALD.dvContract and saldStatusForLabel \"lem:dv_variation\" remain sourceCited because the supremum equality is not proved.",
    "Cycle 37 notes classify the new theorem as one-sided admissible-test inequality only, not Donsker--Varadhan equality.",
    "No SLT theorem is imported or marked formalized, and no downstream SALD theorem assumptions are changed."
  ]
  status := ProofStatus.obligation

/-- Cycle-37 middle obligation tracking the new one-sided tilted backend. -/