AutoSamplingTheory.SALD.cycle42DvVariationMiddleAuditContract

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 cycle42DvVariationMiddleAuditContract : 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. appendix.tex:230-241 for the first SALD scaled test Z=alpha*||v_t||^2
3. Mathlib Probability/Moments/IntegrableExpMul.lean: alpha0-to-alpha exponential-moment interval lemma
4. Mathlib MeasureTheory/Measure/Tilted.lean and LogLikelihoodRatio.lean: one-sided tilted backend

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:73-74 fixes same-space probability measures mu and nu; selected SALD uses keep nu and mu as explicit Measure parameters.
2. appendix.tex:75-78 fixes the finite-log-mgf class for real random variables Z; the selected scaled-test interface sets Z=alpha*q.
3. The SALD applications supply q as a squared velocity/residual/frozen-defect norm and use alpha0-complexity as the intended finite-mgf witness.
4. The Boucheron equality KL(nu||mu)=sup_Z(E_nu[Z]-log E_mu[exp Z]) remains source-cited through probability.dv_variational_formula.

leanStepMap : List String (explicit)

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

Ordered data items

1. AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha proves the local finite-log-mgf monotonicity: Integrable exp(alpha0*q) -> Integrable exp(alpha*q) for 0 <= alpha <= alpha0 under a finite measure.
2. AutoSamplingTheory.dvVariationalOneSidedOfScaledTest composes that finite-log-mgf witness with AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight for Z=alpha*q.
3. The selected-test theorem keeps hnu_mu, Integrable (alpha*q) under nu, Integrable (llr nu mu) under nu, probability, and sigma-finiteness hypotheses explicit.
4. No theorem proves the Boucheron supremum equality or theorem-specific SALD common-space/measurability/log-likelihood witnesses.

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 only the full DV equality as a source-cited result.
2. Mathlib ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le supplies only the finite-mgf monotonicity used by the selected SALD test.
3. No SLT theorem is 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 and SALD.dvContract remain sourceCited.
2. sald.dv_variation.finite_log_mgf_interface still owes theorem-specific q, common-space, absolute-continuity, measurability, finite-KL/log-likelihood, and positive-alpha witnesses.
3. forward-KL, discrete forward-KL, general moving-target, and general discrete theorem blocks may use AutoSamplingTheory.dvVariationalOneSidedOfScaledTest only after supplying their own selected-test hypotheses.

lowerPacket : List String (explicit)

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

Ordered data items

1. Next lower attempt should instantiate q for one concrete source use, preferably appendix.tex:230-241 with q=||v_t||^2, without changing thm:forward-KL.
2. If the theorem-specific hnu_mu, hZ_nu, or hllr hypotheses are unavailable locally, record the exact source gap and keep the interface below formalized.
3. Do not mark lem:dv_variation formalized; this cycle closes only a finite-mgf/selected-test one-sided backend.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha and AutoSamplingTheory.dvVariationalOneSidedOfScaledTest compile without fake proof closures.
2. SALD.dvContract and saldStatusForLabel "lem:dv_variation" remain sourceCited.
3. The conversion window and cited-results page classify the new declarations as selected-test consequences, not as the Boucheron supremum formula.
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 cycle42DvVariationMiddleAuditContract : 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",
    "appendix.tex:230-241 for the first SALD scaled test Z=alpha*||v_t||^2",
    "Mathlib Probability/Moments/IntegrableExpMul.lean: alpha0-to-alpha exponential-moment interval lemma",
    "Mathlib MeasureTheory/Measure/Tilted.lean and LogLikelihoodRatio.lean: one-sided tilted backend"
  ]
  sourceStepMap := [
    "appendix.tex:73-74 fixes same-space probability measures mu and nu; selected SALD uses keep nu and mu as explicit Measure parameters.",
    "appendix.tex:75-78 fixes the finite-log-mgf class for real random variables Z; the selected scaled-test interface sets Z=alpha*q.",
    "The SALD applications supply q as a squared velocity/residual/frozen-defect norm and use alpha0-complexity as the intended finite-mgf witness.",
    "The Boucheron equality KL(nu||mu)=sup_Z(E_nu[Z]-log E_mu[exp Z]) remains source-cited through probability.dv_variational_formula."
  ]
  leanStepMap := [
    "AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha proves the local finite-log-mgf monotonicity: Integrable exp(alpha0*q) -> Integrable exp(alpha*q) for 0 <= alpha <= alpha0 under a finite measure.",
    "AutoSamplingTheory.dvVariationalOneSidedOfScaledTest composes that finite-log-mgf witness with AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight for Z=alpha*q.",
    "The selected-test theorem keeps hnu_mu, Integrable (alpha*q) under nu, Integrable (llr nu mu) under nu, probability, and sigma-finiteness hypotheses explicit.",
    "No theorem proves the Boucheron supremum equality or theorem-specific SALD common-space/measurability/log-likelihood witnesses."
  ]
  citedResultMap := [
    "Boucheron, Lugosi, and Massart, Concentration Inequalities, Corollary 4.15, cited at appendix.tex:73, still supplies only the full DV equality as a source-cited result.",
    "Mathlib ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le supplies only the finite-mgf monotonicity used by the selected SALD test.",
    "No SLT theorem is imported or marked formalized."
  ]
  obligationMap := [
    "probability.dv_variational_formula and SALD.dvContract remain sourceCited.",
    "sald.dv_variation.finite_log_mgf_interface still owes theorem-specific q, common-space, absolute-continuity, measurability, finite-KL/log-likelihood, and positive-alpha witnesses.",
    "forward-KL, discrete forward-KL, general moving-target, and general discrete theorem blocks may use AutoSamplingTheory.dvVariationalOneSidedOfScaledTest only after supplying their own selected-test hypotheses."
  ]
  lowerPacket := [
    "Next lower attempt should instantiate q for one concrete source use, preferably appendix.tex:230-241 with q=||v_t||^2, without changing thm:forward-KL.",
    "If the theorem-specific hnu_mu, hZ_nu, or hllr hypotheses are unavailable locally, record the exact source gap and keep the interface below formalized.",
    "Do not mark lem:dv_variation formalized; this cycle closes only a finite-mgf/selected-test one-sided backend."
  ]
  reviewerChecklist := [
    "AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha and AutoSamplingTheory.dvVariationalOneSidedOfScaledTest compile without fake proof closures.",
    "SALD.dvContract and saldStatusForLabel \"lem:dv_variation\" remain sourceCited.",
    "The conversion window and cited-results page classify the new declarations as selected-test consequences, not as the Boucheron supremum formula.",
    "python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-42 obligation for the selected scaled-test DV interface. -/