AutoSamplingTheory.SALD.cycle15DiscreteForwardKlEmConditionalFpLowerContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle15DiscreteForwardKlEmConditionalFpLowerContract :
    DiscreteForwardKlEmConditionalFpLowerContract

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.cycle15DiscreteForwardKlMiddleContract

targetObligation : String (explicit)

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

sald.discrete_forward_kl.em_conditional_fokker_planck

conditionalDriftDefinition : 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].

conditionalLawInterface : String (explicit)

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

The frozen interpolation hat X_s must provide a law hat rho_s with enough density and conditional-expectation structure for bar b_{k,s} to be a measurable drift field.

fokkerPlanckEquation : String (explicit)

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

appendix.tex:357-364 invokes partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s on each interval [s_k,s_{k+1}].

laplacianSplit : String (explicit)

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

appendix.tex:365-385 rewrites Delta hat rho_s as div(hat rho_s*nabla log(hat rho_s/tilde pi_s)) + div(hat rho_s*nabla log tilde pi_s), then groups the frozen drift defect.

klDerivativeBridge : String (explicit)

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

The output feeds appendix.tex:388-413, where integration by parts turns the divergence form into -FI(hat rho_s||tilde pi_s) and the frozen cross term.

exclusions : List String (explicit)

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

Ordered data items

1. Do not include endpoint law matching beyond the input needed to identify the interval [s_k,s_{k+1}].
2. Do not include the later frozen Gamma/Delta bound, DV velocity estimate, Gronwall accumulation, or linear-slowdown barGamma/barDelta collection.
3. Do not add theorem-level smoothness or absolute-continuity assumptions; record missing density and boundary interfaces as obligations.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.cycle15DiscreteForwardKlMiddleContract
2. SALD.cycle15DiscreteForwardKlConditionalDriftDensityContract
3. SALD.discreteForwardKlEmInterpolationSideConditionContract
4. sald.discrete_forward_kl.conditional_drift_density
5. sald.discrete_forward_kl.em_endpoint_laws
6. sald.discrete_forward_kl.em_conditional_fokker_planck
7. FokkerPlanckContract
8. KLContract
9. FIContract

sourceGaps : List String (explicit)

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

Ordered data items

1. The source names the Fokker--Planck equation associated with the frozen interpolation but does not prove it.
2. The source does not spell out the conditional-expectation regularity that makes bar b_{k,s} a drift in divergence form.
3. The Laplacian split and following integration by parts require density positivity, differentiability, and boundary decay not separately stated in the theorem.

lowerPacket : List String (explicit)

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

Ordered data items

1. First formalize sald.discrete_forward_kl.conditional_drift_density: the law/density interface for hat X_s and bar b_{k,s} on a fixed interval.
2. Then prove or cite the conditional-drift Fokker--Planck equation for the frozen EM interpolation.
3. Finally expose the Laplacian split relative to tilde pi_s as the input to the KL derivative identity.
4. Leave endpoint stitching and accumulated-error algebra to their sibling obligations.

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 cycle15DiscreteForwardKlEmConditionalFpLowerContract :
    DiscreteForwardKlEmConditionalFpLowerContract where
  sourceBlock := saldForwardKlDiscreteConditionalFpSource
  parentPacket := "SALD.cycle15DiscreteForwardKlMiddleContract"
  targetObligation := "sald.discrete_forward_kl.em_conditional_fokker_planck"
  conditionalDriftDefinition := "appendix.tex:347-354 defines bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x]."
  conditionalLawInterface := "The frozen interpolation hat X_s must provide a law hat rho_s with enough density and conditional-expectation structure for bar b_{k,s} to be a measurable drift field."
  fokkerPlanckEquation := "appendix.tex:357-364 invokes partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s on each interval [s_k,s_{k+1}]."
  laplacianSplit := "appendix.tex:365-385 rewrites Delta hat rho_s as div(hat rho_s*nabla log(hat rho_s/tilde pi_s)) + div(hat rho_s*nabla log tilde pi_s), then groups the frozen drift defect."
  klDerivativeBridge := "The output feeds appendix.tex:388-413, where integration by parts turns the divergence form into -FI(hat rho_s||tilde pi_s) and the frozen cross term."
  exclusions := [
    "Do not include endpoint law matching beyond the input needed to identify the interval [s_k,s_{k+1}].",
    "Do not include the later frozen Gamma/Delta bound, DV velocity estimate, Gronwall accumulation, or linear-slowdown barGamma/barDelta collection.",
    "Do not add theorem-level smoothness or absolute-continuity assumptions; record missing density and boundary interfaces as obligations."
  ]
  dependencies := [
    "SALD.cycle15DiscreteForwardKlMiddleContract",
    "SALD.cycle15DiscreteForwardKlConditionalDriftDensityContract",
    "SALD.discreteForwardKlEmInterpolationSideConditionContract",
    "sald.discrete_forward_kl.conditional_drift_density",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "FokkerPlanckContract",
    "KLContract",
    "FIContract"
  ]
  sourceGaps := [
    "The source names the Fokker--Planck equation associated with the frozen interpolation but does not prove it.",
    "The source does not spell out the conditional-expectation regularity that makes bar b_{k,s} a drift in divergence form.",
    "The Laplacian split and following integration by parts require density positivity, differentiability, and boundary decay not separately stated in the theorem."
  ]
  lowerPacket := [
    "First formalize sald.discrete_forward_kl.conditional_drift_density: the law/density interface for hat X_s and bar b_{k,s} on a fixed interval.",
    "Then prove or cite the conditional-drift Fokker--Planck equation for the frozen EM interpolation.",
    "Finally expose the Laplacian split relative to tilde pi_s as the input to the KL derivative identity.",
    "Leave endpoint stitching and accumulated-error algebra to their sibling obligations."
  ]
  status := ProofStatus.obligation