AutoSamplingTheory.SALD.cycle60ForwardKlDerivativeRawLowerObligation

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 cycle60ForwardKlDerivativeRawLowerObligation : 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.forward_kl.cycle60_derivative_raw_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 60 lower compiles the source-shaped scalar handoff for appendix.tex:168-228 starting from the raw KL derivative split with the mass term: after the analytic backend supplies the differentiated KL display, mass conservation, SALD Fokker-Planck/integration-by-parts first-term identity, target Cauchy estimate, KL/FI comparison, slowed-velocity scaling, and inverse-schedule product identity, SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar derives the t-time pre-DV inequality dK/dt <= -dot{s}(t)*C_LSI(t)*K(t)+(1/2)*dot{s}(t)^(-1)*||v_t||^2.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle60ForwardKlSkeletonMiddleContract
2. SALD.cycle60ForwardKlSkeletonMiddleObligation
3. SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar
4. SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar
5. SALD.forwardKlMassConservationDropScalar
6. SALD.forwardKlMassConservationFirstTermFisherScalar
7. SALD.forwardKlDerivativeCandidateContract
8. SALD.forwardKlDerivativeSideConditionContract
9. SALD.forwardKlDerivativeObligation
10. SALD.forwardKlDensityBoundaryObligation
11. SALD.forwardKlScheduleTimeChangeObligation
12. SALD.saldLsiKlFiDensityTestContract
13. sald.forward_kl.kl_derivative
14. sald.forward_kl.density_boundary_regular
15. sald.forward_kl.schedule_time_change
16. probability.lsi_to_kl_fi

note : String (explicit)

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

This is formalized only as Real/order/equality bookkeeping. It keeps mass conservation, KL differentiation, Fokker-Planck, boundary integration by parts, target transport, LSI density-test, and inverse-function calculus as explicit obligations, and it does not promote thm:forward-KL or sald.forward_kl.kl_derivative.

def cycle60ForwardKlDerivativeRawLowerObligation : ProofObligation where
  id := "sald.forward_kl.cycle60_derivative_raw_lower"
  statement := "Cycle 60 lower compiles the source-shaped scalar handoff for appendix.tex:168-228 starting from the raw KL derivative split with the mass term: after the analytic backend supplies the differentiated KL display, mass conservation, SALD Fokker-Planck/integration-by-parts first-term identity, target Cauchy estimate, KL/FI comparison, slowed-velocity scaling, and inverse-schedule product identity, SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar derives the t-time pre-DV inequality dK/dt <= -dot{s}(t)*C_LSI(t)*K(t)+(1/2)*dot{s}(t)^(-1)*||v_t||^2."
  source := saldForwardKlDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle60ForwardKlSkeletonMiddleContract",
    "SALD.cycle60ForwardKlSkeletonMiddleObligation",
    "SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar",
    "SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar",
    "SALD.forwardKlMassConservationDropScalar",
    "SALD.forwardKlMassConservationFirstTermFisherScalar",
    "SALD.forwardKlDerivativeCandidateContract",
    "SALD.forwardKlDerivativeSideConditionContract",
    "SALD.forwardKlDerivativeObligation",
    "SALD.forwardKlDensityBoundaryObligation",
    "SALD.forwardKlScheduleTimeChangeObligation",
    "SALD.saldLsiKlFiDensityTestContract",
    "sald.forward_kl.kl_derivative",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "probability.lsi_to_kl_fi"
  ]
  note := "This is formalized only as Real/order/equality bookkeeping. It keeps mass conservation, KL differentiation, Fokker-Planck, boundary integration by parts, target transport, LSI density-test, and inverse-function calculus as explicit obligations, and it does not promote thm:forward-KL or sald.forward_kl.kl_derivative."

/-- Cycle-60 proof-DAG pane for the post-cycle-59 continuous forward-KL
skeleton route. -/