AutoSamplingTheory.SALD.cycle39ForwardKlDerivativeMiddleContract

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 cycle39ForwardKlDerivativeMiddleContract :
    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:168-228 into source-shaped scalar derivative lemmas: keep the existing KL derivative, first-term, target Cauchy, and LSI premises explicit, and reduce the schedule-side premises to dot{s}(t)*dot{t}(s(t))=1 plus norm-square scaling for tilde v_s=dot{t}(s)v_{t(s)}.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:168-185 still supplies the KL derivative display and first-term Fisher identity only through the density/boundary obligation.
2. appendix.tex:199-208 still supplies the target-side Cauchy input before the existing Young scalar lemma can be used.
3. appendix.tex:210-217 still supplies the source KL/FI comparison through probability.lsi_to_kl_fi and the cycle 38 density-test scalar handoff; SALD.forwardKlLsiDerivativeBoundOfKlFiScalar converts it to the half-Fisher derivative form.
4. appendix.tex:191-197 defines tilde v_s=dot{t}(s)v_{t(s)}; the new scalar lemma SALD.forwardKlVelocitySquareScalingScalar proves the square scaling after the analytic norm identities are supplied.
5. appendix.tex:218-228 uses the inverse schedule; SALD.forwardKlInverseScheduleDerivativeScalar and SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar prove the Real algebra from the supplied product identity dotS*dotT=1.
6. The composed source-shaped pipeline is SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar, which still assumes all analytic premises explicitly.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.forwardKlInverseScheduleDerivativeScalar only after sald.forward_kl.schedule_time_change supplies dotS*dotT=1 from inverse-function calculus.
2. Use SALD.forwardKlVelocitySquareScalingScalar only after the slowed-target transport/L2 backend supplies scalar norm-square identities for tildeVelocitySq and velocitySq.
3. Use SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar and SALD.forwardKlPreDvDerivativeBoundOfProductScalar to avoid requiring lower work to pre-rewrite dotT as dotS^-1.
4. Use SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar when the LSI input has already been converted to the half-Fisher premise.
5. Use SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar when the LSI backend supplies the paper's source-shaped KL/FI comparison rather than the already-multiplied half-Fisher premise.
6. Keep SALD.forwardKlDensityBoundaryObligation, SALD.forwardKlScheduleTimeChangeObligation, probability.lsi_to_kl_fi, and sald.forward_kl.kl_derivative at obligation status.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. No SLT theorem applies to the inverse-schedule or velocity-square scalar algebra.
2. eq:LSI-KL-FI remains an open density-test backend; lem:dv_variation and lem:gronwall are downstream and not used by the pre-DV scalar pipeline.
3. The source-cited analytic facts are not promoted: inverse-function calculus, Fokker--Planck, integration by parts, and L2 transport remain named obligations.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle39_derivative_middle
2. sald.forward_kl.cycle39_derivative_upper
3. sald.forward_kl.density_boundary_regular
4. sald.forward_kl.schedule_time_change
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. First lower slice: verify or reuse SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar as the source-shaped scalar target for appendix.tex:168-228.
2. Second lower slice: refine sald.forward_kl.schedule_time_change to supply dotS*dotT=1, nonnegativity of dotS, the KL chain rule hdKdt, and scalar norm-square inputs from tilde v_s=dotT*v.
3. Third lower slice: refine sald.forward_kl.density_boundary_regular for appendix.tex:168-185 if the KL derivative display or first-term FI identity is still missing.
4. Do not touch DV, Gronwall, endpoint rewrites, coefficient-chain audit, or EM interpolation in this lower packet.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlInverseScheduleDerivativeScalar, SALD.forwardKlVelocitySquareScalingScalar, SALD.forwardKlLsiDerivativeBoundOfKlFiScalar, and SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar compile and are scalar Real lemmas only.
2. The middle packet does not mark sald.forward_kl.schedule_time_change, sald.forward_kl.density_boundary_regular, probability.lsi_to_kl_fi, or sald.forward_kl.kl_derivative formalized.
3. The theorem statement and all source coefficients in appendix.tex:168-228 remain unchanged.
4. No source-index rebaseline or external SLT/SDE import is introduced.

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 cycle39ForwardKlDerivativeMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Translate appendix.tex:168-228 into source-shaped scalar derivative lemmas: keep the existing KL derivative, first-term, target Cauchy, and LSI premises explicit, and reduce the schedule-side premises to dot{s}(t)*dot{t}(s(t))=1 plus norm-square scaling for tilde v_s=dot{t}(s)v_{t(s)}."
  sourceStepMap := [
    "appendix.tex:168-185 still supplies the KL derivative display and first-term Fisher identity only through the density/boundary obligation.",
    "appendix.tex:199-208 still supplies the target-side Cauchy input before the existing Young scalar lemma can be used.",
    "appendix.tex:210-217 still supplies the source KL/FI comparison through probability.lsi_to_kl_fi and the cycle 38 density-test scalar handoff; SALD.forwardKlLsiDerivativeBoundOfKlFiScalar converts it to the half-Fisher derivative form.",
    "appendix.tex:191-197 defines tilde v_s=dot{t}(s)v_{t(s)}; the new scalar lemma SALD.forwardKlVelocitySquareScalingScalar proves the square scaling after the analytic norm identities are supplied.",
    "appendix.tex:218-228 uses the inverse schedule; SALD.forwardKlInverseScheduleDerivativeScalar and SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar prove the Real algebra from the supplied product identity dotS*dotT=1.",
    "The composed source-shaped pipeline is SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar, which still assumes all analytic premises explicitly."
  ]
  leanStepMap := [
    "Use SALD.forwardKlInverseScheduleDerivativeScalar only after sald.forward_kl.schedule_time_change supplies dotS*dotT=1 from inverse-function calculus.",
    "Use SALD.forwardKlVelocitySquareScalingScalar only after the slowed-target transport/L2 backend supplies scalar norm-square identities for tildeVelocitySq and velocitySq.",
    "Use SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar and SALD.forwardKlPreDvDerivativeBoundOfProductScalar to avoid requiring lower work to pre-rewrite dotT as dotS^-1.",
    "Use SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar when the LSI input has already been converted to the half-Fisher premise.",
    "Use SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar when the LSI backend supplies the paper's source-shaped KL/FI comparison rather than the already-multiplied half-Fisher premise.",
    "Keep SALD.forwardKlDensityBoundaryObligation, SALD.forwardKlScheduleTimeChangeObligation, probability.lsi_to_kl_fi, and sald.forward_kl.kl_derivative at obligation status."
  ]
  citedResultInterfaces := [
    "No SLT theorem applies to the inverse-schedule or velocity-square scalar algebra.",
    "eq:LSI-KL-FI remains an open density-test backend; lem:dv_variation and lem:gronwall are downstream and not used by the pre-DV scalar pipeline.",
    "The source-cited analytic facts are not promoted: inverse-function calculus, Fokker--Planck, integration by parts, and L2 transport remain named obligations."
  ]
  obligations := [
    "sald.forward_kl.cycle39_derivative_middle",
    "sald.forward_kl.cycle39_derivative_upper",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.kl_derivative"
  ]
  lowerPacket := [
    "First lower slice: verify or reuse SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar as the source-shaped scalar target for appendix.tex:168-228.",
    "Second lower slice: refine sald.forward_kl.schedule_time_change to supply dotS*dotT=1, nonnegativity of dotS, the KL chain rule hdKdt, and scalar norm-square inputs from tilde v_s=dotT*v.",
    "Third lower slice: refine sald.forward_kl.density_boundary_regular for appendix.tex:168-185 if the KL derivative display or first-term FI identity is still missing.",
    "Do not touch DV, Gronwall, endpoint rewrites, coefficient-chain audit, or EM interpolation in this lower packet."
  ]
  reviewerChecklist := [
    "SALD.forwardKlInverseScheduleDerivativeScalar, SALD.forwardKlVelocitySquareScalingScalar, SALD.forwardKlLsiDerivativeBoundOfKlFiScalar, and SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar compile and are scalar Real lemmas only.",
    "The middle packet does not mark sald.forward_kl.schedule_time_change, sald.forward_kl.density_boundary_regular, probability.lsi_to_kl_fi, or sald.forward_kl.kl_derivative formalized.",
    "The theorem statement and all source coefficients in appendix.tex:168-228 remain unchanged.",
    "No source-index rebaseline or external SLT/SDE import is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-35 upper packet for the discrete EM interpolation Fokker--Planck sprint.

The earlier proof-closure items have current scalar or source-cited slices, so
this packet returns to item (5): the Euler--Maruyama interpolation endpoint
and conditional-drift Fokker--Planck backend in `appendix.tex:260-385`.
It reuses the cycle-15 EM spine instead of broadening the transcript.
-/