AutoSamplingTheory.SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillDag

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 cycle75GeneralMovingTargetDiscreteConditionalLawBackfillDag :
    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.cycle75.global_phase_judgment
interface : String (explicit)
Text describing intended mathematical interface.
Cycle 75 judgment: cycle 74 passed and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the largest remaining shared risk is still the conditional-law layer inside sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387.
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.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillUpperObligation
2. SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface
3. sald.general_moving_target_discrete.em_interpolation_fp
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL-discrete
2. thm:general-moving-target-SALD-discrete
3. 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.cycle75.middle_conditional_law_source_map
interface : String (explicit)
Text describing intended mathematical interface.
Middle source map for appendix.tex:1368-1377: Mathlib condDistrib for X_k^eta conditioned on hat X_s produces the joint law as (hat X_s,X_k^eta), so lower must bridge the existing SALD (X_k^eta,hat X_s) joint-law orientation with AutoSamplingTheory.lawMapProdSwap before using component conditional-integral measurability and integrability facts.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteDerivativeSource — 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.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation
2. SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface
3. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
4. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents
5. AutoSamplingTheory.lawMapProdSwap
6. ProbabilityTheory.compProd_map_condDistrib
7. ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib
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.cycle75.lower_packet.conditional_law_measurability
interface : String (explicit)
Text describing intended mathematical interface.
Selected lower packet: instantiate or sharpen the cycle-74 condDistrib/condExpKernel source-cited interface for appendix.tex:1368-1377, connecting the joint law, named hat rho_s marginal, regular conditional kernel, and measurable/integrable component conditional drift fields.
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.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface
2. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceMiddleObligation
3. SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceLowerObligation
4. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillLowerObligation
5. SALD.generalMovingTargetDiscreteHatRhoFirstMarginalOfSwappedJointMap
6. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents
7. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation
8. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents
9. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
10. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
11. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
12. AutoSamplingTheory.lawMapProdSwap
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.em_interpolation_fp
2. sald.general_moving_target_discrete.kl_derivative
3. 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

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 cycle75GeneralMovingTargetDiscreteConditionalLawBackfillDag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle75.global_phase_judgment"
      interface := "Cycle 75 judgment: cycle 74 passed and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the largest remaining shared risk is still the conditional-law layer inside sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387."
      source := saldGeneralMovingTargetDiscreteKlWeakFpHandoffSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillUpperObligation",
        "SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface",
        "sald.general_moving_target_discrete.em_interpolation_fp"
      ]
      reusedBy := [
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete",
        "sald.general_moving_target_discrete.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle75.middle_conditional_law_source_map"
      interface := "Middle source map for appendix.tex:1368-1377: Mathlib condDistrib for X_k^eta conditioned on hat X_s produces the joint law as (hat X_s,X_k^eta), so lower must bridge the existing SALD (X_k^eta,hat X_s) joint-law orientation with AutoSamplingTheory.lawMapProdSwap before using component conditional-integral measurability and integrability facts."
      source := saldGeneralMovingTargetDiscreteDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation",
        "SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface",
        "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract",
        "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents",
        "AutoSamplingTheory.lawMapProdSwap",
        "ProbabilityTheory.compProd_map_condDistrib",
        "ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib"
      ]
      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.cycle75.lower_packet.conditional_law_measurability"
      interface := "Selected lower packet: instantiate or sharpen the cycle-74 condDistrib/condExpKernel source-cited interface for appendix.tex:1368-1377, connecting the joint law, named hat rho_s marginal, regular conditional kernel, and measurable/integrable component conditional drift fields."
      source := saldGeneralMovingTargetDiscreteConditionalKernelMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface",
        "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceMiddleObligation",
        "SALD.cycle74GeneralMovingTargetDiscreteMeasureInterfaceLowerObligation",
        "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillLowerObligation",
        "SALD.generalMovingTargetDiscreteHatRhoFirstMarginalOfSwappedJointMap",
        "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents",
        "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation",
        "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents",
        "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
        "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract",
        "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents",
        "AutoSamplingTheory.lawMapProdSwap"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.general_moving_target_discrete.kl_derivative",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    }
  ]

/-- Cycle-76 upper packet for endpoint-law to conditional compatibility.

Cycle 75 established the swapped `condDistrib` orientation wrapper.  Cycle 76
returns to the endpoint-law bookkeeping and packages it with that swapped
conditional-kernel orientation so the weak Fokker--Planck interface can consume
one named `hat rho_s` marginal without re-auditing unrelated theorem routes.
-/

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