AutoSamplingTheory.SALD.cycle90DiscreteForwardKlMassConservationLowerObligation

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 cycle90DiscreteForwardKlMassConservationLowerObligation :
    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.discrete_forward_kl.cycle90_mass_conservation_lower

statement : String (explicit)

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

Cycle 90 lower compiles the mapped-law constant weak-test route for eq:KL-derivative-0-discrete. SALD.discreteForwardKlLawConstantTestTotalMassOne proves that the constant test integrates to one against Measure.map (hatX s) P when P is a probability measure. SALD.discreteForwardKlLawConstantTestHasDerivAtZero uses AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample to show the concrete mapped-law constant-test pairing has derivative zero. SALD.discreteForwardKlMassTermZeroOfLawConstantTestDerivative, SALD.discreteForwardKlDerivativeSplitOfLawConstantTestMassScalar, and SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar then feed this into the cycle-89 raw derivative route without a primitive hmass hypothesis or abstract totalMass/local-normalization input. Classification: discharges-supplied-hypothesis for the local scalar hmass/normalization route; the remaining source-cited boundary is identifying the paper massTerm with the derivative of this concrete constant weak-test pairing for hat rho_s = Law(hat X_s).

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldForwardKlDiscreteDerivativeSource — 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.cycle90DiscreteForwardKlMassConservationMiddleObligation
2. SALD.discreteForwardKlLawConstantTestTotalMassOne
3. SALD.discreteForwardKlLawConstantTestHasDerivAtZero
4. SALD.discreteForwardKlMassTermZeroOfLawConstantTestDerivative
5. SALD.discreteForwardKlDerivativeSplitOfLawConstantTestMassScalar
6. SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar
7. AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample
8. AutoSamplingTheory.lawMapIntegral
9. SALD.discreteForwardKlDerivativeSplitOfRawIbpsScalar
10. SALD.discreteForwardKlPostLsiDerivativeBoundOfRawIbpsScalar
11. SALD.discreteForwardKlDerivativeObligation
12. sald.discrete_forward_kl.kl_derivative
13. eq:KL-derivative-0-discrete
14. appendix.tex:338-388
15. Mathlib.MeasureTheory.Measure.Map
16. Mathlib.MeasureTheory.Integral.Bochner.Basic
17. Mathlib.Analysis.Calculus.Deriv.Basic

note : String (explicit)

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

Compiled local probability-law and derivative-transport handoff plus remaining obligation. It proves the constant-test mapped-law derivative is zero, but does not prove the raw KL differentiability theorem, density derivative representation, weak FP, integration by parts, FI, LSI, DV, Gronwall, theorem closure, or any SLT result.

def cycle90DiscreteForwardKlMassConservationLowerObligation :
    ProofObligation where
  id := "sald.discrete_forward_kl.cycle90_mass_conservation_lower"
  statement := "Cycle 90 lower compiles the mapped-law constant weak-test route for eq:KL-derivative-0-discrete. SALD.discreteForwardKlLawConstantTestTotalMassOne proves that the constant test integrates to one against Measure.map (hatX s) P when P is a probability measure. SALD.discreteForwardKlLawConstantTestHasDerivAtZero uses AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample to show the concrete mapped-law constant-test pairing has derivative zero. SALD.discreteForwardKlMassTermZeroOfLawConstantTestDerivative, SALD.discreteForwardKlDerivativeSplitOfLawConstantTestMassScalar, and SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar then feed this into the cycle-89 raw derivative route without a primitive hmass hypothesis or abstract totalMass/local-normalization input. Classification: discharges-supplied-hypothesis for the local scalar hmass/normalization route; the remaining source-cited boundary is identifying the paper massTerm with the derivative of this concrete constant weak-test pairing for hat rho_s = Law(hat X_s)."
  source := saldForwardKlDiscreteDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle90DiscreteForwardKlMassConservationMiddleObligation",
    "SALD.discreteForwardKlLawConstantTestTotalMassOne",
    "SALD.discreteForwardKlLawConstantTestHasDerivAtZero",
    "SALD.discreteForwardKlMassTermZeroOfLawConstantTestDerivative",
    "SALD.discreteForwardKlDerivativeSplitOfLawConstantTestMassScalar",
    "SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar",
    "AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample",
    "AutoSamplingTheory.lawMapIntegral",
    "SALD.discreteForwardKlDerivativeSplitOfRawIbpsScalar",
    "SALD.discreteForwardKlPostLsiDerivativeBoundOfRawIbpsScalar",
    "SALD.discreteForwardKlDerivativeObligation",
    "sald.discrete_forward_kl.kl_derivative",
    "eq:KL-derivative-0-discrete",
    "appendix.tex:338-388",
    "Mathlib.MeasureTheory.Measure.Map",
    "Mathlib.MeasureTheory.Integral.Bochner.Basic",
    "Mathlib.Analysis.Calculus.Deriv.Basic"
  ]
  note := "Compiled local probability-law and derivative-transport handoff plus remaining obligation. It proves the constant-test mapped-law derivative is zero, but does not prove the raw KL differentiability theorem, density derivative representation, weak FP, integration by parts, FI, LSI, DV, Gronwall, theorem closure, or any SLT result."

/-- Cycle-90 proof-DAG pane for the discrete KL mass-conservation blocker. -/