AutoSamplingTheory.SALD.cycle35DiscreteForwardKlEmFpMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle35DiscreteForwardKlEmFpMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract

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

interpolationSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

accumulatedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteAccumulatedErrorSource — 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 the cycle-35 EM interpolation Fokker-Planck target into proof-producing local algebra plus precise analytic obligations: endpoint vector identities for appendix.tex:260-266, conditional drift and density interfaces for appendix.tex:347-364, and divergence-regrouping algebra for appendix.tex:377-385.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:260-266 defines the frozen interpolation hat X_s = X_k^eta+(s-s_k)*nabla log pi_{t_k}(X_k^eta)+sqrt(2)*(W_s-W_{s_k}).
2. appendix.tex:334-335 uses the endpoint laws hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta before differentiating KL on one EM interval.
3. appendix.tex:347-354 defines the frozen conditional drift bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x].
4. appendix.tex:357-364 invokes the conditional-drift Fokker-Planck equation partial_s hat rho_s=-div(hat rho_s*bar b_{k,s})+Delta hat rho_s.
5. appendix.tex:365-385 splits Delta hat rho_s relative to tilde pi_s and regroups the drift as grad log tilde pi_s - bar b_{k,s} before the KL derivative handoff.

leanStepMap : List String (explicit)

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

Ordered data items

1. SALD.discreteForwardKlEmInterpolationLeftEndpointVector compiles only the left endpoint algebra after the Brownian increment and time increment vanish.
2. SALD.discreteForwardKlEmInterpolationRightEndpointVector compiles only the right endpoint algebra after the mesh identity and EM update definition are supplied.
3. SALD.discreteForwardKlConditionalFpDivergenceDriftSplit compiles the additive regrouping of the divergence terms after linearity and the analytic Laplacian split are supplied.
4. SALD.discreteForwardKlEmInterpolationSideConditionContract still owns endpoint law matching, conditional frozen drift, interpolation Fokker-Planck, density regularity, and stitched intervals.
5. SALD.cycle15DiscreteForwardKlConditionalDriftDensityContract and SALD.cycle15DiscreteForwardKlEmConditionalFpLowerContract remain the analytic interfaces for bar b_{k,s} and the conditional Fokker-Planck theorem.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. No SLT theorem is imported for the endpoint algebra or divergence regrouping.
2. SLT one_step_discretization remains only a reference pattern for future EM analytic work; it is not used as a dependency.
3. The conditional-drift Fokker-Planck theorem remains a local analytic obligation below formalized status.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle35_em_fp_middle
2. sald.discrete_forward_kl.cycle35_em_fp_upper
3. sald.discrete_forward_kl.em_endpoint_laws
4. sald.discrete_forward_kl.conditional_drift_density
5. sald.discrete_forward_kl.em_conditional_fokker_planck
6. sald.discrete_forward_kl.em_interpolation_fp
7. sald.discrete_forward_kl.stitched_interval_regularity

lowerPacket : List String (explicit)

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

Ordered data items

1. Use the endpoint-vector lemmas only as pointwise algebra inside sald.discrete_forward_kl.em_endpoint_laws; the law equality still needs the stochastic endpoint interface.
2. Use the divergence regrouping lemma only after the conditional-drift FP equation, Laplacian split, and linearity of divergence have been supplied.
3. Next lower proof-producing target: connect the endpoint vector lemmas to a source-cited endpoint-law interface, or refine the regular conditional law/measurability contract for bar b_{k,s}.
4. Do not move to frozen Gamma/Delta, DV velocity, Gronwall, or accumulated-error collection until the EM conditional-FP backend has a precise theorem interface.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The three new Lean theorems are theorem-independent algebra and make no claim about stochastic laws, densities, Fokker-Planck validity, or integration by parts.
2. SALD.discreteForwardKlProofDag and SALD.saldDependenciesForLabel "thm:forward-KL-discrete" expose the cycle-35 middle packet and the three compiled helper lemmas.
3. The endpoint, conditional-drift density, conditional-FP, EM interpolation, and stitched-interval obligations remain obligation status.
4. No theorem constants, source route, or source file selection changes.

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 cycle35DiscreteForwardKlEmFpMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteConditionalFpSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Translate the cycle-35 EM interpolation Fokker-Planck target into proof-producing local algebra plus precise analytic obligations: endpoint vector identities for appendix.tex:260-266, conditional drift and density interfaces for appendix.tex:347-364, and divergence-regrouping algebra for appendix.tex:377-385."
  sourceStepMap := [
    "appendix.tex:260-266 defines the frozen interpolation hat X_s = X_k^eta+(s-s_k)*nabla log pi_{t_k}(X_k^eta)+sqrt(2)*(W_s-W_{s_k}).",
    "appendix.tex:334-335 uses the endpoint laws hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta before differentiating KL on one EM interval.",
    "appendix.tex:347-354 defines the frozen conditional drift bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x].",
    "appendix.tex:357-364 invokes the conditional-drift Fokker-Planck equation partial_s hat rho_s=-div(hat rho_s*bar b_{k,s})+Delta hat rho_s.",
    "appendix.tex:365-385 splits Delta hat rho_s relative to tilde pi_s and regroups the drift as grad log tilde pi_s - bar b_{k,s} before the KL derivative handoff."
  ]
  leanStepMap := [
    "SALD.discreteForwardKlEmInterpolationLeftEndpointVector compiles only the left endpoint algebra after the Brownian increment and time increment vanish.",
    "SALD.discreteForwardKlEmInterpolationRightEndpointVector compiles only the right endpoint algebra after the mesh identity and EM update definition are supplied.",
    "SALD.discreteForwardKlConditionalFpDivergenceDriftSplit compiles the additive regrouping of the divergence terms after linearity and the analytic Laplacian split are supplied.",
    "SALD.discreteForwardKlEmInterpolationSideConditionContract still owns endpoint law matching, conditional frozen drift, interpolation Fokker-Planck, density regularity, and stitched intervals.",
    "SALD.cycle15DiscreteForwardKlConditionalDriftDensityContract and SALD.cycle15DiscreteForwardKlEmConditionalFpLowerContract remain the analytic interfaces for bar b_{k,s} and the conditional Fokker-Planck theorem."
  ]
  citedResultInterfaces := [
    "No SLT theorem is imported for the endpoint algebra or divergence regrouping.",
    "SLT one_step_discretization remains only a reference pattern for future EM analytic work; it is not used as a dependency.",
    "The conditional-drift Fokker-Planck theorem remains a local analytic obligation below formalized status."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle35_em_fp_middle",
    "sald.discrete_forward_kl.cycle35_em_fp_upper",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.conditional_drift_density",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "sald.discrete_forward_kl.em_interpolation_fp",
    "sald.discrete_forward_kl.stitched_interval_regularity"
  ]
  lowerPacket := [
    "Use the endpoint-vector lemmas only as pointwise algebra inside sald.discrete_forward_kl.em_endpoint_laws; the law equality still needs the stochastic endpoint interface.",
    "Use the divergence regrouping lemma only after the conditional-drift FP equation, Laplacian split, and linearity of divergence have been supplied.",
    "Next lower proof-producing target: connect the endpoint vector lemmas to a source-cited endpoint-law interface, or refine the regular conditional law/measurability contract for bar b_{k,s}.",
    "Do not move to frozen Gamma/Delta, DV velocity, Gronwall, or accumulated-error collection until the EM conditional-FP backend has a precise theorem interface."
  ]
  reviewerChecklist := [
    "The three new Lean theorems are theorem-independent algebra and make no claim about stochastic laws, densities, Fokker-Planck validity, or integration by parts.",
    "SALD.discreteForwardKlProofDag and SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" expose the cycle-35 middle packet and the three compiled helper lemmas.",
    "The endpoint, conditional-drift density, conditional-FP, EM interpolation, and stitched-interval obligations remain obligation status.",
    "No theorem constants, source route, or source file selection changes."
  ]
  status := ProofStatus.obligation

/-- Cycle-40 middle packet for the EM endpoint and conditional-FP backend.

This keeps the proof-closure priority on item (5) and refines the cycle-35 EM
spine with law-level endpoint handoffs.  The conditional-drift
Fokker--Planck theorem, density/disintegration, Laplacian chain rule, and
integration-by-parts backend remain explicit obligations.
-/