AutoSamplingTheory.SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefDag

Data definition / provenance and workflow record

Meaning and type

The result has data type List AutoSamplingTheory.ProofDagBlock. 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 cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefDag :
    List ProofDagBlock

Construction and field-by-field explanation

Construct an ordered list of the following data items. It is not a logical conjunction or proof DAG.

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.

Ordered data items

id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle109.middle_named_barB_source_def_boundary
interface : String (explicit)
Text describing intended mathematical interface.
Middle source map: appendix.tex:1368-1377 defines barB by conditioning the guide-plus-score frozen drift on hat X_s=x. The current theorem boundary is the named representative equality between that source conditional expectation and the canonical condDistrib guide-plus-score field under hatRhoS = Law(hat X_s).
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalDriftSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefMiddleObligation
2. SALD.cycle106GeneralMovingTargetDiscreteCanonicalCondDistribDriftLowerObligation
3. SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfCanonicalAeEq
4. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.em_interpolation_fp
2. sald.discrete_forward_kl.em_interpolation_fp
3. thm:forward-KL-discrete
4. thm:general-moving-target-SALD-discrete
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle109.compiled_named_barB_source_def_bridge
interface : String (explicit)
Text describing intended mathematical interface.
Compiled local bridge: SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpKernelSourceDef transports the source condExpKernel.map definition of barB through the sample-space kernel alignment and hatRhoS = Measure.map hatXAtS P to produce the downstream hatRhoS-a.e. canonical condDistrib equality.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalKernelMathlibSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpKernelSourceDef
2. SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfCanonicalAeEq
3. Mathlib.Probability.Kernel.CondDistrib
4. Mathlib.Probability.Kernel.Condexp
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. ASTIS.SALD.cycle106.remaining_named_barB_version_boundary
2. sald.general_moving_target_discrete.em_interpolation_fp
3. sald.discrete_forward_kl.em_interpolation_fp
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.formalized — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle109.lower_named_barB_condExp_source_bridge
interface : String (explicit)
Text describing intended mathematical interface.
Compiled lower theorem: SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef applies Mathlib condExp_prod_ae_eq_integral_condDistrib to the frozen guide-plus-score summand, uses Bochner integral add/smul linearity along condDistrib fibers, and transports the resulting sample-space equality through hatRhoS = Measure.map hatXAtS.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalDriftSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.cycle109GeneralMovingTargetDiscreteNamedBarBCondExpSourceLowerObligation
2. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef
3. ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib
4. SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfCanonicalAeEq
5. Mathlib.Probability.Kernel.CondDistrib
6. Mathlib.MeasureTheory.Integral.Bochner.Basic
7. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. ASTIS.SALD.cycle106.remaining_named_barB_version_boundary
2. sald.general_moving_target_discrete.em_interpolation_fp
3. sald.discrete_forward_kl.em_interpolation_fp
4. thm:forward-KL-discrete
5. thm:general-moving-target-SALD-discrete
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.formalized — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle109.remaining_condExp_source_representative_for_named_barB
interface : String (explicit)
Text describing intended mathematical interface.
Remaining exact theorem after the lower condExp source bridge: prove the paper's selected representative hbarBCondExp, namely the sample-space a.e. equality between the Mathlib conditional expectation of dotTk • guideIntegrand(hatXAtS omega, XkEta omega) + sigmaCoeff • scoreIntegrand(hatXAtS omega, XkEta omega) given mState.comap hatXAtS and barB (hatXAtS omega), plus equality-set measurability for ae_map_iff. Required hypotheses are finite/probability P, measurable hatXAtS, a.e.-measurable XkEta, standard-Borel state, CompleteSpace Vec, and guide/score Bochner integrability.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalDriftSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef
2. ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib
3. SALD.cycle109GeneralMovingTargetDiscreteNamedBarBCondExpSourceLowerObligation
4. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.em_interpolation_fp
2. sald.discrete_forward_kl.em_interpolation_fp
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle109.remaining_condExpKernel_source_def_and_kernel_alignment
interface : String (explicit)
Text describing intended mathematical interface.
Remaining exact theorem for the older condExpKernel.map route: prove the measure-valued a.e. alignment condDistrib XkEta hatXAtS P (hatXAtS omega) = condExpKernel P (mState.comap hatXAtS).map XkEta omega and prove the source condExpKernel.map conditional-expectation representative for barB. The lower condExp source bridge gives a smaller alternative route through ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib, so this node is no longer the only source-definition path.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalKernelMathlibSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefBoundary
2. AutoSamplingTheory.condDistribAeEqCondExpKernelMap
3. AutoSamplingTheory.condDistribIntegralSampleAeEqOfCondExpKernelMap
4. ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map
5. ProbabilityTheory.condExp_ae_eq_integral_condExpKernel
6. Mathlib.Probability.Kernel.CondDistrib
7. Mathlib.Probability.Kernel.Condexp
8. Mathlib.MeasureTheory.Integral.Bochner.Basic
9. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.em_interpolation_fp
2. sald.discrete_forward_kl.em_interpolation_fp
3. thm:forward-KL-discrete
4. thm:general-moving-target-SALD-discrete
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle109.reviewer_named_barB_source_def_check
interface : String (explicit)
Text describing intended mathematical interface.
Reviewer check: accept only as narrows-source-cited-boundary if the packet names either the remaining condExp source-representative theorem or the older condExpKernel source-definition theorem with imports and hypotheses, avoids a direct hbarBAe wrapper, preserves appendix.tex:1368-1377 and the EM backend, and leaves weak FP, box-trace, KL, LSI, DV, Gronwall, theorem status, SLT import, and Lake dependencies unchanged.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalDriftSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefMiddleObligation
2. SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefBoundary
3. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpKernelSourceDef
4. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef
5. ASTIS.SALD.cycle109.remaining_condExp_source_representative_for_named_barB
6. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. cycle 109 reviewer
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

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 cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefDag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle109.middle_named_barB_source_def_boundary"
      interface := "Middle source map: appendix.tex:1368-1377 defines barB by conditioning the guide-plus-score frozen drift on hat X_s=x.  The current theorem boundary is the named representative equality between that source conditional expectation and the canonical condDistrib guide-plus-score field under hatRhoS = Law(hat X_s)."
      source := saldGeneralMovingTargetDiscreteConditionalDriftSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefMiddleObligation",
        "SALD.cycle106GeneralMovingTargetDiscreteCanonicalCondDistribDriftLowerObligation",
        "SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfCanonicalAeEq",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle109.compiled_named_barB_source_def_bridge"
      interface := "Compiled local bridge: SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpKernelSourceDef transports the source condExpKernel.map definition of barB through the sample-space kernel alignment and hatRhoS = Measure.map hatXAtS P to produce the downstream hatRhoS-a.e. canonical condDistrib equality."
      source := saldGeneralMovingTargetDiscreteConditionalKernelMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpKernelSourceDef",
        "SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfCanonicalAeEq",
        "Mathlib.Probability.Kernel.CondDistrib",
        "Mathlib.Probability.Kernel.Condexp"
      ]
      reusedBy := [
        "ASTIS.SALD.cycle106.remaining_named_barB_version_boundary",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle109.lower_named_barB_condExp_source_bridge"
      interface := "Compiled lower theorem: SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef applies Mathlib condExp_prod_ae_eq_integral_condDistrib to the frozen guide-plus-score summand, uses Bochner integral add/smul linearity along condDistrib fibers, and transports the resulting sample-space equality through hatRhoS = Measure.map hatXAtS."
      source := saldGeneralMovingTargetDiscreteConditionalDriftSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle109GeneralMovingTargetDiscreteNamedBarBCondExpSourceLowerObligation",
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef",
        "ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib",
        "SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfCanonicalAeEq",
        "Mathlib.Probability.Kernel.CondDistrib",
        "Mathlib.MeasureTheory.Integral.Bochner.Basic",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "ASTIS.SALD.cycle106.remaining_named_barB_version_boundary",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle109.remaining_condExp_source_representative_for_named_barB"
      interface := "Remaining exact theorem after the lower condExp source bridge: prove the paper's selected representative hbarBCondExp, namely the sample-space a.e. equality between the Mathlib conditional expectation of dotTk • guideIntegrand(hatXAtS omega, XkEta omega) + sigmaCoeff • scoreIntegrand(hatXAtS omega, XkEta omega) given mState.comap hatXAtS and barB (hatXAtS omega), plus equality-set measurability for ae_map_iff. Required hypotheses are finite/probability P, measurable hatXAtS, a.e.-measurable XkEta, standard-Borel state, CompleteSpace Vec, and guide/score Bochner integrability."
      source := saldGeneralMovingTargetDiscreteConditionalDriftSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef",
        "ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib",
        "SALD.cycle109GeneralMovingTargetDiscreteNamedBarBCondExpSourceLowerObligation",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle109.remaining_condExpKernel_source_def_and_kernel_alignment"
      interface := "Remaining exact theorem for the older condExpKernel.map route: prove the measure-valued a.e. alignment condDistrib XkEta hatXAtS P (hatXAtS omega) = condExpKernel P (mState.comap hatXAtS).map XkEta omega and prove the source condExpKernel.map conditional-expectation representative for barB.  The lower condExp source bridge gives a smaller alternative route through ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib, so this node is no longer the only source-definition path."
      source := saldGeneralMovingTargetDiscreteConditionalKernelMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefBoundary",
        "AutoSamplingTheory.condDistribAeEqCondExpKernelMap",
        "AutoSamplingTheory.condDistribIntegralSampleAeEqOfCondExpKernelMap",
        "ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map",
        "ProbabilityTheory.condExp_ae_eq_integral_condExpKernel",
        "Mathlib.Probability.Kernel.CondDistrib",
        "Mathlib.Probability.Kernel.Condexp",
        "Mathlib.MeasureTheory.Integral.Bochner.Basic",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle109.reviewer_named_barB_source_def_check"
      interface := "Reviewer check: accept only as narrows-source-cited-boundary if the packet names either the remaining condExp source-representative theorem or the older condExpKernel source-definition theorem with imports and hypotheses, avoids a direct hbarBAe wrapper, preserves appendix.tex:1368-1377 and the EM backend, and leaves weak FP, box-trace, KL, LSI, DV, Gronwall, theorem status, SLT import, and Lake dependencies unchanged."
      source := saldGeneralMovingTargetDiscreteConditionalDriftSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefMiddleObligation",
        "SALD.cycle109GeneralMovingTargetDiscreteNamedBarBSourceDefBoundary",
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpKernelSourceDef",
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpSourceDef",
        "ASTIS.SALD.cycle109.remaining_condExp_source_representative_for_named_barB",
        "appendix.tex:1368-1377"
      ]
      reusedBy := ["cycle 109 reviewer"]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 110: named barB equality-set measurability -/

/-- Cycle-110 middle packet for the selected named `barB` representative.

This keeps the post-cycle-109 lower packet on the source conditional-drift
definition.  The only supplied side condition discharged here is the
equality-set measurability required by `ae_map_iff` in the cycle-109
product-conditional-expectation bridge; the source representative equality
itself remains the exact lower theorem.
-/

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