Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

AutoSamplingTheory.SALD.generalMovingTargetDiscreteDerivativeObligation

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.

Lean statement of this data definition

The part after the colon is the output data type. This declaration takes no mathematical proof inputs.

def generalMovingTargetDiscreteDerivativeObligation : 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.kl_derivative
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 1354-1598: differentiate KL(hat rho_s||tilde pi_s), insert the general EM interpolation Fokker--Planck equation through the cycle-73 weak-FP-to-KL handoff at the log-ratio test and the cycle-78 generator-piece-to-KL composition, keep the cycle-74 source-cited conditional-kernel measure interface, the cycle-75 condDistrib orientation/source-map obligation, the cycle-80 conditional-law/measurability middle source map and lower supplied-hypothesis drift-regularity handoff, the cycle-76 endpoint-to-conditional marginal wrappers, and the cycle-77 generator-level weak-FP source-sign handoffs as blockers for the actual weak FP theorem, decompose the cross term into delta_pi^VA and dot{t}*m_t, use Young, lem:frozen_delta_cross_lip, LSI, DV, and the time change to derive the source differential inequality in 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.cycle48_em_endpoint_conditional_fp_audit
  2. SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff
  3. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
  4. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
  5. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
  6. SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap
  7. SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal
  8. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap
  9. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
  10. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff
  11. SALD.cycle70GeneralMovingTargetDiscreteConditionalLawMiddleObligation
  12. SALD.cycle70GeneralMovingTargetDiscreteConditionalLawLowerObligation
  13. SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation
  14. SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalLowerObligation
  15. SALD.cycle72GeneralMovingTargetDiscreteWeakFpMiddleObligation
  16. SALD.cycle72GeneralMovingTargetDiscreteWeakFpLowerObligation
  17. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract
  18. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff
  19. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff
  20. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff
  21. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff
  22. SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorMiddleObligation
  23. SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorLowerObligation
  24. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract
  25. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar
  26. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns
  27. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces
  28. SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpUpperObligation
  29. SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpMiddleObligation
  30. SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpLowerObligation
  31. SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorUpperObligation
  32. SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorMiddleObligation
  33. SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorLowerObligation
  34. SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface
  35. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceUpperObligation
  36. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceMiddleObligation
  37. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceLowerObligation
  38. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillUpperObligation
  39. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation
  40. SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityMiddleObligation
  41. SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityLowerObligation
  42. SALD.cycle76GeneralMovingTargetDiscreteEndpointConditionalLowerObligation
  43. SALD.generalMovingTargetDiscreteEndpointMeasureMapToConditionalCompatibility
  44. SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff
  45. AutoSamplingTheory.lawMapProdSwap
  46. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents
  47. sald.general_moving_target_discrete.derivative_side_conditions
  48. SALD.generalMovingTargetDiscretePostYoungDerivativeBoundScalar
  49. SALD.generalMovingTargetDiscretePostLsiDerivativeBoundScalar
  50. SALD.generalMovingTargetDiscretePostDvDerivativeBoundScalar
  51. SALD.generalMovingTargetDiscreteTimeChangedDerivativeBoundScalar
  52. SALD.generalMovingTargetDiscreteDerivativeDvTimeChangedScalar
  53. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
  54. sald.general_moving_target_discrete.cycle54_em_fp_lower
  55. sald.general_moving_target_discrete.cycle53_derivative_dv_lower
  56. sald.general_moving_target_discrete.em_interpolation_fp
  57. sald.general_moving_target_discrete.frozen_delta_cross_lip
  58. sald.general_moving_target_discrete.constant_schedule_stitching
  59. probability.lsi_to_kl_fi
  60. probability.dv_variational_formula
  61. sald.forward_kl.density_boundary_regular
  62. sald.forward_kl.schedule_time_change
note : String (explicit)

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

This is the discrete general analogue of generalMovingTargetDerivativeObligation, with additional frozen-delta and stitched-EM interfaces. The side-condition contract records the analytic setup, cycle 74 records only the source-cited conditional-kernel measure blocker and middle source map, cycle 75 records only the condDistrib orientation and component-integral audit map, cycle 76 records only endpoint-to-conditional marginal packaging under supplied kernel hypotheses, cycle 80 records only the supplied-hypothesis composition from endpoint/kernel compatibility plus component regularity to measurable/integrable bar b_{k,s}, cycle 77 compiles only generator-level weak-FP source-sign handoffs under supplied analytic hypotheses, including the split drift/diffusion component wrapper, cycle 73 compiles only the weak-FP-to-KL scalar substitution wrappers, and cycle 53 lower compiles only the scalar Young/LSI/DV/time-change handoff after those analytic inputs are supplied.
Exact Lean data construction

Each field assignment stores the corresponding value shown above. Omitted fields use the explicitly identified schema defaults. Strings that name theorems remain strings; they do not call those theorems.

def generalMovingTargetDiscreteDerivativeObligation : ProofObligation where
  id := "sald.general_moving_target_discrete.kl_derivative"
  statement := "Formalize appendix lines 1354-1598: differentiate KL(hat rho_s||tilde pi_s), insert the general EM interpolation Fokker--Planck equation through the cycle-73 weak-FP-to-KL handoff at the log-ratio test and the cycle-78 generator-piece-to-KL composition, keep the cycle-74 source-cited conditional-kernel measure interface, the cycle-75 condDistrib orientation/source-map obligation, the cycle-80 conditional-law/measurability middle source map and lower supplied-hypothesis drift-regularity handoff, the cycle-76 endpoint-to-conditional marginal wrappers, and the cycle-77 generator-level weak-FP source-sign handoffs as blockers for the actual weak FP theorem, decompose the cross term into delta_pi^VA and dot{t}*m_t, use Young, lem:frozen_delta_cross_lip, LSI, DV, and the time change to derive the source differential inequality in t."
  source := saldGeneralMovingTargetDiscreteDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract",
    "SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap",
    "SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff",
    "SALD.cycle70GeneralMovingTargetDiscreteConditionalLawMiddleObligation",
    "SALD.cycle70GeneralMovingTargetDiscreteConditionalLawLowerObligation",
    "SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalMiddleObligation",
    "SALD.cycle71GeneralMovingTargetDiscreteEndpointConditionalLowerObligation",
    "SALD.cycle72GeneralMovingTargetDiscreteWeakFpMiddleObligation",
    "SALD.cycle72GeneralMovingTargetDiscreteWeakFpLowerObligation",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff",
    "SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorMiddleObligation",
    "SALD.cycle77GeneralMovingTargetDiscreteWeakFpGeneratorLowerObligation",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces",
    "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpUpperObligation",
    "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpMiddleObligation",
    "SALD.cycle73GeneralMovingTargetDiscreteKlDerivativeWeakFpLowerObligation",
    "SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorUpperObligation",
    "SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorMiddleObligation",
    "SALD.cycle78GeneralMovingTargetDiscreteKlDerivativeGeneratorLowerObligation",
    "SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface",
    "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceUpperObligation",
    "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceMiddleObligation",
    "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceLowerObligation",
      "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillUpperObligation",
      "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation",
      "SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityMiddleObligation",
      "SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityLowerObligation",
      "SALD.cycle76GeneralMovingTargetDiscreteEndpointConditionalLowerObligation",
      "SALD.generalMovingTargetDiscreteEndpointMeasureMapToConditionalCompatibility",
      "SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff",
      "AutoSamplingTheory.lawMapProdSwap",
      "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents",
    "sald.general_moving_target_discrete.derivative_side_conditions",
    "SALD.generalMovingTargetDiscretePostYoungDerivativeBoundScalar",
    "SALD.generalMovingTargetDiscretePostLsiDerivativeBoundScalar",
    "SALD.generalMovingTargetDiscretePostDvDerivativeBoundScalar",
    "SALD.generalMovingTargetDiscreteTimeChangedDerivativeBoundScalar",
    "SALD.generalMovingTargetDiscreteDerivativeDvTimeChangedScalar",
    "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff",
    "sald.general_moving_target_discrete.cycle54_em_fp_lower",
    "sald.general_moving_target_discrete.cycle53_derivative_dv_lower",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.frozen_delta_cross_lip",
    "sald.general_moving_target_discrete.constant_schedule_stitching",
    "probability.lsi_to_kl_fi",
    "probability.dv_variational_formula",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change"
  ]
  note := "This is the discrete general analogue of generalMovingTargetDerivativeObligation, with additional frozen-delta and stitched-EM interfaces. The side-condition contract records the analytic setup, cycle 74 records only the source-cited conditional-kernel measure blocker and middle source map, cycle 75 records only the condDistrib orientation and component-integral audit map, cycle 76 records only endpoint-to-conditional marginal packaging under supplied kernel hypotheses, cycle 80 records only the supplied-hypothesis composition from endpoint/kernel compatibility plus component regularity to measurable/integrable bar b_{k,s}, cycle 77 compiles only generator-level weak-FP source-sign handoffs under supplied analytic hypotheses, including the split drift/diffusion component wrapper, cycle 73 compiles only the weak-FP-to-KL scalar substitution wrappers, and cycle 53 lower compiles only the scalar Young/LSI/DV/time-change handoff after those analytic inputs are supplied."

Existing module entry · Audited data-reader index · All teaching coverage