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

AutoSamplingTheory.SALD.cycle65ForwardKlSkeletonDag

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 cycle65ForwardKlSkeletonDag : 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.cycle65_global_phase_judgment
    interface : String (explicit)

    Text describing intended mathematical interface.

    Upper judgment for cycle 65: cycle 64 passed and needs no recovery; Phase 1 supports this narrow continuous forward-KL route audit only; the largest remaining continuous proof risk is sald.forward_kl.kl_derivative over appendix.tex:168-228.
    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.cycle65ForwardKlSkeletonUpperPacket
    2. SALD.cycle64MainSkeletonAnalyticMiddleObligation
    3. SALD.cycle64GeneralMovingTargetDiscreteConditionalDriftLowerObligation
    reusedBy : List String (explicit)

    Declared consumers as strings, default empty.

    Ordered data items

    1. ASTIS-SALD-001 cycle 65
    2. thm:forward-KL
    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.cycle65_five_backend_check
    interface : String (explicit)

    Text describing intended mathematical interface.

    Explicit cycle-65 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.forwardKlDvFiniteLogMgfWitnessContract
    6. SALD.saldLsiKlFiDensityTestContract
    7. SALD.forwardKlDerivativeSideConditionContract
    8. SALD.discreteForwardKlEmInterpolationSideConditionContract
    9. SALD.cycle64MainSkeletonAnalyticInterfaceObligation
    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
  3. id : String (explicit)

    Stable plan-node identifier.

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

    Text describing intended mathematical interface.

    Post-cycle-64 upper route: consume the five-backend analytic ledger and existing continuous forward-KL route data, 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.cycle65ForwardKlSkeletonUpperPacket
    2. SALD.cycle65ForwardKlSkeletonObligation
    3. SALD.cycle65ForwardKlSkeletonMiddleContract
    4. SALD.cycle65ForwardKlSkeletonMiddleObligation
    5. SALD.cycle64MainSkeletonAnalyticInterfaceObligation
    6. SALD.cycle64MainSkeletonAnalyticMiddleObligation
    7. SALD.cycle60ForwardKlSkeletonObligation
    8. SALD.cycle60ForwardKlSkeletonMiddleObligation
    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. cycle 65 middle route audit
    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.cycle65_middle_route_audit
    interface : String (explicit)

    Text describing intended mathematical interface.

    Cycle-65 middle audit: verify the post-cycle-64 continuous forward-KL route in source order, keep main_body.tex:238-247 and all 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.cycle65ForwardKlSkeletonMiddleContract
    2. SALD.cycle65ForwardKlSkeletonMiddleObligation
    3. SALD.cycle65ForwardKlSkeletonObligation
    4. SALD.cycle64MainSkeletonAnalyticMiddleObligation
    5. SALD.cycle60ForwardKlSkeletonMiddleObligation
    6. SALD.cycle60ForwardKlDerivativeRawLowerObligation
    7. SALD.continuousForwardKlStatementContract
    8. SALD.forwardKlDerivativeCandidateContract
    9. SALD.forwardKlDerivativeSideConditionContract
    10. SALD.forwardKlDerivativeObligation
    11. sald.forward_kl.kl_derivative
    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. cycle 65 lower derivative packet
    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.cycle65_lower_packet.kl_derivative
    interface : String (explicit)

    Text describing intended mathematical interface.

    Selected lower packet for cycle 65: keep proof-producing work on sald.forward_kl.kl_derivative over appendix.tex:168-228, with the source split into mass/KL differentiation and -FI, target-velocity Young, then inverse-schedule square scaling.
    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.cycle65ForwardKlSkeletonObligation
    2. SALD.cycle65ForwardKlSkeletonMiddleObligation
    3. SALD.cycle60ForwardKlDerivativeRawLowerObligation
    4. SALD.forwardKlDerivativeCandidateContract
    5. SALD.forwardKlDerivativeSideConditionContract
    6. SALD.forwardKlDerivativeObligation
    7. SALD.forwardKlDensityBoundaryObligation
    8. SALD.forwardKlScheduleTimeChangeObligation
    9. SALD.cycle65ForwardKlDerivativePointwiseLowerObligation
    10. SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling
    11. SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar
    12. SALD.forwardKlMassConservationDropScalar
    13. SALD.forwardKlMassConservationFirstTermFisherScalar
    14. SALD.forwardKlDerivativeDvGronwallCoefficientOfKlFiVelocityScalingScalar
    15. sald.forward_kl.density_boundary_regular
    16. sald.forward_kl.schedule_time_change
    17. 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 65 lower handoff
    status : AutoSamplingTheory.ProofStatus (explicit)

    Recorded workflow status, default planned.

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

    Stable plan-node identifier.

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

    Text describing intended mathematical interface.

    Cycle-65 lower proof-producing wrapper for appendix.tex:168-228: lift the compiled raw-derivative scalar handoff to the pointwise t-indexed pre-DV inequality used by thm:forward-KL before DV and Gronwall.
    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.cycle65ForwardKlDerivativePointwiseLowerObligation
    2. SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling
    3. SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar
    4. SALD.forwardKlDerivativeCandidateContract
    5. SALD.forwardKlDerivativeSideConditionContract
    6. SALD.forwardKlDerivativeObligation
    7. SALD.forwardKlDensityBoundaryObligation
    8. SALD.forwardKlScheduleTimeChangeObligation
    9. SALD.saldLsiKlFiDensityTestContract
    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 65 lower handoff
    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 cycle65ForwardKlSkeletonDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.forward_KL.cycle65_global_phase_judgment"
      interface := "Upper judgment for cycle 65: cycle 64 passed and needs no recovery; Phase 1 supports this narrow continuous forward-KL route audit only; the largest remaining continuous proof risk is sald.forward_kl.kl_derivative over appendix.tex:168-228."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle65ForwardKlSkeletonUpperPacket",
        "SALD.cycle64MainSkeletonAnalyticMiddleObligation",
        "SALD.cycle64GeneralMovingTargetDiscreteConditionalDriftLowerObligation"
      ]
      reusedBy := ["ASTIS-SALD-001 cycle 65", "thm:forward-KL"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle65_five_backend_check"
      interface := "Explicit cycle-65 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.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract",
        "SALD.cycle64MainSkeletonAnalyticInterfaceObligation"
      ]
      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.cycle65_continuous_route"
      interface := "Post-cycle-64 upper route: consume the five-backend analytic ledger and existing continuous forward-KL route data, 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.cycle65ForwardKlSkeletonUpperPacket",
        "SALD.cycle65ForwardKlSkeletonObligation",
        "SALD.cycle65ForwardKlSkeletonMiddleContract",
        "SALD.cycle65ForwardKlSkeletonMiddleObligation",
        "SALD.cycle64MainSkeletonAnalyticInterfaceObligation",
        "SALD.cycle64MainSkeletonAnalyticMiddleObligation",
        "SALD.cycle60ForwardKlSkeletonObligation",
        "SALD.cycle60ForwardKlSkeletonMiddleObligation",
        "SALD.continuousForwardKlStatementContract",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.forwardKlGronwallInstantiationContract",
        "SALD.forwardKlGronwallSideConditionContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract"
      ]
      reusedBy := ["thm:forward-KL", "cycle 65 middle route audit"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle65_middle_route_audit"
      interface := "Cycle-65 middle audit: verify the post-cycle-64 continuous forward-KL route in source order, keep main_body.tex:238-247 and all 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.cycle65ForwardKlSkeletonMiddleContract",
        "SALD.cycle65ForwardKlSkeletonMiddleObligation",
        "SALD.cycle65ForwardKlSkeletonObligation",
        "SALD.cycle64MainSkeletonAnalyticMiddleObligation",
        "SALD.cycle60ForwardKlSkeletonMiddleObligation",
        "SALD.cycle60ForwardKlDerivativeRawLowerObligation",
        "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 65 lower derivative packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle65_lower_packet.kl_derivative"
      interface := "Selected lower packet for cycle 65: keep proof-producing work on sald.forward_kl.kl_derivative over appendix.tex:168-228, with the source split into mass/KL differentiation and -FI, target-velocity Young, then inverse-schedule square scaling."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle65ForwardKlSkeletonObligation",
        "SALD.cycle65ForwardKlSkeletonMiddleObligation",
        "SALD.cycle60ForwardKlDerivativeRawLowerObligation",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDerivativeObligation",
        "SALD.forwardKlDensityBoundaryObligation",
        "SALD.forwardKlScheduleTimeChangeObligation",
        "SALD.cycle65ForwardKlDerivativePointwiseLowerObligation",
        "SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling",
        "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 65 lower handoff"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle65_derivative_pointwise_lower"
      interface := "Cycle-65 lower proof-producing wrapper for appendix.tex:168-228: lift the compiled raw-derivative scalar handoff to the pointwise t-indexed pre-DV inequality used by thm:forward-KL before DV and Gronwall."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle65ForwardKlDerivativePointwiseLowerObligation",
        "SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling",
        "SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDerivativeObligation",
        "SALD.forwardKlDensityBoundaryObligation",
        "SALD.forwardKlScheduleTimeChangeObligation",
        "SALD.saldLsiKlFiDensityTestContract",
        "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 65 lower handoff"]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 66: discrete forward-KL post-cycle65 route -/

/-- Cycle-66 upper packet for the discrete forward-KL skeleton after the
accepted cycle-65 continuous route.

This is upper-route data only.  It returns the main skeleton sprint to
`thm:forward-KL-discrete`, checks that the five slow analytic interfaces are
still explicit, and assigns the next lower packet to the Gronwall/output
stitching and accumulated-error bridge without changing the paper statement,
constants, labels, or proof statuses.
-/

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