AutoSamplingTheory.SALD.cycle49MainSkeletonAnalyticReadinessDag

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 cycle49MainSkeletonAnalyticReadinessDag : 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.cycle49.analytic_readiness
interface : String (explicit)
Text describing intended mathematical interface.
Post-route check that Gronwall, DV, LSI/KL/FI, continuous KL derivative, and EM interpolation Fokker--Planck have explicit source-cited or obligation interfaces before lower work resumes.
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.cycle49MainSkeletonAnalyticReadinessLedger
2. SALD.cycle49MainSkeletonAnalyticReadinessObligation
3. SALD.cycle44MainSkeletonAnalyticInterfaceDag
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL
2. thm:forward-KL-discrete
3. prop:guided_path_residual
4. thm:general-moving-target-SALD
5. thm:unified-forward-KL
6. 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.cycle49.middle_route_audit
interface : String (explicit)
Text describing intended mathematical interface.
Middle source-to-Lean audit for the post-route analytic readiness ledger: verify the five backend interfaces against the six theorem consumers and keep appendix.tex:1354-1387 as the next lower EM endpoint/conditional-law/Fokker--Planck slice.
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.cycle49MainSkeletonAnalyticMiddleContract
2. SALD.cycle49MainSkeletonAnalyticMiddleObligation
3. SALD.cycle49MainSkeletonAnalyticReadinessObligation
4. SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation
5. SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff
6. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
7. sald.general_moving_target_discrete.em_interpolation_fp
8. sald.general_moving_target_discrete.kl_derivative
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL
2. thm:forward-KL-discrete
3. prop:guided_path_residual
4. thm:general-moving-target-SALD
5. thm:unified-forward-KL
6. thm:general-moving-target-SALD-discrete
7. cycle49 lower packet
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.cycle49.lower_packet.general_discrete_em_fp
interface : String (explicit)
Text describing intended mathematical interface.
Lower packet for appendix.tex:1354-1387: use the named-interpolation endpoint-law handoff for concrete named laws and pointwise endpoint identities, then expose regular conditional drift, density/AC, common space, and weak conditional Fokker--Planck before the KL derivative proof.
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.generalMovingTargetDiscreteDerivativeCandidateContract
2. SALD.generalMovingTargetDiscreteDerivativeObligation
3. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
4. SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff
5. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
6. SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation
7. sald.general_moving_target_discrete.em_interpolation_fp
8. sald.general_moving_target_discrete.kl_derivative
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:general-moving-target-SALD-discrete
2. cycle49 lower
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 cycle49MainSkeletonAnalyticReadinessDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle49.analytic_readiness"
      interface := "Post-route check that Gronwall, DV, LSI/KL/FI, continuous KL derivative, and EM interpolation Fokker--Planck have explicit source-cited or obligation interfaces before lower work resumes."
      source := saldGeneralMovingTargetDiscreteDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle49MainSkeletonAnalyticReadinessLedger",
        "SALD.cycle49MainSkeletonAnalyticReadinessObligation",
        "SALD.cycle44MainSkeletonAnalyticInterfaceDag"
      ]
      reusedBy := [
        "thm:forward-KL",
        "thm:forward-KL-discrete",
        "prop:guided_path_residual",
        "thm:general-moving-target-SALD",
        "thm:unified-forward-KL",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle49.middle_route_audit"
      interface := "Middle source-to-Lean audit for the post-route analytic readiness ledger: verify the five backend interfaces against the six theorem consumers and keep appendix.tex:1354-1387 as the next lower EM endpoint/conditional-law/Fokker--Planck slice."
      source := saldGeneralMovingTargetDiscreteDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle49MainSkeletonAnalyticMiddleContract",
        "SALD.cycle49MainSkeletonAnalyticMiddleObligation",
        "SALD.cycle49MainSkeletonAnalyticReadinessObligation",
        "SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation",
        "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff",
        "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.general_moving_target_discrete.kl_derivative"
      ]
      reusedBy := [
        "thm:forward-KL",
        "thm:forward-KL-discrete",
        "prop:guided_path_residual",
        "thm:general-moving-target-SALD",
        "thm:unified-forward-KL",
        "thm:general-moving-target-SALD-discrete",
        "cycle49 lower packet"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle49.lower_packet.general_discrete_em_fp"
      interface := "Lower packet for appendix.tex:1354-1387: use the named-interpolation endpoint-law handoff for concrete named laws and pointwise endpoint identities, then expose regular conditional drift, density/AC, common space, and weak conditional Fokker--Planck before the KL derivative proof."
      source := saldGeneralMovingTargetDiscreteDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteDerivativeCandidateContract",
        "SALD.generalMovingTargetDiscreteDerivativeObligation",
        "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract",
        "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff",
        "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation",
        "SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.general_moving_target_discrete.kl_derivative"
      ]
      reusedBy := ["thm:general-moving-target-SALD-discrete", "cycle49 lower"]
      status := ProofStatus.obligation
    }
  ]

/-- Cycle-45 upper packet for the continuous forward-KL theorem skeleton.

This keeps the cycle-44 global interface ledger in place and wires those
interfaces into the specific `thm:forward-KL` route requested for main skeleton
sprint 2.  It is workflow data only; the analytic backends remain obligations
or source-cited interfaces.
-/

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