AutoSamplingTheory.SALD.cycle45ForwardKlSkeletonDag

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 cycle45ForwardKlSkeletonDag : 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.forward_KL.cycle45_theorem_skeleton_route
interface : String (explicit)
Text describing intended mathematical interface.
Continuous forward-KL theorem-level route: source statement, derivative/Fokker-Planck interface, LSI handoff, DV finite-log-mgf witness, and Gronwall endpoint/exponent side conditions compose to the exact main_body.tex:243-246 display.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlProofSource — 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.cycle45ForwardKlSkeletonUpperPacket
2. SALD.cycle45ForwardKlSkeletonObligation
3. SALD.cycle45ForwardKlSkeletonMiddleContract
4. SALD.cycle45ForwardKlSkeletonMiddleObligation
5. SALD.continuousForwardKlStatementContract
6. SALD.forwardKlDerivativeCandidateContract
7. SALD.forwardKlDerivativeSideConditionContract
8. SALD.saldLsiKlFiDensityTestContract
9. SALD.forwardKlDvFiniteLogMgfWitnessContract
10. SALD.forwardKlDvEnergyCandidateContract
11. SALD.forwardKlGronwallInstantiationContract
12. SALD.forwardKlGronwallSideConditionContract
13. SALD.discreteForwardKlEmInterpolationSideConditionContract
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL
2. thm:forward-KL-discrete theorem-route reuse
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 cycle45ForwardKlSkeletonDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route"
      interface := "Continuous forward-KL theorem-level route: source statement, derivative/Fokker-Planck interface, LSI handoff, DV finite-log-mgf witness, and Gronwall endpoint/exponent side conditions compose to the exact main_body.tex:243-246 display."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle45ForwardKlSkeletonUpperPacket",
        "SALD.cycle45ForwardKlSkeletonObligation",
        "SALD.cycle45ForwardKlSkeletonMiddleContract",
        "SALD.cycle45ForwardKlSkeletonMiddleObligation",
        "SALD.continuousForwardKlStatementContract",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.forwardKlDvEnergyCandidateContract",
        "SALD.forwardKlGronwallInstantiationContract",
        "SALD.forwardKlGronwallSideConditionContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract"
      ]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete theorem-route reuse"]
      status := ProofStatus.obligation
    }
  ]

/-- Cycle-45 middle audit for the continuous forward-KL theorem skeleton.

This is the middle-role source-to-Lean synchronization layer for the upper
route wrapper.  It checks that the theorem statement and appendix proof are
consumed through the already named analytic interfaces in the paper order, and
selects one lower-ready backend without changing the theorem display.
-/

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