AutoSamplingTheory.SALD.cycle15DiscreteForwardKlConditionalDriftDensityContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle15DiscreteForwardKlConditionalDriftDensityContract :
    DiscreteForwardKlConditionalDriftDensityContract

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.saldForwardKlDiscreteConditionalFpSource — audited data reference, not expanded and not a compiled dependency edge

parentPacket : String (explicit)

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

SALD.cycle15DiscreteForwardKlEmConditionalFpLowerContract

targetObligation : String (explicit)

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

sald.discrete_forward_kl.conditional_drift_density

randomVariables : String (explicit)

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

On a fixed interval [s_k,s_{k+1}], the pair (X_k^eta, hat X_s) is generated by the frozen EM interpolation in appendix.tex:260-266.

conditionalLawKernel : String (explicit)

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

appendix.tex:347-354 requires a regular conditional law for X_k^eta given hat X_s=x so bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x] is defined pointwise or almost everywhere.

densityInterface : String (explicit)

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

The law hat rho_s=Law(hat X_s) must admit a smooth positive density on the Euclidean state space before the divergence form in appendix.tex:357-364 is meaningful.

driftMeasurability : String (explicit)

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

The conditional expectation must select a measurable vector field x |-> bar b_{k,s}(x) compatible with the density hat rho_s.

driftIntegrability : String (explicit)

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

The product hat rho_s*bar b_{k,s} must have enough local integrability and weak differentiability for div(hat rho_s*bar b_{k,s}) to be used in the Fokker--Planck equation.

fokkerPlanckInput : String (explicit)

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

This contract supplies only the drift/density input to partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s; the FP identity and Laplacian split remain separate obligations.

exclusions : List String (explicit)

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

Ordered data items

1. Do not prove the Fokker--Planck equation in this interface.
2. Do not perform the Laplacian split relative to tilde pi_s.
3. Do not include endpoint stitching, frozen Gamma/Delta bounds, DV, Gronwall, or accumulated-error algebra.

dependencies : List String (explicit)

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

Ordered data items

1. eq:frozen_interp_terminal_disc_prop_additive_final
2. SALD.discreteSaldEulerMaruyamaContract
3. sald.discrete_forward_kl.em_endpoint_laws

sourceGaps : List String (explicit)

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

Ordered data items

1. The source writes the conditional expectation defining bar b_{k,s} but does not state the regular conditional probability or measurability interface.
2. The source uses hat rho_s as a density in divergence form without separately proving density existence, positivity, or smoothness for the EM interpolation law.
3. The source does not isolate the integrability needed for hat rho_s*bar b_{k,s} before applying the Fokker--Planck equation.

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 cycle15DiscreteForwardKlConditionalDriftDensityContract :
    DiscreteForwardKlConditionalDriftDensityContract where
  sourceBlock := saldForwardKlDiscreteConditionalFpSource
  parentPacket := "SALD.cycle15DiscreteForwardKlEmConditionalFpLowerContract"
  targetObligation := "sald.discrete_forward_kl.conditional_drift_density"
  randomVariables := "On a fixed interval [s_k,s_{k+1}], the pair (X_k^eta, hat X_s) is generated by the frozen EM interpolation in appendix.tex:260-266."
  conditionalLawKernel := "appendix.tex:347-354 requires a regular conditional law for X_k^eta given hat X_s=x so bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x] is defined pointwise or almost everywhere."
  densityInterface := "The law hat rho_s=Law(hat X_s) must admit a smooth positive density on the Euclidean state space before the divergence form in appendix.tex:357-364 is meaningful."
  driftMeasurability := "The conditional expectation must select a measurable vector field x |-> bar b_{k,s}(x) compatible with the density hat rho_s."
  driftIntegrability := "The product hat rho_s*bar b_{k,s} must have enough local integrability and weak differentiability for div(hat rho_s*bar b_{k,s}) to be used in the Fokker--Planck equation."
  fokkerPlanckInput := "This contract supplies only the drift/density input to partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s; the FP identity and Laplacian split remain separate obligations."
  exclusions := [
    "Do not prove the Fokker--Planck equation in this interface.",
    "Do not perform the Laplacian split relative to tilde pi_s.",
    "Do not include endpoint stitching, frozen Gamma/Delta bounds, DV, Gronwall, or accumulated-error algebra."
  ]
  dependencies := [
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "SALD.discreteSaldEulerMaruyamaContract",
    "sald.discrete_forward_kl.em_endpoint_laws"
  ]
  sourceGaps := [
    "The source writes the conditional expectation defining bar b_{k,s} but does not state the regular conditional probability or measurability interface.",
    "The source uses hat rho_s as a density in divergence form without separately proving density existence, positivity, or smoothness for the EM interpolation law.",
    "The source does not isolate the integrability needed for hat rho_s*bar b_{k,s} before applying the Fokker--Planck equation."
  ]
  status := ProofStatus.obligation