AutoSamplingTheory.SALD.cycle34ForwardKlDerivativeMiddleContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.ForwardKlMiddleSourceToLeanContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle34ForwardKlDerivativeMiddleContract :
    ForwardKlMiddleSourceToLeanContract

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.

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlSource — audited data reference, not expanded and not a compiled dependency edge

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlProofSource — audited data reference, not expanded and not a compiled dependency edge

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — audited data reference, not expanded and not a compiled dependency edge

dvSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDvEnergySource — audited data reference, not expanded and not a compiled dependency edge

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlGronwallSource — audited data reference, not expanded and not a compiled dependency edge

objective : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Translate appendix.tex:218-228 into a compiled scalar time-change handoff for the continuous forward-KL derivative, after the post-Young and LSI scalar inequalities from appendix.tex:168-217 have been supplied.

sourceStepMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. appendix.tex:210-217 supplies the s-time inequality dK/ds <= -C_LSI(t(s))*K_s+(1/2)*||tilde v_s||^2 through the existing post-Young and LSI scalar lemmas.
2. appendix.tex:218-222 applies the analytic chain rule d/dt K(s(t))=dot{s}(t)*dK/ds at s=s(t); Lean uses this as the input hdKdt.
3. appendix.tex:191-197 gives tilde v_s=dot{t}(s)*v_{t(s)}, so the L2 square scales as ||tilde v_s||^2=dot{t}(s)^2*||v_t||^2; Lean uses this as the input hvelocity.
4. appendix.tex:223-228 rewrites dot{s}(t)*dot{t}(s(t))^2 to dot{s}(t)^(-1), requiring dot{t}(s(t))=dot{s}(t)^(-1), dot{s}(t) != 0, and nonnegative dot{s}(t).
5. The resulting t-time pre-DV inequality is dK/dt <= -dot{s}(t)*C_LSI(t)*K(t)+(1/2)*dot{s}(t)^(-1)*||v_t||^2.

leanStepMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. SALD.forwardKlTimeChangedDerivativeBoundScalar compiles the real-order handoff from the supplied s-time bound to the t-time pre-DV inequality.
2. SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlLsiDerivativeBoundScalar remain the compiled inputs for appendix.tex:168-217.
3. SALD.forwardKlScheduleTimeChangeObligation still owns the analytic chain rule, inverse-schedule derivative identity, velocity-square scaling, and dot{s}(t) positivity/nonzero facts.
4. SALD.forwardKlDerivativeObligation may use the scalar lemma only after the density/boundary backend, LSI comparison, and schedule-time-change inputs are available.

citedResultInterfaces : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. No SLT theorem applies to this scalar time-change handoff.
2. eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall remain separate obligations/source-cited dependencies and are not promoted by this middle packet.

obligations : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. sald.forward_kl.cycle34_derivative_middle
2. sald.forward_kl.cycle34_derivative_scalar
3. sald.forward_kl.schedule_time_change
4. sald.forward_kl.density_boundary_regular
5. probability.lsi_to_kl_fi
6. sald.forward_kl.kl_derivative

lowerPacket : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. If continuing the derivative sprint, target exactly SALD.forwardKlScheduleTimeChangeObligation / sald.forward_kl.schedule_time_change.
2. First lower sub-slice: prove or precisely interface the analytic chain-rule input d/dt K(s(t))=dot{s}(t)*dK/ds and the inverse derivative identity dot{t}(s(t))=dot{s}(t)^(-1).
3. Second sub-slice: expose the L2 velocity-square scaling ||tilde v_s||^2=dot{t}(s)^2*||v_t||^2 under the slowed target transport identity.
4. Use SALD.forwardKlTimeChangedDerivativeBoundScalar only after those inputs are supplied; do not mark the schedule backend, KL derivative theorem, DV, Gronwall, or thm:forward-KL formalized.

reviewerChecklist : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. SALD.forwardKlTimeChangedDerivativeBoundScalar is a scalar Real theorem and does not prove the analytic chain rule or inverse-function theorem.
2. SALD.forwardKlScheduleTimeChangeObligation remains obligation status and lists the scalar theorem as a downstream bookkeeping helper.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes the cycle-34 middle contract and the new scalar lemma.
4. No source theorem statement or coefficient is changed, and the mandatory ASTIS check passes.

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def cycle34ForwardKlDerivativeMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Translate appendix.tex:218-228 into a compiled scalar time-change handoff for the continuous forward-KL derivative, after the post-Young and LSI scalar inequalities from appendix.tex:168-217 have been supplied."
  sourceStepMap := [
    "appendix.tex:210-217 supplies the s-time inequality dK/ds <= -C_LSI(t(s))*K_s+(1/2)*||tilde v_s||^2 through the existing post-Young and LSI scalar lemmas.",
    "appendix.tex:218-222 applies the analytic chain rule d/dt K(s(t))=dot{s}(t)*dK/ds at s=s(t); Lean uses this as the input hdKdt.",
    "appendix.tex:191-197 gives tilde v_s=dot{t}(s)*v_{t(s)}, so the L2 square scales as ||tilde v_s||^2=dot{t}(s)^2*||v_t||^2; Lean uses this as the input hvelocity.",
    "appendix.tex:223-228 rewrites dot{s}(t)*dot{t}(s(t))^2 to dot{s}(t)^(-1), requiring dot{t}(s(t))=dot{s}(t)^(-1), dot{s}(t) != 0, and nonnegative dot{s}(t).",
    "The resulting t-time pre-DV inequality is dK/dt <= -dot{s}(t)*C_LSI(t)*K(t)+(1/2)*dot{s}(t)^(-1)*||v_t||^2."
  ]
  leanStepMap := [
    "SALD.forwardKlTimeChangedDerivativeBoundScalar compiles the real-order handoff from the supplied s-time bound to the t-time pre-DV inequality.",
    "SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlLsiDerivativeBoundScalar remain the compiled inputs for appendix.tex:168-217.",
    "SALD.forwardKlScheduleTimeChangeObligation still owns the analytic chain rule, inverse-schedule derivative identity, velocity-square scaling, and dot{s}(t) positivity/nonzero facts.",
    "SALD.forwardKlDerivativeObligation may use the scalar lemma only after the density/boundary backend, LSI comparison, and schedule-time-change inputs are available."
  ]
  citedResultInterfaces := [
    "No SLT theorem applies to this scalar time-change handoff.",
    "eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall remain separate obligations/source-cited dependencies and are not promoted by this middle packet."
  ]
  obligations := [
    "sald.forward_kl.cycle34_derivative_middle",
    "sald.forward_kl.cycle34_derivative_scalar",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.density_boundary_regular",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.kl_derivative"
  ]
  lowerPacket := [
    "If continuing the derivative sprint, target exactly SALD.forwardKlScheduleTimeChangeObligation / sald.forward_kl.schedule_time_change.",
    "First lower sub-slice: prove or precisely interface the analytic chain-rule input d/dt K(s(t))=dot{s}(t)*dK/ds and the inverse derivative identity dot{t}(s(t))=dot{s}(t)^(-1).",
    "Second sub-slice: expose the L2 velocity-square scaling ||tilde v_s||^2=dot{t}(s)^2*||v_t||^2 under the slowed target transport identity.",
    "Use SALD.forwardKlTimeChangedDerivativeBoundScalar only after those inputs are supplied; do not mark the schedule backend, KL derivative theorem, DV, Gronwall, or thm:forward-KL formalized."
  ]
  reviewerChecklist := [
    "SALD.forwardKlTimeChangedDerivativeBoundScalar is a scalar Real theorem and does not prove the analytic chain rule or inverse-function theorem.",
    "SALD.forwardKlScheduleTimeChangeObligation remains obligation status and lists the scalar theorem as a downstream bookkeeping helper.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes the cycle-34 middle contract and the new scalar lemma.",
    "No source theorem statement or coefficient is changed, and the mandatory ASTIS check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-39 upper packet for the continuous forward-KL derivative sprint.

This packet follows the current proof-closure focus: keep the source theorem
fixed and translate `appendix.tex:168-228` into the forward-KL
Fokker--Planck/KL derivative identity before returning to ledger expansion or
the EM interpolation backend.
-/