AutoSamplingTheory.SALD.cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureLowerObligation

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 cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureLowerObligation :
    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.cycle79_weak_fp_generator_measure_lower

statement : String (explicit)

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

Cycle 79 lower compiles the narrow local Measure.map handoff used before the missing weak generator theorem: AutoSamplingTheory.lawMapIntegral rewrites an admissible weak-test integral against Law(hat X_s)=Measure.map (hat X_s) P as the corresponding sample-space integral, and AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample transports a supplied sample-space HasDerivAt result to the mapped-law weak-test integral. This reduces the measure-calculus boundary for appendix.tex:1379-1387 but still leaves the actual EM generator derivative, conditional drift construction, density/AC, boundary conditions, source-sign weak Fokker-Planck theorem, and KL derivative backend as obligations or source-cited interfaces.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpGeneratorMathlibSource — 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.formalized — 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. AutoSamplingTheory.lawMapIntegral
2. AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample
3. SALD.cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureInterface
4. SALD.cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureMiddleObligation
5. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff
6. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff
7. sald.general_moving_target_discrete.em_interpolation_fp

note : String (explicit)

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

Formalized local Measure.map/Bochner integral derivative transport under explicit supplied hypotheses only. It does not prove parametric differentiation of the EM process, Ito/generator calculus, weak Fokker-Planck source signs, log-ratio admissibility, or any theorem-level SALD backend.

def cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureLowerObligation :
    ProofObligation where
  id := "sald.general_moving_target_discrete.cycle79_weak_fp_generator_measure_lower"
  statement := "Cycle 79 lower compiles the narrow local Measure.map handoff used before the missing weak generator theorem: AutoSamplingTheory.lawMapIntegral rewrites an admissible weak-test integral against Law(hat X_s)=Measure.map (hat X_s) P as the corresponding sample-space integral, and AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample transports a supplied sample-space HasDerivAt result to the mapped-law weak-test integral. This reduces the measure-calculus boundary for appendix.tex:1379-1387 but still leaves the actual EM generator derivative, conditional drift construction, density/AC, boundary conditions, source-sign weak Fokker-Planck theorem, and KL derivative backend as obligations or source-cited interfaces."
  source := saldGeneralMovingTargetDiscreteWeakFpGeneratorMathlibSource
  status := ProofStatus.formalized
  dependsOn := [
    "AutoSamplingTheory.lawMapIntegral",
    "AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample",
    "SALD.cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureInterface",
    "SALD.cycle79GeneralMovingTargetDiscreteWeakFpGeneratorMeasureMiddleObligation",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  note := "Formalized local Measure.map/Bochner integral derivative transport under explicit supplied hypotheses only. It does not prove parametric differentiation of the EM process, Ito/generator calculus, weak Fokker-Planck source signs, log-ratio admissibility, or any theorem-level SALD backend."

/-- Cycle-79 proof-DAG pane for the weak generator-to-law cited interface. -/