AutoSamplingTheory.SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation

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 generalMovingTargetDiscreteDerivativeSideConditionObligation : 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.derivative_side_conditions

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 the side interfaces used in appendix lines 1354-1600 before the discrete general VA-SALD derivative inequality: EM endpoint laws through the compiled named-interpolation handoff, endpoint-to-conditional marginal compatibility through the cycle-71 Measure.map wrappers, regular conditional drift through the cycle-64 drift contract and linearity wrappers, the cycle-74 source-cited condExpKernel/conditional-kernel measure interface plus middle source map and lower supplied-kernel regularity wrapper for the blocked conditional-law theorem, the cycle-75 middle condDistrib orientation handoff and lower swapped-joint supplied-kernel wrapper from the existing (X_k^eta,hat X_s) joint-law name to Mathlib's (hat X_s,X_k^eta) conditioning order, the cycle-76 endpoint Measure.map-to-conditional compatibility wrappers connecting endpoint laws, named hat rho_s marginal in both swapped first-marginal and original second-marginal views, swap equality, and original-orientation kernel compatibility under supplied hypotheses, the cycle-80 endpoint/conditional drift-regularity wrapper that composes those marginal/kernel facts with supplied component conditional-integral regularity to obtain measurable/integrable bar b_{k,s}, the cycle-72 weak-test source-sign interface and wrappers for the conditional Fokker--Planck equation, including the admissible-test predicate variant, the cycle-77 generator-level handoffs splitting the supplied weak FP theorem into generator/time-derivative, generator source-expansion, and component drift/diffusion source-action hypotheses, the cycle-73 weak-FP-to-KL derivative handoff at the log-ratio test and its direct composition through the cycle-72 admissible source-sign wrapper, the cycle-78 generator-piece-to-KL derivative handoff composing the cycle-77 source-action hypotheses directly into the same log-ratio derivative display, the cycle-69 source-sign/coefficient handoff for the supplied weak conditional Fokker--Planck equation, conditional Fokker--Planck split with the cycle-54 sigma-weighted divergence regrouping, slowed transport velocity, frozen/residual algebra delta_pi^VA+dot t*m, the two sigma_eta^2/8 Young splits, DV finite-log-mgf side condition, and stitched time-change to K(t).

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

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

note : String (explicit)

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

generalMovingTargetDiscreteDerivativeSideConditionContract keeps these source steps explicit so the theorem target is not strengthened by hidden regularity or coefficient assumptions. The cycle-71 wrappers prove only Measure.map marginal/equality transport for a supplied conditional-kernel predicate, the cycle-64 lower theorem proves only conditional-expectation linear-combination algebra under supplied linearity hypotheses, cycle 74 records the source-cited Mathlib conditional-kernel interface and middle source map and proves only a supplied-kernel compatibility/regularity wrapper, cycle 75 records the condDistrib orientation map and compiles only the first-marginal/swap supplied-kernel regularity wrapper, cycle 76 compiles only endpoint Measure.map-to-conditional compatibility packaging with both swapped and original marginal views, cycle 80 compiles only the supplied-hypothesis composition from those endpoint/kernel facts and component regularity to measurable/integrable bar b_{k,s}, cycle 77 compiles only generator-level source-sign handoffs after generator/time-derivative, generator-expansion, and split drift/diffusion source-action hypotheses are supplied, the cycle-72 and cycle-69 lower theorems prove only weak-test/source-sign coefficient rewriting after the weak FP identity is supplied, cycle 73 proves only the scalar substitution of that supplied weak FP identity into the KL derivative display at an admissible log-ratio test, including the wrapper that composes through cycle 72, cycle 78 proves only the equality composition from supplied generator pieces into that same KL derivative display, and the cycle-54 lower theorem proves only the additive/sigma algebra after analytic FP identities are supplied.

def generalMovingTargetDiscreteDerivativeSideConditionObligation : ProofObligation where
  id := "sald.general_moving_target_discrete.derivative_side_conditions"
  statement := "Formalize the side interfaces used in appendix lines 1354-1600 before the discrete general VA-SALD derivative inequality: EM endpoint laws through the compiled named-interpolation handoff, endpoint-to-conditional marginal compatibility through the cycle-71 Measure.map wrappers, regular conditional drift through the cycle-64 drift contract and linearity wrappers, the cycle-74 source-cited condExpKernel/conditional-kernel measure interface plus middle source map and lower supplied-kernel regularity wrapper for the blocked conditional-law theorem, the cycle-75 middle condDistrib orientation handoff and lower swapped-joint supplied-kernel wrapper from the existing (X_k^eta,hat X_s) joint-law name to Mathlib's (hat X_s,X_k^eta) conditioning order, the cycle-76 endpoint Measure.map-to-conditional compatibility wrappers connecting endpoint laws, named hat rho_s marginal in both swapped first-marginal and original second-marginal views, swap equality, and original-orientation kernel compatibility under supplied hypotheses, the cycle-80 endpoint/conditional drift-regularity wrapper that composes those marginal/kernel facts with supplied component conditional-integral regularity to obtain measurable/integrable bar b_{k,s}, the cycle-72 weak-test source-sign interface and wrappers for the conditional Fokker--Planck equation, including the admissible-test predicate variant, the cycle-77 generator-level handoffs splitting the supplied weak FP theorem into generator/time-derivative, generator source-expansion, and component drift/diffusion source-action hypotheses, the cycle-73 weak-FP-to-KL derivative handoff at the log-ratio test and its direct composition through the cycle-72 admissible source-sign wrapper, the cycle-78 generator-piece-to-KL derivative handoff composing the cycle-77 source-action hypotheses directly into the same log-ratio derivative display, the cycle-69 source-sign/coefficient handoff for the supplied weak conditional Fokker--Planck equation, conditional Fokker--Planck split with the cycle-54 sigma-weighted divergence regrouping, slowed transport velocity, frozen/residual algebra delta_pi^VA+dot t*m, the two sigma_eta^2/8 Young splits, DV finite-log-mgf side condition, and stitched time-change to K(t)."
  source := saldGeneralMovingTargetDiscreteDerivativeSource
  status := ProofStatus.obligation
  dependsOn := ["sald.general_moving_target_discrete.cycle28_derivative_side_middle", "sald.general_moving_target_discrete.cycle28_derivative_side_lower", "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff", "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation", "SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation", "SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation", "SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation", "SALD.generalMovingTargetDiscreteConditionalDriftContract", "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract", "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract", "SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap", "SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal", "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap", "SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation", "SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalLowerObligation", "SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination", "SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination", "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents", "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff", "SALD.cycle70GeneralMovingTargetDiscreteConditionalLawMiddleObligation", "SALD.cycle70GeneralMovingTargetDiscreteConditionalLawLowerObligation", "sald.general_moving_target_discrete.cycle64_conditional_drift_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.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff", "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff", "SALD.cycle72GeneralMovingTargetDiscreteWeakFpMiddleObligation", "SALD.cycle72GeneralMovingTargetDiscreteWeakFpLowerObligation", "sald.general_moving_target_discrete.cycle72_weak_fp_source_signs_lower", "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.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract", "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar", "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns", "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpUpperObligation", "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpMiddleObligation", "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpLowerObligation", "sald.general_moving_target_discrete.cycle73_kl_derivative_weak_fp_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", "sald.general_moving_target_discrete.em_interpolation_fp", "sald.general_moving_target_discrete.frozen_delta_cross_lip", "sald.forward_kl.schedule_time_change", "TransportVelocityContract", "FokkerPlanckContract", "KLContract", "FIContract"]
  note := "generalMovingTargetDiscreteDerivativeSideConditionContract keeps these source steps explicit so the theorem target is not strengthened by hidden regularity or coefficient assumptions. The cycle-71 wrappers prove only Measure.map marginal/equality transport for a supplied conditional-kernel predicate, the cycle-64 lower theorem proves only conditional-expectation linear-combination algebra under supplied linearity hypotheses, cycle 74 records the source-cited Mathlib conditional-kernel interface and middle source map and proves only a supplied-kernel compatibility/regularity wrapper, cycle 75 records the condDistrib orientation map and compiles only the first-marginal/swap supplied-kernel regularity wrapper, cycle 76 compiles only endpoint Measure.map-to-conditional compatibility packaging with both swapped and original marginal views, cycle 80 compiles only the supplied-hypothesis composition from those endpoint/kernel facts and component regularity to measurable/integrable bar b_{k,s}, cycle 77 compiles only generator-level source-sign handoffs after generator/time-derivative, generator-expansion, and split drift/diffusion source-action hypotheses are supplied, the cycle-72 and cycle-69 lower theorems prove only weak-test/source-sign coefficient rewriting after the weak FP identity is supplied, cycle 73 proves only the scalar substitution of that supplied weak FP identity into the KL derivative display at an admissible log-ratio test, including the wrapper that composes through cycle 72, cycle 78 proves only the equality composition from supplied generator pieces into that same KL derivative display, and the cycle-54 lower theorem proves only the additive/sigma algebra after analytic FP identities are supplied."