AutoSamplingTheory.SALD.cycle66DiscreteForwardKlSkeletonDag

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 cycle66DiscreteForwardKlSkeletonDag : 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_discrete.cycle66_global_phase_judgment
interface : String (explicit)
Text describing intended mathematical interface.
Upper judgment for cycle 66: cycle 65 passed and needs no recovery; Phase 1 supports this narrow discrete forward-KL route audit only; the largest remaining discrete proof risk is sald.discrete_forward_kl.accumulated_error_bridge over appendix.tex:557-592 and main_body.tex:309-323.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteProofSource — 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.cycle66DiscreteForwardKlSkeletonUpperPacket
2. SALD.cycle65ForwardKlSkeletonMiddleObligation
3. SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation
4. SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. ASTIS-SALD-001 cycle 66
2. thm:forward-KL-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.forward_KL_discrete.cycle66_five_backend_check
interface : String (explicit)
Text describing intended mathematical interface.
Explicit cycle-66 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 endpoint/conditional-law Fokker-Planck.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteProofSource — 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.discreteForwardKlGronwallInstantiationContract
3. dvVariationalFormulaInterface saldDvVariationSource
4. SALD.saldDvFiniteLogMgfContract
5. SALD.discreteForwardKlDvFiniteLogMgfWitnessContract
6. SALD.saldLsiKlFiDensityTestContract
7. SALD.forwardKlDerivativeSideConditionContract
8. SALD.cycle65ForwardKlSkeletonMiddleObligation
9. SALD.discreteForwardKlEmInterpolationSideConditionContract
10. sald.discrete_forward_kl.em_interpolation_fp
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.forward_KL_discrete.cycle66_discrete_route
interface : String (explicit)
Text describing intended mathematical interface.
Post-cycle-65 upper route: consume the five-backend analytic ledger and existing cycle-51/56/61 discrete route data, then wire main_body.tex:299-323 and appendix.tex:260-592 through EM conditional-FP, KL derivative/frozen-defect/LSI, DV velocity, time-changed Gronwall, and accumulated-error display interfaces without changing the theorem display.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteProofSource — 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.cycle66DiscreteForwardKlSkeletonUpperPacket
2. SALD.cycle66DiscreteForwardKlSkeletonObligation
3. SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation
4. SALD.cycle56DiscreteForwardKlGronwallLowerObligation
5. SALD.discreteForwardKlStatementContract
6. SALD.discreteForwardKlEmInterpolationSideConditionContract
7. SALD.discreteForwardKlDerivativeCandidateContract
8. SALD.frozenDeltaCrossLipSaldContract
9. SALD.saldLsiKlFiDensityTestContract
10. SALD.discreteForwardKlDvFiniteLogMgfWitnessContract
11. SALD.discreteForwardKlGronwallInstantiationContract
12. SALD.discreteForwardKlAccumulatedErrorBridgeContract
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL-discrete
2. cycle 66 middle route audit
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.forward_KL_discrete.cycle66_middle_route_audit
interface : String (explicit)
Text describing intended mathematical interface.
Middle audit for cycle 66: verify the post-cycle-65 discrete route in paper order, keep the EM/Fokker-Planck, derivative/LSI, DV, and Gronwall interfaces explicit, and keep lower work on the accumulated-error bridge to the main-body linear-slowdown display.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteProofSource — 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.cycle66DiscreteForwardKlSkeletonMiddleContract
2. SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation
3. SALD.cycle66DiscreteForwardKlSkeletonObligation
4. SALD.cycle65ForwardKlSkeletonMiddleObligation
5. SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation
6. SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation
7. SALD.cycle56DiscreteForwardKlGronwallLowerObligation
8. SALD.discreteForwardKlStatementContract
9. SALD.discreteForwardKlEmInterpolationSideConditionContract
10. sald.discrete_forward_kl.em_interpolation_fp
11. SALD.discreteForwardKlDerivativeCandidateContract
12. sald.discrete_forward_kl.kl_derivative
13. SALD.frozenDeltaCrossLipSaldContract
14. SALD.saldLsiKlFiDensityTestContract
15. SALD.discreteForwardKlDvFiniteLogMgfWitnessContract
16. sald.discrete_forward_kl.dv_velocity_bound
17. SALD.discreteForwardKlGronwallInstantiationContract
18. SALD.discreteForwardKlAccumulatedErrorBridgeContract
19. sald.discrete_forward_kl.accumulated_error_bridge
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL-discrete
2. cycle 66 lower accumulated-error 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.forward_KL_discrete.cycle66_lower_packet.accumulated_error
interface : String (explicit)
Text describing intended mathematical interface.
Selected lower packet for cycle 66: keep proof-producing work on sald.discrete_forward_kl.accumulated_error_bridge over appendix.tex:557-592 and main_body.tex:309-323, using the supplied cycle-56 pointwise Gronwall input, the cycle-61 residual-display wrapper, and the cycle-66 final main-display scalar wrapper.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteAccumulatedErrorSource — 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.cycle66DiscreteForwardKlSkeletonObligation
2. SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation
3. SALD.cycle66DiscreteForwardKlAccumulatedDisplayLowerObligation
4. SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation
5. SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar
6. SALD.discreteForwardKlPointwiseGronwallInputOfPostDvTimeChanged
7. SALD.discreteForwardKlGronwallInstantiationContract
8. SALD.discreteForwardKlAccumulatedErrorBridgeContract
9. SALD.discreteForwardKlAccumulatedErrorBridgeObligation
10. SALD.discreteForwardKlGronwallCoeffIntervalIntegrable
11. SALD.discreteForwardKlGronwallCoeffIntegralSubSub
12. SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces
13. SALD.discreteForwardKlResidualExponentBoundScalar
14. SALD.discreteForwardKlResidualExpBoundScalar
15. SALD.discreteForwardKlAlphaComplexityCollectionScalar
16. SALD.discreteForwardKlDeltaAccumulationScalar
17. SALD.discreteForwardKlAccumulatedErrorCollectionScalar
18. SALD.discreteForwardKlResidualIntegralDisplayBoundScalar
19. SALD.discreteForwardKlMainDisplayBoundScalar
20. sald.discrete_forward_kl.gronwall_accumulation
21. sald.discrete_forward_kl.linear_slowdown_specialization
22. sald.discrete_forward_kl.residual_exponent_bound
23. sald.discrete_forward_kl.accumulated_error_bridge
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.discrete_forward_kl.accumulated_error_bridge
2. thm:forward-KL-discrete
3. cycle 66 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 cycle66DiscreteForwardKlSkeletonDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle66_global_phase_judgment"
      interface := "Upper judgment for cycle 66: cycle 65 passed and needs no recovery; Phase 1 supports this narrow discrete forward-KL route audit only; the largest remaining discrete proof risk is sald.discrete_forward_kl.accumulated_error_bridge over appendix.tex:557-592 and main_body.tex:309-323."
      source := saldForwardKlDiscreteProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle66DiscreteForwardKlSkeletonUpperPacket",
        "SALD.cycle65ForwardKlSkeletonMiddleObligation",
        "SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation"
      ]
      reusedBy := ["ASTIS-SALD-001 cycle 66", "thm:forward-KL-discrete"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle66_five_backend_check"
      interface := "Explicit cycle-66 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 endpoint/conditional-law Fokker-Planck."
      source := saldForwardKlDiscreteProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.saldGronwallEndpointCalculusContract",
        "SALD.discreteForwardKlGronwallInstantiationContract",
        "dvVariationalFormulaInterface saldDvVariationSource",
        "SALD.saldDvFiniteLogMgfContract",
        "SALD.discreteForwardKlDvFiniteLogMgfWitnessContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.cycle65ForwardKlSkeletonMiddleObligation",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      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_discrete.cycle66_discrete_route"
      interface := "Post-cycle-65 upper route: consume the five-backend analytic ledger and existing cycle-51/56/61 discrete route data, then wire main_body.tex:299-323 and appendix.tex:260-592 through EM conditional-FP, KL derivative/frozen-defect/LSI, DV velocity, time-changed Gronwall, and accumulated-error display interfaces without changing the theorem display."
      source := saldForwardKlDiscreteProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle66DiscreteForwardKlSkeletonUpperPacket",
        "SALD.cycle66DiscreteForwardKlSkeletonObligation",
        "SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle56DiscreteForwardKlGronwallLowerObligation",
        "SALD.discreteForwardKlStatementContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract",
        "SALD.discreteForwardKlDerivativeCandidateContract",
        "SALD.frozenDeltaCrossLipSaldContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.discreteForwardKlDvFiniteLogMgfWitnessContract",
        "SALD.discreteForwardKlGronwallInstantiationContract",
        "SALD.discreteForwardKlAccumulatedErrorBridgeContract"
      ]
      reusedBy := ["thm:forward-KL-discrete", "cycle 66 middle route audit"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle66_middle_route_audit"
      interface := "Middle audit for cycle 66: verify the post-cycle-65 discrete route in paper order, keep the EM/Fokker-Planck, derivative/LSI, DV, and Gronwall interfaces explicit, and keep lower work on the accumulated-error bridge to the main-body linear-slowdown display."
      source := saldForwardKlDiscreteProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle66DiscreteForwardKlSkeletonMiddleContract",
        "SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle66DiscreteForwardKlSkeletonObligation",
        "SALD.cycle65ForwardKlSkeletonMiddleObligation",
        "SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation",
        "SALD.cycle56DiscreteForwardKlGronwallLowerObligation",
        "SALD.discreteForwardKlStatementContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "SALD.discreteForwardKlDerivativeCandidateContract",
        "sald.discrete_forward_kl.kl_derivative",
        "SALD.frozenDeltaCrossLipSaldContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.discreteForwardKlDvFiniteLogMgfWitnessContract",
        "sald.discrete_forward_kl.dv_velocity_bound",
        "SALD.discreteForwardKlGronwallInstantiationContract",
        "SALD.discreteForwardKlAccumulatedErrorBridgeContract",
        "sald.discrete_forward_kl.accumulated_error_bridge"
      ]
      reusedBy := ["thm:forward-KL-discrete", "cycle 66 lower accumulated-error packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle66_lower_packet.accumulated_error"
      interface := "Selected lower packet for cycle 66: keep proof-producing work on sald.discrete_forward_kl.accumulated_error_bridge over appendix.tex:557-592 and main_body.tex:309-323, using the supplied cycle-56 pointwise Gronwall input, the cycle-61 residual-display wrapper, and the cycle-66 final main-display scalar wrapper."
      source := saldForwardKlDiscreteAccumulatedErrorSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle66DiscreteForwardKlSkeletonObligation",
        "SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle66DiscreteForwardKlAccumulatedDisplayLowerObligation",
        "SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation",
        "SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar",
        "SALD.discreteForwardKlPointwiseGronwallInputOfPostDvTimeChanged",
        "SALD.discreteForwardKlGronwallInstantiationContract",
        "SALD.discreteForwardKlAccumulatedErrorBridgeContract",
        "SALD.discreteForwardKlAccumulatedErrorBridgeObligation",
        "SALD.discreteForwardKlGronwallCoeffIntervalIntegrable",
        "SALD.discreteForwardKlGronwallCoeffIntegralSubSub",
        "SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces",
        "SALD.discreteForwardKlResidualExponentBoundScalar",
        "SALD.discreteForwardKlResidualExpBoundScalar",
        "SALD.discreteForwardKlAlphaComplexityCollectionScalar",
        "SALD.discreteForwardKlDeltaAccumulationScalar",
        "SALD.discreteForwardKlAccumulatedErrorCollectionScalar",
        "SALD.discreteForwardKlResidualIntegralDisplayBoundScalar",
        "SALD.discreteForwardKlMainDisplayBoundScalar",
        "sald.discrete_forward_kl.gronwall_accumulation",
        "sald.discrete_forward_kl.linear_slowdown_specialization",
        "sald.discrete_forward_kl.residual_exponent_bound",
        "sald.discrete_forward_kl.accumulated_error_bridge"
      ]
      reusedBy := ["sald.discrete_forward_kl.accumulated_error_bridge", "thm:forward-KL-discrete", "cycle 66 lower handoff"]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 67: guided residual and continuous general moving-target route -/

/-- Cycle-67 upper packet for returning to the guided residual and continuous
general moving-target theorem after the accepted cycle-66 discrete route.

This is a theorem-skeleton route packet only.  It rechecks the five slow
interfaces, wires `appendix.tex:619-951` through the named guided/general
interfaces, and selects one lower packet for the residual-to-Gronwall bridge
without changing any source theorem statement or analytic backend status.
-/

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