AutoSamplingTheory.SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeDag

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 cycle93GeneralMovingTargetDiscreteKlMassDerivativeDag :
    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.cycle93.middle_kl_mass_derivative_source_map
interface : String (explicit)
Text describing intended mathematical interface.
Middle source map: appendix.tex:1358-1366 differentiates KL(hat rho_s||tilde pi_s), keeps the target-time term with the paper's minus sign, and drops int partial_s hat rho_s dx=0. Cycle 93 targets only that mass-drop sub-boundary by using hat rho_s=Law(hat X_s) and the mapped-law constant weak-test derivative.
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.cycle93GeneralMovingTargetDiscreteKlMassDerivativeMiddleObligation
2. SALD.cycle92GeneralMovingTargetDiscreteWeakFpGeneratorSplitLowerObligation
3. SALD.cycle87GeneralMovingTargetDiscreteKlLogRatioBoundaryLowerObligation
4. SALD.cycle88GeneralMovingTargetDiscreteKlLogRatioAdmissibilityLowerObligation
5. 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
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.obligation — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.cycle93.lower_law_constant_test_mass
interface : String (explicit)
Text describing intended mathematical interface.
Lower proof-producing theorem: SALD.generalMovingTargetDiscreteKlMassTermZeroOfLawConstantTestDerivative proves massTerm=0 from the derivative of integral 1 d Measure.map (hatX s) P; SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfLawConstantTestMassAndSourceSignsWithLogAction then feeds that result into the raw KL plus weak-FP source-sign handoff without a primitive hmass premise.
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.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation
2. SALD.generalMovingTargetDiscreteKlMassTermZeroOfLawConstantTestDerivative
3. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfLawConstantTestMassAndSourceSignsWithLogAction
4. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfRawKlAndSourceSignsWithLogAction
5. AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfRawKlAndSourceSignsWithLogAction
2. sald.general_moving_target_discrete.kl_derivative
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.cycle93.lower_finite_kl_llr_law_mass_handoff
interface : String (explicit)
Text describing intended mathematical interface.
Lower proof-producing theorem: SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfFiniteKlLlrLawConstantTestMassWithLogAction specializes the law-constant mass handoff to the exact Mathlib llr hatRho tildePi weak test. Finite KL plus SALD.GeneralMovingTargetDiscreteKlLogRatioAdmissibilityClosure supplies admissibility, so this composite no longer needs primitive hlog or hmass inputs; raw KL differentiation, target-time identification, the closure package internals, weak FP, IBP, and FI remain explicit boundaries.
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.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation
2. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfFiniteKlLlrLawConstantTestMassWithLogAction
3. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfLawConstantTestMassAndSourceSignsWithLogAction
4. SALD.generalMovingTargetDiscreteKlMassTermZeroOfLawConstantTestDerivative
5. SALD.generalMovingTargetDiscreteKlLogRatioAdmissibleOfFiniteKlClosure
6. SALD.GeneralMovingTargetDiscreteKlLogRatioAdmissibilityClosure
7. SALD.generalMovingTargetDiscreteKlLogRatioRegularityOfFiniteKl
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
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.cycle93.remaining_raw_kl_target_time_boundary
interface : String (explicit)
Text describing intended mathematical interface.
Remaining exact boundary after the finite-KL llr and law-mass handoff: prove hklRaw by differentiating KL(hat rho_s||tilde pi_s) under the integral at the Mathlib llr weak test, identify massTerm with the constant-test derivative, and prove the target-time derivative formula int (hat rho_s/tilde pi_s) partial_s tilde pi_s. The cycle-88 closure package internals, downstream IBP, and FI identification remain separate.
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.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation
2. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfFiniteKlLlrLawConstantTestMassWithLogAction
3. SALD.generalMovingTargetDiscreteKlLogRatioRegularityOfFiniteKl
4. SALD.generalMovingTargetDiscreteKlLogRatioAdmissibleOfFiniteKlClosure
5. SALD.generalMovingTargetDiscreteWeakConditionalFpLawDerivativeOfSampleSplitGeneratorHandoff
6. Mathlib.InformationTheory.KullbackLeibler.Basic
7. Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
8. Mathlib.Analysis.Calculus.ParametricIntegral
9. 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.discrete_forward_kl.kl_derivative
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

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 cycle93GeneralMovingTargetDiscreteKlMassDerivativeDag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle93.middle_kl_mass_derivative_source_map"
      interface := "Middle source map: appendix.tex:1358-1366 differentiates KL(hat rho_s||tilde pi_s), keeps the target-time term with the paper's minus sign, and drops int partial_s hat rho_s dx=0. Cycle 93 targets only that mass-drop sub-boundary by using hat rho_s=Law(hat X_s) and the mapped-law constant weak-test derivative."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeMiddleObligation",
        "SALD.cycle92GeneralMovingTargetDiscreteWeakFpGeneratorSplitLowerObligation",
        "SALD.cycle87GeneralMovingTargetDiscreteKlLogRatioBoundaryLowerObligation",
        "SALD.cycle88GeneralMovingTargetDiscreteKlLogRatioAdmissibilityLowerObligation",
        "eq:general_KL_derivative_0_discrete"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.kl_derivative",
        "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.cycle93.lower_law_constant_test_mass"
      interface := "Lower proof-producing theorem: SALD.generalMovingTargetDiscreteKlMassTermZeroOfLawConstantTestDerivative proves massTerm=0 from the derivative of integral 1 d Measure.map (hatX s) P; SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfLawConstantTestMassAndSourceSignsWithLogAction then feeds that result into the raw KL plus weak-FP source-sign handoff without a primitive hmass premise."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation",
        "SALD.generalMovingTargetDiscreteKlMassTermZeroOfLawConstantTestDerivative",
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfLawConstantTestMassAndSourceSignsWithLogAction",
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfRawKlAndSourceSignsWithLogAction",
        "AutoSamplingTheory.lawMapIntegralHasDerivAtOfSample"
      ]
      reusedBy := [
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfRawKlAndSourceSignsWithLogAction",
        "sald.general_moving_target_discrete.kl_derivative",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle93.lower_finite_kl_llr_law_mass_handoff"
      interface := "Lower proof-producing theorem: SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfFiniteKlLlrLawConstantTestMassWithLogAction specializes the law-constant mass handoff to the exact Mathlib llr hatRho tildePi weak test. Finite KL plus SALD.GeneralMovingTargetDiscreteKlLogRatioAdmissibilityClosure supplies admissibility, so this composite no longer needs primitive hlog or hmass inputs; raw KL differentiation, target-time identification, the closure package internals, weak FP, IBP, and FI remain explicit boundaries."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation",
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfFiniteKlLlrLawConstantTestMassWithLogAction",
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfLawConstantTestMassAndSourceSignsWithLogAction",
        "SALD.generalMovingTargetDiscreteKlMassTermZeroOfLawConstantTestDerivative",
        "SALD.generalMovingTargetDiscreteKlLogRatioAdmissibleOfFiniteKlClosure",
        "SALD.GeneralMovingTargetDiscreteKlLogRatioAdmissibilityClosure",
        "SALD.generalMovingTargetDiscreteKlLogRatioRegularityOfFiniteKl"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.kl_derivative",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle93.remaining_raw_kl_target_time_boundary"
      interface := "Remaining exact boundary after the finite-KL llr and law-mass handoff: prove hklRaw by differentiating KL(hat rho_s||tilde pi_s) under the integral at the Mathlib llr weak test, identify massTerm with the constant-test derivative, and prove the target-time derivative formula int (hat rho_s/tilde pi_s) partial_s tilde pi_s. The cycle-88 closure package internals, downstream IBP, and FI identification remain separate."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation",
        "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfFiniteKlLlrLawConstantTestMassWithLogAction",
        "SALD.generalMovingTargetDiscreteKlLogRatioRegularityOfFiniteKl",
        "SALD.generalMovingTargetDiscreteKlLogRatioAdmissibleOfFiniteKlClosure",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpLawDerivativeOfSampleSplitGeneratorHandoff",
        "Mathlib.InformationTheory.KullbackLeibler.Basic",
        "Mathlib.MeasureTheory.Measure.LogLikelihoodRatio",
        "Mathlib.Analysis.Calculus.ParametricIntegral",
        "appendix.tex:1358-1366"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.kl_derivative",
        "sald.discrete_forward_kl.kl_derivative",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 94: conditional-drift weak action boundary -/

/-- Cycle-94 middle obligation for the conditional-drift source-action
boundary.

This returns to the weak Fokker--Planck invocation at `appendix.tex:1379-1387`
after the cycle-93 KL/log-ratio mass handoff.  The selected supplied hypothesis
is the primitive `hdriftSource` input used by the cycle-77/82/92 weak-FP source
routes.  The new lower-ready boundary factors that input through the paper's
conditional drift `bar b_{k,s}`: first identify the frozen drift generator
action with the weak test-gradient pairing against `barB`, then prove the
source-cited no-boundary divergence identity for that pairing.
-/

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