AutoSamplingTheory.SALD.cycle40DiscreteForwardKlEmFpMiddleContract

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 cycle40DiscreteForwardKlEmFpMiddleContract :
    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.

Cycle 40 middle priority check: Gronwall, DV, LSI/KL/FI, and the continuous forward-KL derivative have current source-cited or scalar progress but still leave analytic backends open, so this packet follows item (5) and translates appendix.tex:260-385 into endpoint-law handoffs plus the existing conditional-drift Fokker-Planck obligation.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:260-266 defines 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.
3. appendix.tex:347-354 defines 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 for 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}.

leanStepMap : List String (explicit)

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

Ordered data items

1. SALD.discreteForwardKlEmInterpolationLeftEndpointVector and SALD.discreteForwardKlEmInterpolationRightEndpointVector remain the pointwise endpoint algebra.
2. SALD.discreteForwardKlLawEqOfPointwise turns any supplied pointwise equality of random variables into equality under an abstract law operator.
3. SALD.discreteForwardKlEmInterpolationLeftEndpointLawHandoff and SALD.discreteForwardKlEmInterpolationRightEndpointLawHandoff are the new endpoint-law handoffs for sald.discrete_forward_kl.em_endpoint_laws.
4. SALD.discreteForwardKlEmEndpointLawPairHandoff is the lower endpoint-law pair: after named representations for hat rho_s, rho_k^eta, and rho_{k+1}^eta are supplied, it proves both endpoint laws used at appendix.tex:334-335.
5. SALD.discreteForwardKlConditionalFpLaplacianSplitHandoff remains the source regrouping after hfp and hlap are supplied.
6. SALD.discreteForwardKlEmConditionalFpObligation remains the precise source-cited interface for conditional drift, density, Fokker-Planck, and Laplacian split.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. No SLT theorem is imported or marked formalized for EM endpoint laws.
2. The one_step_discretization pattern remains only a possible future reference route for analytic EM facts.
3. The conditional-drift Fokker-Planck theorem is local SDE/measure analysis and stays 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.cycle40_em_fp_middle
2. sald.discrete_forward_kl.em_endpoint_laws
3. sald.discrete_forward_kl.conditional_drift_density
4. sald.discrete_forward_kl.em_conditional_fokker_planck
5. sald.discrete_forward_kl.em_interpolation_fp
6. 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. First lower target: instantiate SALD.discreteForwardKlEmInterpolationLeftEndpointLawHandoff and SALD.discreteForwardKlEmInterpolationRightEndpointLawHandoff with the repository's eventual law notation for hat rho_s, rho_k^eta, and rho_{k+1}^eta; SALD.discreteForwardKlEmEndpointLawPairHandoff now proves the pair from explicit named-law representation hypotheses.
2. Second lower target: refine sald.discrete_forward_kl.conditional_drift_density for the regular conditional law and measurability/integrability of bar b_{k,s}.
3. Third lower target only if the interface is stable: state the source-cited conditional-drift Fokker-Planck theorem that supplies hfp and the Laplacian split consumed by SALD.discreteForwardKlConditionalFpLaplacianSplitHandoff.
4. Keep frozen Gamma/Delta, LSI, DV, Gronwall, coefficient-chain, and accumulated-error work outside this lower packet.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The endpoint-law handoff lemmas compile and are only abstract funext/congruence plus pointwise endpoint algebra.
2. SALD.discreteForwardKlEmEndpointLawPairHandoff compiles only under explicit named-law representation hypotheses for hat rho_s, rho_k^eta, and rho_{k+1}^eta.
3. The packet does not construct Brownian motion, regular conditional laws, densities, or the Fokker-Planck theorem.
4. sald.discrete_forward_kl.em_endpoint_laws, conditional_drift_density, em_conditional_fokker_planck, and em_interpolation_fp remain obligations.
5. The source theorem, constants, step-size condition, alpha ranges, and source files are unchanged.
6. The mandatory source-index and ASTIS checks pass.

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 cycle40DiscreteForwardKlEmFpMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteConditionalFpSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Cycle 40 middle priority check: Gronwall, DV, LSI/KL/FI, and the continuous forward-KL derivative have current source-cited or scalar progress but still leave analytic backends open, so this packet follows item (5) and translates appendix.tex:260-385 into endpoint-law handoffs plus the existing conditional-drift Fokker-Planck obligation."
  sourceStepMap := [
    "appendix.tex:260-266 defines 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.",
    "appendix.tex:347-354 defines 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 for 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}."
  ]
  leanStepMap := [
    "SALD.discreteForwardKlEmInterpolationLeftEndpointVector and SALD.discreteForwardKlEmInterpolationRightEndpointVector remain the pointwise endpoint algebra.",
    "SALD.discreteForwardKlLawEqOfPointwise turns any supplied pointwise equality of random variables into equality under an abstract law operator.",
    "SALD.discreteForwardKlEmInterpolationLeftEndpointLawHandoff and SALD.discreteForwardKlEmInterpolationRightEndpointLawHandoff are the new endpoint-law handoffs for sald.discrete_forward_kl.em_endpoint_laws.",
    "SALD.discreteForwardKlEmEndpointLawPairHandoff is the lower endpoint-law pair: after named representations for hat rho_s, rho_k^eta, and rho_{k+1}^eta are supplied, it proves both endpoint laws used at appendix.tex:334-335.",
    "SALD.discreteForwardKlConditionalFpLaplacianSplitHandoff remains the source regrouping after hfp and hlap are supplied.",
    "SALD.discreteForwardKlEmConditionalFpObligation remains the precise source-cited interface for conditional drift, density, Fokker-Planck, and Laplacian split."
  ]
  citedResultInterfaces := [
    "No SLT theorem is imported or marked formalized for EM endpoint laws.",
    "The one_step_discretization pattern remains only a possible future reference route for analytic EM facts.",
    "The conditional-drift Fokker-Planck theorem is local SDE/measure analysis and stays below formalized status."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle40_em_fp_middle",
    "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 := [
    "First lower target: instantiate SALD.discreteForwardKlEmInterpolationLeftEndpointLawHandoff and SALD.discreteForwardKlEmInterpolationRightEndpointLawHandoff with the repository's eventual law notation for hat rho_s, rho_k^eta, and rho_{k+1}^eta; SALD.discreteForwardKlEmEndpointLawPairHandoff now proves the pair from explicit named-law representation hypotheses.",
    "Second lower target: refine sald.discrete_forward_kl.conditional_drift_density for the regular conditional law and measurability/integrability of bar b_{k,s}.",
    "Third lower target only if the interface is stable: state the source-cited conditional-drift Fokker-Planck theorem that supplies hfp and the Laplacian split consumed by SALD.discreteForwardKlConditionalFpLaplacianSplitHandoff.",
    "Keep frozen Gamma/Delta, LSI, DV, Gronwall, coefficient-chain, and accumulated-error work outside this lower packet."
  ]
  reviewerChecklist := [
    "The endpoint-law handoff lemmas compile and are only abstract funext/congruence plus pointwise endpoint algebra.",
    "SALD.discreteForwardKlEmEndpointLawPairHandoff compiles only under explicit named-law representation hypotheses for hat rho_s, rho_k^eta, and rho_{k+1}^eta.",
    "The packet does not construct Brownian motion, regular conditional laws, densities, or the Fokker-Planck theorem.",
    "sald.discrete_forward_kl.em_endpoint_laws, conditional_drift_density, em_conditional_fokker_planck, and em_interpolation_fp remain obligations.",
    "The source theorem, constants, step-size condition, alpha ranges, and source files are unchanged.",
    "The mandatory source-index and ASTIS checks pass."
  ]
  status := ProofStatus.obligation