AutoSamplingTheory.SALD.generalMovingTargetDiscreteEmInterpolationObligation

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteEmInterpolationObligation : ProofObligation

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.

id : String (explicit)

Stable obligation identifier.

sald.general_moving_target_discrete.em_interpolation_fp

statement : String (explicit)

Desired mathematical or workflow content as String; it is not a proposition in Prop and the def does not prove it.

Formalize appendix lines 957-996 and 1354-1387: the discrete general VA-SALD EM interpolation has endpoint laws rho_k^eta, rho_{k+1}^eta and satisfies the conditional-drift Fokker--Planck equation with diffusion coefficient sigma_eta^2/2. The named-interpolation endpoint law pair now compiles from pointwise endpoint identities and law representations, cycle 64 records the regular conditional drift interface for bar b_{k,s} and compiles only its abstract linear-combination algebra, cycle 70 compiles only the named component drift and component-regularity handoffs, cycle 71 compiles only the Measure.map second-marginal identification and supplied kernel-compatibility transport from the joint law to the named hat rho_s marginal, cycle 72 records the weak-test FP source-sign interface and compiles only the test-indexed and admissible-test coefficient/sign packaging with -div drift and +(sigma_eta^2/2) Delta diffusion, cycle 73 compiles only the scalar substitution of that supplied weak FP identity into the differentiated KL formula at the log-ratio test, including a direct composition through the cycle-72 admissible source-sign wrapper, cycle 74 records the blocked condExpKernel/conditional-kernel Mathlib measure interface as sourceCited, middle-synchronizes the exact condDistrib/condExpKernel audit map for appendix.tex:1368-1377, and lower compiles only a supplied-kernel compatibility/regularity wrapper, cycle 75 middle sharpens the condDistrib orientation handoff from the existing (X_k^eta,hat X_s) joint-law naming to Mathlib's (hat X_s,X_k^eta) conditioning order, while cycle 75 lower compiles only the first-marginal, swap-orientation, and supplied-kernel regularity wrapper under explicit component-integral hypotheses, cycle 76 compiles only endpoint Measure.map-to-conditional compatibility wrappers that package endpoint laws, the swapped first marginal, the original second marginal, the swap equality, and original-orientation kernel compatibility under supplied hypotheses, cycle 80 lower compiles only the composition of that endpoint/conditional compatibility package with supplied component conditional-integral regularity to obtain measurable/integrable bar b_{k,s}, cycle 77 compiles only generator-level weak-FP source-sign handoffs from supplied generator/time-derivative, generator-expansion, and split drift/diffusion source-action hypotheses to the exact -div drift and +(sigma_eta^2/2) Delta diffusion statement, cycle 78 middle maps those supplied generator pieces to the differentiated KL display and cycle 78 lower compiles only the equality composition at the admissible log-ratio test, cycle 69 compiles only the source-sign/coefficient rewrite for the supplied weak FP identity, and the cycle-54 lower handoff compiles only the sigma-weighted divergence regrouping after the FP and Laplacian identities are supplied; the conditional-drift Fokker--Planck and KL differentiation backends remain open.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

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

status : AutoSamplingTheory.ProofStatus (explicit)

Stored ProofStatus, default obligation; even an explicitly stored formalized does not independently certify a Lean theorem.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

dependsOn : List String (explicit)

List of declared dependency names as strings; may mix theorem names, obligations, source labels, or descriptions. Not the compiled dependency DAG.

Ordered data items

1. sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit
2. SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff
3. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
4. SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation
5. SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation
6. SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation
7. SALD.generalMovingTargetDiscreteConditionalDriftContract
8. SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination
9. SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination
10. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
11. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
12. SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap
13. SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal
14. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap
15. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
16. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff
17. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents
18. sald.general_moving_target_discrete.cycle64_conditional_drift_lower
19. SALD.cycle70GeneralMovingTargetDiscreteConditionalLawMiddleObligation
20. SALD.cycle70GeneralMovingTargetDiscreteConditionalLawLowerObligation
21. sald.general_moving_target_discrete.cycle70_named_conditional_drift_lower
22. SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation
23. SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalLowerObligation
24. sald.general_moving_target_discrete.cycle71_endpoint_conditional_lower
25. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract
26. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff
27. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff
28. SALD.cycle72GeneralMovingTargetDiscreteWeakFpMiddleObligation
29. SALD.cycle72GeneralMovingTargetDiscreteWeakFpLowerObligation
30. sald.general_moving_target_discrete.cycle72_weak_fp_source_signs_lower
31. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract
32. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar
33. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns
34. SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpUpperObligation
35. SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpMiddleObligation
36. SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpLowerObligation
37. sald.general_moving_target_discrete.cycle73_kl_derivative_weak_fp_lower
38. SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface
39. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceUpperObligation
40. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceMiddleObligation
41. sald.general_moving_target_discrete.cycle74_conditional_kernel_measure_interface
42. sald.general_moving_target_discrete.cycle74_measure_interface_middle
43. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation
44. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillLowerObligation
45. SALD.generalMovingTargetDiscreteHatRhoFirstMarginalOfSwappedJointMap
46. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents
47. SALD.cycle76GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation
48. SALD.cycle76GeneralMovingTargetDiscreteEndpointConditionalLowerObligation
49. SALD.generalMovingTargetDiscreteEndpointMeasureMapToSwappedConditionalCompatibility
50. SALD.generalMovingTargetDiscreteEndpointMeasureMapToConditionalCompatibility
51. SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityLowerObligation
52. SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff
53. AutoSamplingTheory.lawMapProdSwap
54. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff
55. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff
56. SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorMiddleObligation
57. SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorLowerObligation
58. sald.general_moving_target_discrete.cycle77_weak_fp_generator_lower
59. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces
60. SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorUpperObligation
61. SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorLowerObligation
62. sald.general_moving_target_discrete.cycle78_kl_derivative_generator_lower
63. SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff
64. SALD.cycle69GeneralMovingTargetDiscreteEmFpSourceSignsLowerObligation
65. sald.general_moving_target_discrete.cycle69_em_fp_source_signs_lower
66. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
67. sald.general_moving_target_discrete.cycle54_em_fp_lower
68. EulerMaruyamaContract
69. FokkerPlanckContract
70. KLContract
71. FIContract

note : String (explicit)

Recorded evidence/caveats; may distinguish a compiled scalar helper from still-open source analysis.

This is the general VA analogue of the SALD EM interpolation backend; endpoint-law handoffs, conditional-drift linearity algebra, named component regularity wrappers, endpoint-to-conditional marginal transport and packaged compatibility, weak-test and admissible-test source-sign packaging, weak-FP-to-KL scalar substitution including the cycle-72 composition wrapper, the cycle-74 source-cited conditional-kernel measure interface, middle source map, lower supplied-kernel regularity wrapper, the cycle-75 condDistrib orientation source map and lower swapped-joint regularity wrapper, cycle-76 endpoint Measure.map-to-conditional compatibility packaging in both swapped and original marginal views, cycle-80 endpoint/conditional drift-regularity composition, cycle-77 generator-level source-sign handoffs including the split drift/diffusion component wrapper, cycle-78 middle source map and lower generator-piece-to-KL derivative equality composition, source-sign coefficient rewriting, and the sigma-weighted FP regrouping compile or are recorded under explicit hypotheses, while the source's common-space construction, regular conditional law, density/absolute-continuity, actual weak Fokker-Planck theorem, log-ratio admissibility, KL differentiation, and integration by parts remain obligations.

def generalMovingTargetDiscreteEmInterpolationObligation : ProofObligation where
  id := "sald.general_moving_target_discrete.em_interpolation_fp"
  statement := "Formalize appendix lines 957-996 and 1354-1387: the discrete general VA-SALD EM interpolation has endpoint laws rho_k^eta, rho_{k+1}^eta and satisfies the conditional-drift Fokker--Planck equation with diffusion coefficient sigma_eta^2/2. The named-interpolation endpoint law pair now compiles from pointwise endpoint identities and law representations, cycle 64 records the regular conditional drift interface for bar b_{k,s} and compiles only its abstract linear-combination algebra, cycle 70 compiles only the named component drift and component-regularity handoffs, cycle 71 compiles only the Measure.map second-marginal identification and supplied kernel-compatibility transport from the joint law to the named hat rho_s marginal, cycle 72 records the weak-test FP source-sign interface and compiles only the test-indexed and admissible-test coefficient/sign packaging with -div drift and +(sigma_eta^2/2) Delta diffusion, cycle 73 compiles only the scalar substitution of that supplied weak FP identity into the differentiated KL formula at the log-ratio test, including a direct composition through the cycle-72 admissible source-sign wrapper, cycle 74 records the blocked condExpKernel/conditional-kernel Mathlib measure interface as sourceCited, middle-synchronizes the exact condDistrib/condExpKernel audit map for appendix.tex:1368-1377, and lower compiles only a supplied-kernel compatibility/regularity wrapper, cycle 75 middle sharpens the condDistrib orientation handoff from the existing (X_k^eta,hat X_s) joint-law naming to Mathlib's (hat X_s,X_k^eta) conditioning order, while cycle 75 lower compiles only the first-marginal, swap-orientation, and supplied-kernel regularity wrapper under explicit component-integral hypotheses, cycle 76 compiles only endpoint Measure.map-to-conditional compatibility wrappers that package endpoint laws, the swapped first marginal, the original second marginal, the swap equality, and original-orientation kernel compatibility under supplied hypotheses, cycle 80 lower compiles only the composition of that endpoint/conditional compatibility package with supplied component conditional-integral regularity to obtain measurable/integrable bar b_{k,s}, cycle 77 compiles only generator-level weak-FP source-sign handoffs from supplied generator/time-derivative, generator-expansion, and split drift/diffusion source-action hypotheses to the exact -div drift and +(sigma_eta^2/2) Delta diffusion statement, cycle 78 middle maps those supplied generator pieces to the differentiated KL display and cycle 78 lower compiles only the equality composition at the admissible log-ratio test, cycle 69 compiles only the source-sign/coefficient rewrite for the supplied weak FP identity, and the cycle-54 lower handoff compiles only the sigma-weighted divergence regrouping after the FP and Laplacian identities are supplied; the conditional-drift Fokker--Planck and KL differentiation backends remain open."
  source := saldGeneralMovingTargetDiscreteEmSource
  status := ProofStatus.obligation
  dependsOn := ["sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit", "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff", "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation", "SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation", "SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation", "SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation", "SALD.generalMovingTargetDiscreteConditionalDriftContract", "SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination", "SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination", "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract", "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract", "SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap", "SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal", "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap", "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents", "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff", "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents", "sald.general_moving_target_discrete.cycle64_conditional_drift_lower", "SALD.cycle70GeneralMovingTargetDiscreteConditionalLawMiddleObligation", "SALD.cycle70GeneralMovingTargetDiscreteConditionalLawLowerObligation", "sald.general_moving_target_discrete.cycle70_named_conditional_drift_lower", "SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation", "SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalLowerObligation", "sald.general_moving_target_discrete.cycle71_endpoint_conditional_lower", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff", "SALD.cycle72GeneralMovingTargetDiscreteWeakFpMiddleObligation", "SALD.cycle72GeneralMovingTargetDiscreteWeakFpLowerObligation", "sald.general_moving_target_discrete.cycle72_weak_fp_source_signs_lower", "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract", "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar", "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns", "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpUpperObligation", "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpMiddleObligation", "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpLowerObligation", "sald.general_moving_target_discrete.cycle73_kl_derivative_weak_fp_lower", "SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface", "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceUpperObligation", "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceMiddleObligation", "sald.general_moving_target_discrete.cycle74_conditional_kernel_measure_interface", "sald.general_moving_target_discrete.cycle74_measure_interface_middle", "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation", "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillLowerObligation", "SALD.generalMovingTargetDiscreteHatRhoFirstMarginalOfSwappedJointMap", "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents", "SALD.cycle76GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation", "SALD.cycle76GeneralMovingTargetDiscreteEndpointConditionalLowerObligation", "SALD.generalMovingTargetDiscreteEndpointMeasureMapToSwappedConditionalCompatibility", "SALD.generalMovingTargetDiscreteEndpointMeasureMapToConditionalCompatibility", "SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityLowerObligation", "SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff", "AutoSamplingTheory.lawMapProdSwap", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff", "SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorMiddleObligation", "SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorLowerObligation", "sald.general_moving_target_discrete.cycle77_weak_fp_generator_lower", "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces", "SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorUpperObligation", "SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorLowerObligation", "sald.general_moving_target_discrete.cycle78_kl_derivative_generator_lower", "SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff", "SALD.cycle69GeneralMovingTargetDiscreteEmFpSourceSignsLowerObligation", "sald.general_moving_target_discrete.cycle69_em_fp_source_signs_lower", "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff", "sald.general_moving_target_discrete.cycle54_em_fp_lower", "EulerMaruyamaContract", "FokkerPlanckContract", "KLContract", "FIContract"]
  note := "This is the general VA analogue of the SALD EM interpolation backend; endpoint-law handoffs, conditional-drift linearity algebra, named component regularity wrappers, endpoint-to-conditional marginal transport and packaged compatibility, weak-test and admissible-test source-sign packaging, weak-FP-to-KL scalar substitution including the cycle-72 composition wrapper, the cycle-74 source-cited conditional-kernel measure interface, middle source map, lower supplied-kernel regularity wrapper, the cycle-75 condDistrib orientation source map and lower swapped-joint regularity wrapper, cycle-76 endpoint Measure.map-to-conditional compatibility packaging in both swapped and original marginal views, cycle-80 endpoint/conditional drift-regularity composition, cycle-77 generator-level source-sign handoffs including the split drift/diffusion component wrapper, cycle-78 middle source map and lower generator-piece-to-KL derivative equality composition, source-sign coefficient rewriting, and the sigma-weighted FP regrouping compile or are recorded under explicit hypotheses, while the source's common-space construction, regular conditional law, density/absolute-continuity, actual weak Fokker-Planck theorem, log-ratio admissibility, KL differentiation, and integration by parts remain obligations."