Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

AutoSamplingTheory.SALD.cycle60ForwardKlSkeletonDag

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 cycle60ForwardKlSkeletonDag : 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

  1. id : String (explicit)

    Stable plan-node identifier.

    ASTIS.SALD.forward_KL.cycle60_post_cycle59_route
    interface : String (explicit)

    Text describing intended mathematical interface.

    Post-cycle-59 upper route: consume the accepted five-backend analytic ledger and cycle-55 continuous route, then wire main_body.tex:238-247 and appendix.tex:164-252 through derivative/Fokker-Planck, LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent, and downstream EM-interface visibility without changing the theorem 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.cycle60ForwardKlSkeletonUpperPacket
    2. SALD.cycle60ForwardKlSkeletonObligation
    3. SALD.cycle60ForwardKlSkeletonMiddleContract
    4. SALD.cycle60ForwardKlSkeletonMiddleObligation
    5. SALD.cycle59MainSkeletonAnalyticInterfaceObligation
    6. SALD.cycle59MainSkeletonAnalyticMiddleObligation
    7. SALD.cycle55ForwardKlSkeletonObligation
    8. SALD.cycle55ForwardKlSkeletonMiddleObligation
    9. SALD.continuousForwardKlStatementContract
    10. SALD.forwardKlDerivativeCandidateContract
    11. SALD.forwardKlDerivativeSideConditionContract
    12. SALD.saldLsiKlFiDensityTestContract
    13. SALD.forwardKlDvFiniteLogMgfWitnessContract
    14. SALD.forwardKlGronwallInstantiationContract
    15. SALD.forwardKlGronwallSideConditionContract
    16. SALD.discreteForwardKlEmInterpolationSideConditionContract
    reusedBy : List String (explicit)

    Declared consumers as strings, default empty.

    Ordered data items

    1. thm:forward-KL
    2. ASTIS-SALD-001 cycle 60
    status : AutoSamplingTheory.ProofStatus (explicit)

    Recorded workflow status, default planned.

    AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
  2. id : String (explicit)

    Stable plan-node identifier.

    ASTIS.SALD.forward_KL.cycle60_middle_route_audit
    interface : String (explicit)

    Text describing intended mathematical interface.

    Cycle-60 middle audit: verify the post-cycle-59 continuous forward-KL route in source order, keep the theorem display and constants fixed, and select appendix.tex:168-228 sald.forward_kl.kl_derivative as the lower backend while LSI, DV, Gronwall, and EM interfaces remain separate obligations.
    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.cycle60ForwardKlSkeletonMiddleContract
    2. SALD.cycle60ForwardKlSkeletonMiddleObligation
    3. SALD.cycle60ForwardKlSkeletonObligation
    4. SALD.cycle59MainSkeletonAnalyticMiddleObligation
    5. SALD.cycle55ForwardKlSkeletonMiddleObligation
    6. SALD.cycle55ForwardKlDerivativeMassLowerObligation
    7. SALD.cycle50ForwardKlDerivativeLowerObligation
    8. SALD.continuousForwardKlStatementContract
    9. SALD.forwardKlDerivativeCandidateContract
    10. SALD.forwardKlDerivativeSideConditionContract
    11. SALD.forwardKlDerivativeObligation
    12. sald.forward_kl.kl_derivative
    13. SALD.saldLsiKlFiDensityTestContract
    14. SALD.forwardKlDvFiniteLogMgfWitnessContract
    15. SALD.forwardKlGronwallInstantiationContract
    16. SALD.forwardKlGronwallSideConditionContract
    17. SALD.discreteForwardKlEmInterpolationSideConditionContract
    reusedBy : List String (explicit)

    Declared consumers as strings, default empty.

    Ordered data items

    1. thm:forward-KL
    2. cycle 60 lower derivative packet
    status : AutoSamplingTheory.ProofStatus (explicit)

    Recorded workflow status, default planned.

    AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
  3. id : String (explicit)

    Stable plan-node identifier.

    ASTIS.SALD.forward_KL.cycle60_five_backend_check
    interface : String (explicit)

    Text describing intended mathematical interface.

    Explicit cycle-60 check of the five slow interfaces before lower work: endpoint-safe Gronwall, common-space DV with finite log-mgf, LSI/KL/FI density-test bridge, continuous Fokker-Planck/KL derivative, and EM interpolation Fokker-Planck for downstream discrete reuse.
    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.saldGronwallEndpointCalculusContract
    2. SALD.forwardKlGronwallSideConditionContract
    3. dvVariationalFormulaInterface saldDvVariationSource
    4. SALD.saldDvFiniteLogMgfContract
    5. SALD.saldLsiKlFiDensityTestContract
    6. SALD.forwardKlDerivativeSideConditionContract
    7. SALD.discreteForwardKlEmInterpolationSideConditionContract
    8. SALD.cycle59MainSkeletonAnalyticInterfaceObligation
    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
  4. id : String (explicit)

    Stable plan-node identifier.

    ASTIS.SALD.forward_KL.cycle60_lower_packet.kl_derivative
    interface : String (explicit)

    Text describing intended mathematical interface.

    Selected lower packet for cycle 60: return proof-producing work to sald.forward_kl.kl_derivative over appendix.tex:168-228, starting with mass conservation, KL differentiation, SALD Fokker-Planck substitution, target transport, boundary integration by parts, and inverse-schedule calculus.
    source : AutoSamplingTheory.SourceAnchor (explicit)

    Source pointer.

    AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle60ForwardKlSkeletonObligation
    2. SALD.cycle60ForwardKlSkeletonMiddleObligation
    3. SALD.forwardKlDerivativeCandidateContract
    4. SALD.forwardKlDerivativeSideConditionContract
    5. SALD.forwardKlDerivativeObligation
    6. SALD.forwardKlDensityBoundaryObligation
    7. SALD.forwardKlScheduleTimeChangeObligation
    8. SALD.cycle60ForwardKlDerivativeRawLowerObligation
    9. SALD.cycle55ForwardKlDerivativeMassLowerObligation
    10. SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar
    11. SALD.forwardKlMassConservationDropScalar
    12. SALD.forwardKlMassConservationFirstTermFisherScalar
    13. SALD.forwardKlDerivativeDvGronwallCoefficientOfKlFiVelocityScalingScalar
    14. sald.forward_kl.density_boundary_regular
    15. sald.forward_kl.schedule_time_change
    16. sald.forward_kl.kl_derivative
    reusedBy : List String (explicit)

    Declared consumers as strings, default empty.

    Ordered data items

    1. sald.forward_kl.kl_derivative
    2. thm:forward-KL
    3. cycle 60 lower handoff
    status : AutoSamplingTheory.ProofStatus (explicit)

    Recorded workflow status, default planned.

    AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
  5. id : String (explicit)

    Stable plan-node identifier.

    ASTIS.SALD.forward_KL.cycle60_derivative_raw_lower
    interface : String (explicit)

    Text describing intended mathematical interface.

    Cycle-60 lower proof-producing scalar wrapper for appendix.tex:168-228: start from the raw KL derivative split with the mass term, drop that term by supplied mass conservation, and feed the existing first-term, target Young, LSI, slowed-velocity, and inverse-schedule pipeline to obtain the t-time pre-DV derivative inequality.
    source : AutoSamplingTheory.SourceAnchor (explicit)

    Source pointer.

    AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle60ForwardKlDerivativeRawLowerObligation
    2. SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar
    3. SALD.forwardKlMassConservationDropScalar
    4. SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar
    5. SALD.forwardKlDerivativeCandidateContract
    6. SALD.forwardKlDerivativeSideConditionContract
    7. SALD.forwardKlDerivativeObligation
    8. SALD.forwardKlDensityBoundaryObligation
    9. SALD.forwardKlScheduleTimeChangeObligation
    10. probability.lsi_to_kl_fi
    11. sald.forward_kl.density_boundary_regular
    12. sald.forward_kl.schedule_time_change
    13. sald.forward_kl.kl_derivative
    reusedBy : List String (explicit)

    Declared consumers as strings, default empty.

    Ordered data items

    1. sald.forward_kl.kl_derivative
    2. thm:forward-KL
    3. cycle 60 reviewer
    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 cycle60ForwardKlSkeletonDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.forward_KL.cycle60_post_cycle59_route"
      interface := "Post-cycle-59 upper route: consume the accepted five-backend analytic ledger and cycle-55 continuous route, then wire main_body.tex:238-247 and appendix.tex:164-252 through derivative/Fokker-Planck, LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent, and downstream EM-interface visibility without changing the theorem display."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle60ForwardKlSkeletonUpperPacket",
        "SALD.cycle60ForwardKlSkeletonObligation",
        "SALD.cycle60ForwardKlSkeletonMiddleContract",
        "SALD.cycle60ForwardKlSkeletonMiddleObligation",
        "SALD.cycle59MainSkeletonAnalyticInterfaceObligation",
        "SALD.cycle59MainSkeletonAnalyticMiddleObligation",
        "SALD.cycle55ForwardKlSkeletonObligation",
        "SALD.cycle55ForwardKlSkeletonMiddleObligation",
        "SALD.continuousForwardKlStatementContract",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.forwardKlGronwallInstantiationContract",
        "SALD.forwardKlGronwallSideConditionContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract"
      ]
      reusedBy := ["thm:forward-KL", "ASTIS-SALD-001 cycle 60"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle60_middle_route_audit"
      interface := "Cycle-60 middle audit: verify the post-cycle-59 continuous forward-KL route in source order, keep the theorem display and constants fixed, and select appendix.tex:168-228 sald.forward_kl.kl_derivative as the lower backend while LSI, DV, Gronwall, and EM interfaces remain separate obligations."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle60ForwardKlSkeletonMiddleContract",
        "SALD.cycle60ForwardKlSkeletonMiddleObligation",
        "SALD.cycle60ForwardKlSkeletonObligation",
        "SALD.cycle59MainSkeletonAnalyticMiddleObligation",
        "SALD.cycle55ForwardKlSkeletonMiddleObligation",
        "SALD.cycle55ForwardKlDerivativeMassLowerObligation",
        "SALD.cycle50ForwardKlDerivativeLowerObligation",
        "SALD.continuousForwardKlStatementContract",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDerivativeObligation",
        "sald.forward_kl.kl_derivative",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.forwardKlGronwallInstantiationContract",
        "SALD.forwardKlGronwallSideConditionContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract"
      ]
      reusedBy := ["thm:forward-KL", "cycle 60 lower derivative packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle60_five_backend_check"
      interface := "Explicit cycle-60 check of the five slow interfaces before lower work: endpoint-safe Gronwall, common-space DV with finite log-mgf, LSI/KL/FI density-test bridge, continuous Fokker-Planck/KL derivative, and EM interpolation Fokker-Planck for downstream discrete reuse."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.saldGronwallEndpointCalculusContract",
        "SALD.forwardKlGronwallSideConditionContract",
        "dvVariationalFormulaInterface saldDvVariationSource",
        "SALD.saldDvFiniteLogMgfContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract",
        "SALD.cycle59MainSkeletonAnalyticInterfaceObligation"
      ]
      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.forward_KL.cycle60_lower_packet.kl_derivative"
      interface := "Selected lower packet for cycle 60: return proof-producing work to sald.forward_kl.kl_derivative over appendix.tex:168-228, starting with mass conservation, KL differentiation, SALD Fokker-Planck substitution, target transport, boundary integration by parts, and inverse-schedule calculus."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle60ForwardKlSkeletonObligation",
        "SALD.cycle60ForwardKlSkeletonMiddleObligation",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDerivativeObligation",
        "SALD.forwardKlDensityBoundaryObligation",
        "SALD.forwardKlScheduleTimeChangeObligation",
        "SALD.cycle60ForwardKlDerivativeRawLowerObligation",
        "SALD.cycle55ForwardKlDerivativeMassLowerObligation",
        "SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar",
        "SALD.forwardKlMassConservationDropScalar",
        "SALD.forwardKlMassConservationFirstTermFisherScalar",
        "SALD.forwardKlDerivativeDvGronwallCoefficientOfKlFiVelocityScalingScalar",
        "sald.forward_kl.density_boundary_regular",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.kl_derivative"
      ]
      reusedBy := ["sald.forward_kl.kl_derivative", "thm:forward-KL", "cycle 60 lower handoff"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle60_derivative_raw_lower"
      interface := "Cycle-60 lower proof-producing scalar wrapper for appendix.tex:168-228: start from the raw KL derivative split with the mass term, drop that term by supplied mass conservation, and feed the existing first-term, target Young, LSI, slowed-velocity, and inverse-schedule pipeline to obtain the t-time pre-DV derivative inequality."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle60ForwardKlDerivativeRawLowerObligation",
        "SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar",
        "SALD.forwardKlMassConservationDropScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDerivativeObligation",
        "SALD.forwardKlDensityBoundaryObligation",
        "SALD.forwardKlScheduleTimeChangeObligation",
        "probability.lsi_to_kl_fi",
        "sald.forward_kl.density_boundary_regular",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.kl_derivative"
      ]
      reusedBy := ["sald.forward_kl.kl_derivative", "thm:forward-KL", "cycle 60 reviewer"]
      status := ProofStatus.obligation
    }
  ]

/-- Cycle-61 upper packet for the recovered discrete forward-KL skeleton.

Cycle 60 passed the continuous forward-KL reviewer/build gate.  This packet
returns to the interrupted cycle-56 discrete route and keeps the next work at
the theorem skeleton level: EM/Fokker--Planck, frozen defect, LSI, DV, and
Gronwall/accumulated-error interfaces are consumed explicitly without promoting
any slow analytic backend.
-/

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