AutoSamplingTheory.SALD.cycle42DvVariationLowerObligation

Data definition / provenance and workflow record

Meaning and type

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

def cycle42DvVariationLowerObligation : ProofObligation

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.

id : String (explicit)

Stable obligation identifier.

sald.dv_variation.cycle42_lower_scaled_energy

statement : String (explicit)

Desired mathematical or workflow content as String; it is not a proposition in Prop and the def does not prove it.

Maintain the cycle 42 lower scaled-test DV energy bridge for appendix.tex lines 73-79 and the first SALD use at appendix.tex lines 230-241: AutoSamplingTheory.dvVariationalScaledTestEnergyBound divides the selected-test one-sided inequality for Z=alpha*q by alpha>0 and rewrites the log-mgf quotient as eAlpha; AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff preserves the downstream nonnegative coefficient.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldForwardKlDvEnergySource — audited data reference, not expanded and not a compiled dependency edge

status : AutoSamplingTheory.ProofStatus (explicit)

Stored ProofStatus, default obligation; even an explicitly stored formalized does not independently certify a Lean theorem.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

dependsOn : List String (explicit)

List of declared dependency names as strings; may mix theorem names, obligations, source labels, or descriptions. Not the compiled dependency DAG.

Ordered data items

1. SALD.cycle42DvVariationMiddleAuditContract
2. SALD.cycle42DvVariationMiddleObligation
3. AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha
4. AutoSamplingTheory.dvVariationalOneSidedOfScaledTest
5. AutoSamplingTheory.dvVariationalScaledTestEnergyBound
6. AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff
7. AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight
8. probability.dv_variational_formula
9. dvVariationalFormulaInterface saldDvVariationSource
10. SALD.saldDvFiniteLogMgfContract
11. SALD.forwardKlDvFiniteLogMgfWitnessContract
12. SALD.forwardKlDvPositiveAlphaScalingScalar
13. SALD.forwardKlDvPositiveAlphaCoefficientScalar

note : String (explicit)

Recorded evidence/caveats; may distinguish a compiled scalar helper from still-open source analysis.

This is a proof-producing lower consequence for selected scaled tests only. It does not prove the Boucheron supremum equality, does not mark lem:dv_variation formalized, and does not discharge the theorem-specific common-space, absolute-continuity, q-integrability, alpha0 finite-mgf, or log-likelihood hypotheses.

def cycle42DvVariationLowerObligation : ProofObligation where
  id := "sald.dv_variation.cycle42_lower_scaled_energy"
  statement := "Maintain the cycle 42 lower scaled-test DV energy bridge for appendix.tex lines 73-79 and the first SALD use at appendix.tex lines 230-241: AutoSamplingTheory.dvVariationalScaledTestEnergyBound divides the selected-test one-sided inequality for Z=alpha*q by alpha>0 and rewrites the log-mgf quotient as eAlpha; AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff preserves the downstream nonnegative coefficient."
  source := saldForwardKlDvEnergySource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle42DvVariationMiddleAuditContract",
    "SALD.cycle42DvVariationMiddleObligation",
    "AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha",
    "AutoSamplingTheory.dvVariationalOneSidedOfScaledTest",
    "AutoSamplingTheory.dvVariationalScaledTestEnergyBound",
    "AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff",
    "AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight",
    "probability.dv_variational_formula",
    "dvVariationalFormulaInterface saldDvVariationSource",
    "SALD.saldDvFiniteLogMgfContract",
    "SALD.forwardKlDvFiniteLogMgfWitnessContract",
    "SALD.forwardKlDvPositiveAlphaScalingScalar",
    "SALD.forwardKlDvPositiveAlphaCoefficientScalar"
  ]
  note := "This is a proof-producing lower consequence for selected scaled tests only. It does not prove the Boucheron supremum equality, does not mark lem:dv_variation formalized, and does not discharge the theorem-specific common-space, absolute-continuity, q-integrability, alpha0 finite-mgf, or log-likelihood hypotheses."

/-- Cycle-18 upper packet returning to the continuous forward-KL chain.

This packet uses the accepted cycle-17 scalar Gronwall algebra only as a
dependency marker for the continuous theorem's final Gronwall bookkeeping.  It
does not claim the full Gronwall lemma, DV, LSI-to-KL/FI, or the KL derivative
backend has been formalized.
-/