AutoSamplingTheory.SALD.discreteForwardKlEmInterpolationSideConditionContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlEmInterpolationSideConditionContract :
    DiscreteForwardKlEmInterpolationSideConditionContract

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.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

endpointLawMatching : String (explicit)

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

appendix.tex:260-266 defines hat X_s on [s_k,s_{k+1}], and appendix.tex:334-335 uses hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta; SALD.discreteForwardKlEmInterpolationLeftEndpointLawHandoff and SALD.discreteForwardKlEmInterpolationRightEndpointLawHandoff now compile the abstract pointwise-to-law handoff after a concrete law operator is supplied.

conditionalFrozenDrift : String (explicit)

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

appendix.tex:347-354 defines bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x].

interpolationFokkerPlanck : String (explicit)

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

appendix.tex:357-385 uses partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s and rewrites the Laplacian term relative to tilde pi_s.

densityRegularity : String (explicit)

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

The KL derivative block requires hat rho_s and tilde pi_s to have smooth positive densities, finite KL/FI, and valid integration by parts on every EM subinterval.

stitchedIntervalInterface : String (explicit)

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

The local inequalities on [s_k,s_{k+1}] must stitch through the endpoint laws so K(t)=KL(hat rho_{s(t)}||pi_t) is endpoint-continuous or absolutely continuous in the sense needed by lem:gronwall.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.em_endpoint_laws
2. sald.discrete_forward_kl.em_conditional_fokker_planck
3. sald.discrete_forward_kl.stitched_interval_regularity
4. sald.discrete_forward_kl.cycle40_em_fp_middle

sourceGaps : List String (explicit)

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

Ordered data items

1. the source states endpoint matching in the proof but does not isolate it as a lemma; the new handoff still needs the project law notation and stochastic-process endpoint definitions
2. the interpolation Fokker--Planck equation with conditional drift is invoked as a standard fact
3. the proof applies a single Gronwall bound after deriving interval-wise inequalities, without a separate stitched-interval lemma

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 discreteForwardKlEmInterpolationSideConditionContract :
    DiscreteForwardKlEmInterpolationSideConditionContract where
  sourceBlock := saldForwardKlDiscreteInterpolationSource
  endpointLawMatching := "appendix.tex:260-266 defines hat X_s on [s_k,s_{k+1}], and appendix.tex:334-335 uses hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta; SALD.discreteForwardKlEmInterpolationLeftEndpointLawHandoff and SALD.discreteForwardKlEmInterpolationRightEndpointLawHandoff now compile the abstract pointwise-to-law handoff after a concrete law operator is supplied."
  conditionalFrozenDrift := "appendix.tex:347-354 defines bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x]."
  interpolationFokkerPlanck := "appendix.tex:357-385 uses partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s and rewrites the Laplacian term relative to tilde pi_s."
  densityRegularity := "The KL derivative block requires hat rho_s and tilde pi_s to have smooth positive densities, finite KL/FI, and valid integration by parts on every EM subinterval."
  stitchedIntervalInterface := "The local inequalities on [s_k,s_{k+1}] must stitch through the endpoint laws so K(t)=KL(hat rho_{s(t)}||pi_t) is endpoint-continuous or absolutely continuous in the sense needed by lem:gronwall."
  obligations := [
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "sald.discrete_forward_kl.cycle40_em_fp_middle"
  ]
  sourceGaps := [
    "the source states endpoint matching in the proof but does not isolate it as a lemma; the new handoff still needs the project law notation and stochastic-process endpoint definitions",
    "the interpolation Fokker--Planck equation with conditional drift is invoked as a standard fact",
    "the proof applies a single Gronwall bound after deriving interval-wise inequalities, without a separate stitched-interval lemma"
  ]
  status := ProofStatus.obligation