AutoSamplingTheory.SALD.cycle51DiscreteForwardKlDerivativeLowerObligation

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.

Lean statement of this data definition

The part after the colon is the output data type. This declaration takes no mathematical proof inputs.

def cycle51DiscreteForwardKlDerivativeLowerObligation : 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.cycle51_derivative_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.

Record the cycle 51 lower proof-producing scalar handoff for appendix.tex lines 388-491: once the EM conditional-Fokker-Planck and integration-by-parts backend supplies dK=-FI+frozenCross+movingCross, the frozen-defect lemma supplies the first quarter-FI plus Gamma/Delta terms, Young supplies the moving quarter-FI plus ||tilde v_s||^2, and eq:LSI-KL-FI supplies C_LSI*K <= (1/2)*FI, SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar yields the exact pre-DV inequality dK <= -(C_LSI-2*eta^2*alpha'^(-1)*Gamma)*K + ||tilde v_s||^2 + 2*eta*Delta.

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

SALD.discreteForwardKlPostLsiDerivativeBoundScalar
SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar
SALD.discreteForwardKlDerivativeCandidateContract
SALD.discreteForwardKlDerivativeObligation
sald.discrete_forward_kl.em_interpolation_fp
sald.discrete_forward_kl.em_conditional_fokker_planck
sald.discrete_forward_kl.frozen_delta_cross_lip
SALD.frozenDeltaCrossLipSaldContract
SALD.saldLsiKlFiDensityTestContract
probability.lsi_to_kl_fi

note : String (explicit)

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

The scalar lemmas compile, but the EM conditional-Fokker-Planck theorem, KL differentiation under the integral, boundary integration by parts, frozen-defect specialization, and LSI density-test backend remain obligations. No theorem statement or source constant is changed.

Exact Lean data construction

Each field assignment stores the corresponding value shown above. Omitted fields use the explicitly identified schema defaults. Strings that name theorems remain strings; they do not call those theorems.

def cycle51DiscreteForwardKlDerivativeLowerObligation : ProofObligation where
  id := "sald.discrete_forward_kl.cycle51_derivative_lower"
  statement := "Record the cycle 51 lower proof-producing scalar handoff for appendix.tex lines 388-491: once the EM conditional-Fokker-Planck and integration-by-parts backend supplies dK=-FI+frozenCross+movingCross, the frozen-defect lemma supplies the first quarter-FI plus Gamma/Delta terms, Young supplies the moving quarter-FI plus ||tilde v_s||^2, and eq:LSI-KL-FI supplies C_LSI*K <= (1/2)*FI, SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar yields the exact pre-DV inequality dK <= -(C_LSI-2*eta^2*alpha'^(-1)*Gamma)*K + ||tilde v_s||^2 + 2*eta*Delta."
  source := saldForwardKlDiscreteDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.discreteForwardKlPostLsiDerivativeBoundScalar",
    "SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar",
    "SALD.discreteForwardKlDerivativeCandidateContract",
    "SALD.discreteForwardKlDerivativeObligation",
    "sald.discrete_forward_kl.em_interpolation_fp",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "sald.discrete_forward_kl.frozen_delta_cross_lip",
    "SALD.frozenDeltaCrossLipSaldContract",
    "SALD.saldLsiKlFiDensityTestContract",
    "probability.lsi_to_kl_fi"
  ]
  note := "The scalar lemmas compile, but the EM conditional-Fokker-Planck theorem, KL differentiation under the integral, boundary integration by parts, frozen-defect specialization, and LSI density-test backend remain obligations. No theorem statement or source constant is changed."

Existing module entry · Audited data-reader index · All teaching coverage