AutoSamplingTheory.SALD.cycle34ForwardKlDerivativeScalarObligation

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 cycle34ForwardKlDerivativeScalarObligation : 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.cycle34_derivative_scalar

statement : String (explicit)

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

Use the compiled scalar lemmas for appendix.tex lines 168-228: SALD.forwardKlTargetTransportYoungBoundScalar closes the Real Young step from the supplied Cauchy target bound; SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar combine the KL derivative display, first-term Fisher identity, and target-side bound to get dK/ds <= -(1/2)*FI+(1/2)*||tilde v_s||^2; SALD.forwardKlLsiDerivativeBoundScalar then uses the supplied LSI half-Fisher comparison C_LSI*K <= (1/2)*FI to obtain dK/ds <= -C_LSI*K+(1/2)*||tilde v_s||^2; SALD.forwardKlTimeChangedDerivativeBoundScalar performs the real-order inverse-schedule handoff once the analytic chain rule, velocity-square scaling, and inverse-derivative identities are supplied. The analytic Fokker-Planck, integration-by-parts, target transport, Cauchy input, LSI density-test, and time-change backends remain obligations.

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.cycle34ForwardKlDerivativeUpperPacket
2. SALD.cycle34ForwardKlDerivativeMiddleContract
3. SALD.forwardKlTargetTransportYoungBoundScalar
4. SALD.forwardKlPostYoungDerivativeBoundScalar
5. SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar
6. SALD.forwardKlLsiDerivativeBoundScalar
7. SALD.forwardKlLsiDerivativeBoundOfKlFiScalar
8. SALD.forwardKlTimeChangedDerivativeBoundScalar
9. SALD.forwardKlFirstTermFisherSubstitutionScalar
10. SALD.cycle30ForwardKlDensityBoundaryLowerObligation
11. SALD.forwardKlDerivativeSideConditionContract
12. SALD.forwardKlDensityBoundaryObligation
13. SALD.saldLsiKlFiDensityTestContract
14. SALD.lsiKlFiDensityTestObligation
15. sald.forward_kl.density_boundary_regular
16. probability.lsi_to_kl_fi
17. sald.forward_kl.schedule_time_change
18. sald.forward_kl.kl_derivative

note : String (explicit)

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

Cycle 34 closes only Real arithmetic/order handoffs inside the derivative block, including the target-side Young coefficient and the time-change coefficient after their analytic inputs are supplied. It does not close the KL derivative theorem, the Fokker-Planck equation, target transport/Cauchy backend, LSI-to-KL/FI, inverse-schedule calculus, DV, Gronwall, or thm:forward-KL.

def cycle34ForwardKlDerivativeScalarObligation : ProofObligation where
  id := "sald.forward_kl.cycle34_derivative_scalar"
  statement := "Use the compiled scalar lemmas for appendix.tex lines 168-228: SALD.forwardKlTargetTransportYoungBoundScalar closes the Real Young step from the supplied Cauchy target bound; SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar combine the KL derivative display, first-term Fisher identity, and target-side bound to get dK/ds <= -(1/2)*FI+(1/2)*||tilde v_s||^2; SALD.forwardKlLsiDerivativeBoundScalar then uses the supplied LSI half-Fisher comparison C_LSI*K <= (1/2)*FI to obtain dK/ds <= -C_LSI*K+(1/2)*||tilde v_s||^2; SALD.forwardKlTimeChangedDerivativeBoundScalar performs the real-order inverse-schedule handoff once the analytic chain rule, velocity-square scaling, and inverse-derivative identities are supplied. The analytic Fokker-Planck, integration-by-parts, target transport, Cauchy input, LSI density-test, and time-change backends remain obligations."
  source := saldForwardKlDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle34ForwardKlDerivativeUpperPacket",
    "SALD.cycle34ForwardKlDerivativeMiddleContract",
    "SALD.forwardKlTargetTransportYoungBoundScalar",
    "SALD.forwardKlPostYoungDerivativeBoundScalar",
    "SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar",
    "SALD.forwardKlLsiDerivativeBoundScalar",
    "SALD.forwardKlLsiDerivativeBoundOfKlFiScalar",
    "SALD.forwardKlTimeChangedDerivativeBoundScalar",
    "SALD.forwardKlFirstTermFisherSubstitutionScalar",
    "SALD.cycle30ForwardKlDensityBoundaryLowerObligation",
    "SALD.forwardKlDerivativeSideConditionContract",
    "SALD.forwardKlDensityBoundaryObligation",
    "SALD.saldLsiKlFiDensityTestContract",
    "SALD.lsiKlFiDensityTestObligation",
    "sald.forward_kl.density_boundary_regular",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.kl_derivative"
  ]
  note := "Cycle 34 closes only Real arithmetic/order handoffs inside the derivative block, including the target-side Young coefficient and the time-change coefficient after their analytic inputs are supplied. It does not close the KL derivative theorem, the Fokker-Planck equation, target transport/Cauchy backend, LSI-to-KL/FI, inverse-schedule calculus, DV, Gronwall, or thm:forward-KL."