AutoSamplingTheory.SALD.forwardKlDerivativeObligation

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 forwardKlDerivativeObligation : 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.kl_derivative

statement : String (explicit)

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

Formalize appendix lines 166-225: differentiate K(t)=KL(rho_{s(t)}||pi_t), use the SALD Fokker-Planck equation, transport-velocity identity for pi_t, integration by parts, and LSI to derive dK/dt <= -dot{s}(t)*C_LSI(t)*K(t) + (1/2)*dot{s}(t)^(-1)*||v_t||_{L2(rho_{s(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.cycle30ForwardKlUpperPacket
2. SALD.cycle30ForwardKlMiddleContract
3. sald.forward_kl.cycle30_derivative_side_upper
4. sald.forward_kl.cycle30_derivative_side_middle
5. eq:SALD
6. eq:FP-eq
7. eq:LSI-KL-FI
8. TransportVelocityContract
9. FokkerPlanckContract
10. SALD.forwardKlMassConservationDropScalar
11. SALD.forwardKlMassConservationFirstTermFisherScalar
12. SALD.forwardKlFirstTermFisherSubstitutionScalar
13. SALD.cycle55ForwardKlDerivativeMassLowerObligation
14. sald.forward_kl.cycle30_density_boundary_lower
15. SALD.forwardKlTargetTransportYoungBoundScalar
16. SALD.forwardKlPostYoungDerivativeBoundScalar
17. SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar
18. SALD.forwardKlLsiDerivativeBoundScalar
19. SALD.forwardKlTimeChangedDerivativeBoundScalar
20. SALD.forwardKlInverseScheduleDerivativeScalar
21. SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar
22. SALD.forwardKlVelocitySquareScalingScalar
23. SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar
24. SALD.forwardKlPreDvDerivativeBoundScalar
25. SALD.forwardKlPreDvDerivativeBoundOfProductScalar
26. SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar
27. SALD.forwardKlLsiDerivativeBoundOfKlFiScalar
28. SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar
29. SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar
30. SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling
31. SALD.cycle65ForwardKlDerivativePointwiseLowerObligation
32. SALD.forwardKlDerivativeDvGronwallCoefficientOfKlFiVelocityScalingScalar
33. SALD.cycle50ForwardKlDerivativeLowerObligation
34. SALD.cycle39ForwardKlDerivativeMiddleObligation
35. sald.forward_kl.cycle34_target_young_lower
36. sald.forward_kl.cycle34_derivative_scalar
37. sald.forward_kl.cycle34_derivative_middle
38. sald.forward_kl.cycle39_derivative_middle
39. sald.forward_kl.density_boundary_regular
40. sald.forward_kl.schedule_time_change

note : String (explicit)

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

This is the main measure-theoretic KL derivative backend for thm:forward-KL; forwardKlDerivativeCandidateContract and forwardKlDerivativeSideConditionContract record the required schedule, density, boundary, and time-change interfaces before proof search. Cycle 30 selects the density/boundary slice first; cycle 34 closes only the scalar target-side Young, post-Young, LSI, and pre-rewritten time-change coefficient handoffs after their analytic inputs are supplied. Cycle 39 adds source-shaped scalar schedule and velocity-square handoffs, while the analytic KL derivative, Fokker-Planck, integration by parts, LSI, and schedule backends remain obligations.

def forwardKlDerivativeObligation : ProofObligation where
  id := "sald.forward_kl.kl_derivative"
  statement := "Formalize appendix lines 166-225: differentiate K(t)=KL(rho_{s(t)}||pi_t), use the SALD Fokker-Planck equation, transport-velocity identity for pi_t, integration by parts, and LSI to derive dK/dt <= -dot{s}(t)*C_LSI(t)*K(t) + (1/2)*dot{s}(t)^(-1)*||v_t||_{L2(rho_{s(t)})}^2."
  source := saldForwardKlDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle30ForwardKlUpperPacket",
    "SALD.cycle30ForwardKlMiddleContract",
    "sald.forward_kl.cycle30_derivative_side_upper",
    "sald.forward_kl.cycle30_derivative_side_middle",
    "eq:SALD",
    "eq:FP-eq",
      "eq:LSI-KL-FI",
      "TransportVelocityContract",
      "FokkerPlanckContract",
      "SALD.forwardKlMassConservationDropScalar",
      "SALD.forwardKlMassConservationFirstTermFisherScalar",
      "SALD.forwardKlFirstTermFisherSubstitutionScalar",
      "SALD.cycle55ForwardKlDerivativeMassLowerObligation",
      "sald.forward_kl.cycle30_density_boundary_lower",
      "SALD.forwardKlTargetTransportYoungBoundScalar",
      "SALD.forwardKlPostYoungDerivativeBoundScalar",
      "SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar",
      "SALD.forwardKlLsiDerivativeBoundScalar",
      "SALD.forwardKlTimeChangedDerivativeBoundScalar",
      "SALD.forwardKlInverseScheduleDerivativeScalar",
      "SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar",
      "SALD.forwardKlVelocitySquareScalingScalar",
      "SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar",
      "SALD.forwardKlPreDvDerivativeBoundScalar",
      "SALD.forwardKlPreDvDerivativeBoundOfProductScalar",
      "SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar",
      "SALD.forwardKlLsiDerivativeBoundOfKlFiScalar",
      "SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar",
      "SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar",
      "SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling",
      "SALD.cycle65ForwardKlDerivativePointwiseLowerObligation",
      "SALD.forwardKlDerivativeDvGronwallCoefficientOfKlFiVelocityScalingScalar",
      "SALD.cycle50ForwardKlDerivativeLowerObligation",
      "SALD.cycle39ForwardKlDerivativeMiddleObligation",
      "sald.forward_kl.cycle34_target_young_lower",
      "sald.forward_kl.cycle34_derivative_scalar",
      "sald.forward_kl.cycle34_derivative_middle",
      "sald.forward_kl.cycle39_derivative_middle",
      "sald.forward_kl.density_boundary_regular",
      "sald.forward_kl.schedule_time_change"
    ]
  note := "This is the main measure-theoretic KL derivative backend for thm:forward-KL; forwardKlDerivativeCandidateContract and forwardKlDerivativeSideConditionContract record the required schedule, density, boundary, and time-change interfaces before proof search. Cycle 30 selects the density/boundary slice first; cycle 34 closes only the scalar target-side Young, post-Young, LSI, and pre-rewritten time-change coefficient handoffs after their analytic inputs are supplied. Cycle 39 adds source-shaped scalar schedule and velocity-square handoffs, while the analytic KL derivative, Fokker-Planck, integration by parts, LSI, and schedule backends remain obligations."