AutoSamplingTheory.SALD.cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeDag

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 cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeDag :
    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.cycle111.middle_target_time_derivative_boundary
interface : String (explicit)
Text describing intended mathematical interface.
Middle source map: inside appendix.tex:1358-1366, isolate the target-time term -int (hat rho_s / tilde pi_s) * partial_s tilde pi_s dx from the remaining pure no-mass finite-KL llr KL-differentiability package.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource — 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.cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeMiddleObligation
2. ASTIS.SALD.cycle105.remaining_pure_raw_kl_boundary
3. eq:general_KL_derivative_0_discrete
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.kl_derivative
2. sald.general_moving_target_discrete.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.cycle111.lower_packet.target_time_dominated_derivative
interface : String (explicit)
Text describing intended mathematical interface.
Compiled lower theorem: a fixed density-ratio weight, pointwise target-density derivative, local derivative domination, and target-time term identification imply weighted derivative integrability and the HasDerivAt formula for the weighted target integral.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource — 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.cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeLowerObligation
2. SALD.generalMovingTargetDiscreteTargetTimeDerivativeOfDominated
3. Mathlib.Analysis.Calculus.ParametricIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le
4. appendix.tex:1358-1366
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. ASTIS.SALD.cycle105.remaining_pure_raw_kl_boundary
2. sald.general_moving_target_discrete.kl_derivative
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.cycle111.lower_packet.target_time_source_ratio_congr
interface : String (explicit)
Text describing intended mathematical interface.
Compiled lower bridge: if the chosen target-time weight agrees a.e. with the paper's source density-ratio representative, then the target-time integral, weighted-derivative integrability, and HasDerivAt formula transfer to that source ratio by a.e. integral congruence.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource — 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.generalMovingTargetDiscreteTargetTimeDerivativeSourceRatioCongr
2. MeasureTheory.integral_congr_ae
3. MeasureTheory.Integrable.congr
4. appendix.tex:1358-1366
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. ASTIS.SALD.cycle111.remaining_pure_raw_kl_after_target_time
2. SALD.generalMovingTargetDiscretePureRawKlTargetTimeFieldsOfDominated
3. sald.general_moving_target_discrete.kl_derivative
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.cycle111.lower_packet.target_time_fields_for_pure_raw_kl
interface : String (explicit)
Text describing intended mathematical interface.
Compiled field handoff: finite KL supplies Mathlib llr regularity, and the dominated target-time theorem supplies the two target-time fields consumed by SALD.GeneralMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlr through explicit source-specific bridges.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource — 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.generalMovingTargetDiscretePureRawKlTargetTimeFieldsOfDominated
2. SALD.generalMovingTargetDiscreteKlLogRatioRegularityOfFiniteKl
3. SALD.generalMovingTargetDiscreteTargetTimeDerivativeOfDominated
4. SALD.GeneralMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlr
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. SALD.generalMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlrHkl
2. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfPureNoMassRawKlBoundaryAtFiniteKlLlrWithLogAction
3. thm:forward-KL-discrete
4. 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.cycle111.remaining_pure_raw_kl_after_target_time
interface : String (explicit)
Text describing intended mathematical interface.
Remaining exact theorem after the target-time narrowing: prove the a.e. equality identifying the fixed weight with the source density-ratio representative hat rho_s / tilde pi_s, prove the target-density pointwise derivative/domination package and source bridges, and separately prove endpoint-safe first-term KL differentiation at the finite-KL llr weak test.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource — 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. ASTIS.SALD.cycle105.remaining_pure_raw_kl_boundary
2. SALD.generalMovingTargetDiscretePureRawKlTargetTimeFieldsOfDominated
3. SALD.generalMovingTargetDiscreteTargetTimeDerivativeSourceRatioCongr
4. SALD.GeneralMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlr
5. appendix.tex:1358-1366
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.kl_derivative
2. sald.general_moving_target_discrete.em_interpolation_fp
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 cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeDag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle111.middle_target_time_derivative_boundary"
      interface := "Middle source map: inside appendix.tex:1358-1366, isolate the target-time term -int (hat rho_s / tilde pi_s) * partial_s tilde pi_s dx from the remaining pure no-mass finite-KL llr KL-differentiability package."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeMiddleObligation",
        "ASTIS.SALD.cycle105.remaining_pure_raw_kl_boundary",
        "eq:general_KL_derivative_0_discrete"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.kl_derivative",
        "sald.general_moving_target_discrete.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle111.lower_packet.target_time_dominated_derivative"
      interface := "Compiled lower theorem: a fixed density-ratio weight, pointwise target-density derivative, local derivative domination, and target-time term identification imply weighted derivative integrability and the HasDerivAt formula for the weighted target integral."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle111GeneralMovingTargetDiscreteTargetTimeDerivativeLowerObligation",
        "SALD.generalMovingTargetDiscreteTargetTimeDerivativeOfDominated",
        "Mathlib.Analysis.Calculus.ParametricIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le",
        "appendix.tex:1358-1366"
      ]
      reusedBy := [
        "ASTIS.SALD.cycle105.remaining_pure_raw_kl_boundary",
        "sald.general_moving_target_discrete.kl_derivative"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle111.lower_packet.target_time_source_ratio_congr"
      interface := "Compiled lower bridge: if the chosen target-time weight agrees a.e. with the paper's source density-ratio representative, then the target-time integral, weighted-derivative integrability, and HasDerivAt formula transfer to that source ratio by a.e. integral congruence."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteTargetTimeDerivativeSourceRatioCongr",
        "MeasureTheory.integral_congr_ae",
        "MeasureTheory.Integrable.congr",
        "appendix.tex:1358-1366"
      ]
      reusedBy := [
        "ASTIS.SALD.cycle111.remaining_pure_raw_kl_after_target_time",
        "SALD.generalMovingTargetDiscretePureRawKlTargetTimeFieldsOfDominated",
        "sald.general_moving_target_discrete.kl_derivative"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle111.lower_packet.target_time_fields_for_pure_raw_kl"
      interface := "Compiled field handoff: finite KL supplies Mathlib llr regularity, and the dominated target-time theorem supplies the two target-time fields consumed by SALD.GeneralMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlr through explicit source-specific bridges."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscretePureRawKlTargetTimeFieldsOfDominated",
        "SALD.generalMovingTargetDiscreteKlLogRatioRegularityOfFiniteKl",
        "SALD.generalMovingTargetDiscreteTargetTimeDerivativeOfDominated",
        "SALD.GeneralMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlr"
      ]
      reusedBy := [
        "SALD.generalMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlrHkl",
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfPureNoMassRawKlBoundaryAtFiniteKlLlrWithLogAction",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle111.remaining_pure_raw_kl_after_target_time"
      interface := "Remaining exact theorem after the target-time narrowing: prove the a.e. equality identifying the fixed weight with the source density-ratio representative hat rho_s / tilde pi_s, prove the target-density pointwise derivative/domination package and source bridges, and separately prove endpoint-safe first-term KL differentiation at the finite-KL llr weak test."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "ASTIS.SALD.cycle105.remaining_pure_raw_kl_boundary",
        "SALD.generalMovingTargetDiscretePureRawKlTargetTimeFieldsOfDominated",
        "SALD.generalMovingTargetDiscreteTargetTimeDerivativeSourceRatioCongr",
        "SALD.GeneralMovingTargetDiscretePureRawKlDerivativeNoMassAtFiniteKlLlr",
        "appendix.tex:1358-1366"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.kl_derivative",
        "sald.general_moving_target_discrete.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 112: named `barB` conditional-expectation representative -/

/-- Cycle-112 middle obligation for the selected named `barB` representative.

The active source slice is `appendix.tex:1368-1377`.  This packet narrows the
remaining `hbarBCondExp` premise after cycle 110 by replacing it with the
standard uniqueness characterization of conditional expectation.
-/

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