AutoSamplingTheory.SALD.cycle62GuidedGeneralSkeletonDag

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 cycle62GuidedGeneralSkeletonDag : 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.guided_general.cycle62_global_phase_judgment
interface : String (explicit)
Text describing intended mathematical interface.
Upper judgment for cycle 62: cycle 61 passed and needs no recovery; Phase 1 is not ready for broad cited-theory backfill until the guided residual and continuous general moving-target route is synchronized; the selected lower packet is the appendix.tex:619-951 guided/general route audit narrowing to sald.general_moving_target.kl_derivative.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetSource — 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.cycle62GuidedGeneralSkeletonUpperPacket
2. SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation
3. SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation
4. SALD.cycle57GuidedGeneralSkeletonMiddleObligation
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. prop:guided_path_residual
2. thm:general-moving-target-SALD
3. ASTIS-SALD-001 cycle 62
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.guided_general.cycle62_five_backend_check
interface : String (explicit)
Text describing intended mathematical interface.
Explicit cycle-62 check before middle/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 endpoint/conditional-law Fokker-Planck are all named source-cited or obligation interfaces.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetSource — 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.generalMovingTargetGronwallInstantiationContract
3. SALD.generalMovingTargetGronwallSideConditionContract
4. dvVariationalFormulaInterface saldDvVariationSource
5. SALD.saldDvFiniteLogMgfContract
6. SALD.generalMovingTargetDvFiniteLogMgfWitnessContract
7. SALD.saldLsiKlFiDensityTestContract
8. SALD.forwardKlDerivativeSideConditionContract
9. SALD.generalMovingTargetDerivativeCandidateContract
10. SALD.discreteForwardKlEmInterpolationSideConditionContract
11. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
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.guided_general.cycle62_upper_route
interface : String (explicit)
Text describing intended mathematical interface.
Upper route for appendix.tex:619-951 after cycle 61: route guided residual through normalizer/centered identity, route continuous general SALD through derivative, LSI, residual DV, Gronwall, and pure-contraction interfaces, and keep unified reuse as the source specialization.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetSource — 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.cycle62GuidedGeneralSkeletonObligation
2. SALD.guidedResidualIdentityContract
3. sald.guided_path_residual.identity
4. SALD.generalMovingTargetStatementContract
5. SALD.generalMovingTargetDerivativeCandidateContract
6. sald.general_moving_target.kl_derivative
7. SALD.saldLsiKlFiDensityTestContract
8. SALD.generalMovingTargetDvFiniteLogMgfWitnessContract
9. SALD.generalMovingTargetGronwallSideConditionContract
10. sald.general_moving_target.pure_contraction
11. SALD.unifiedForwardKlSpecializationContract
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. prop:guided_path_residual
2. thm:general-moving-target-SALD
3. thm:unified-forward-KL
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.guided_general.cycle62_middle_route_audit
interface : String (explicit)
Text describing intended mathematical interface.
Middle source-to-Lean audit for cycle 62: verify appendix.tex:619-951 in paper order after the upper wrapper, keep guided residual and continuous general theorem statements fixed, and route proof-producing lower work to sald.general_moving_target.kl_derivative while guided residual, LSI, residual DV, Gronwall, pure contraction, unified specialization, and EM reuse remain separate obligations.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetSource — 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.cycle62GuidedGeneralSkeletonMiddleContract
2. SALD.cycle62GuidedGeneralSkeletonMiddleObligation
3. SALD.cycle62GuidedGeneralSkeletonObligation
4. SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation
5. SALD.cycle57GuidedGeneralSkeletonMiddleObligation
6. SALD.guidedResidualIdentityContract
7. SALD.generalMovingTargetStatementContract
8. SALD.generalMovingTargetDerivativeCandidateContract
9. SALD.generalMovingTargetDerivativeObligation
10. sald.general_moving_target.kl_derivative
11. SALD.generalMovingTargetDvFiniteLogMgfWitnessContract
12. SALD.generalMovingTargetGronwallSideConditionContract
13. SALD.saldLsiKlFiDensityTestContract
14. SALD.saldGronwallEndpointCalculusContract
15. SALD.unifiedForwardKlSpecializationContract
16. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. prop:guided_path_residual
2. thm:general-moving-target-SALD
3. cycle62 lower derivative 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.guided_general.cycle62_lower_packet.route_audit
interface : String (explicit)
Text describing intended mathematical interface.
Selected lower packet for cycle 62 after the middle audit: narrow proof-producing work to the continuous general Fokker-Planck/KL derivative backend over appendix.tex:765-884.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDerivativeSource — 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.cycle62GuidedGeneralSkeletonObligation
2. SALD.cycle62GuidedGeneralSkeletonMiddleObligation
3. SALD.cycle57GuidedGeneralDerivativeSplitLowerObligation
4. SALD.generalMovingTargetDerivativeCandidateContract
5. SALD.generalMovingTargetDerivativeObligation
6. sald.general_moving_target.kl_derivative
7. SALD.generalMovingTargetKlDerivativeResidualSplitScalar
8. SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar
9. SALD.saldLsiKlFiDensityTestContract
10. sald.forward_kl.schedule_time_change
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target.kl_derivative
2. thm:general-moving-target-SALD
3. thm:unified-forward-KL
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.general_moving_target.cycle62_scaled_residual_lower
interface : String (explicit)
Text describing intended mathematical interface.
Lower proof-producing scalar core for appendix.tex:813-835: preserve the tilde-v dot{t}(s) scaling and rewrite c_t-v_t into the source residual sign -dot{t}(s)*m_t before the Young step.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDerivativeSource — 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.cycle62GuidedGeneralScaledResidualLowerObligation
2. SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar
3. SALD.generalMovingTargetKlDerivativeResidualSplitScalar
4. SALD.generalMovingTargetDerivativeCandidateContract
5. SALD.generalMovingTargetDerivativeObligation
6. sald.general_moving_target.kl_derivative
7. TransportVelocityContract
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target.kl_derivative
2. thm:general-moving-target-SALD
3. thm:unified-forward-KL
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 cycle62GuidedGeneralSkeletonDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.guided_general.cycle62_global_phase_judgment"
      interface := "Upper judgment for cycle 62: cycle 61 passed and needs no recovery; Phase 1 is not ready for broad cited-theory backfill until the guided residual and continuous general moving-target route is synchronized; the selected lower packet is the appendix.tex:619-951 guided/general route audit narrowing to sald.general_moving_target.kl_derivative."
      source := saldGeneralMovingTargetSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle62GuidedGeneralSkeletonUpperPacket",
        "SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation",
        "SALD.cycle57GuidedGeneralSkeletonMiddleObligation"
      ]
      reusedBy := ["prop:guided_path_residual", "thm:general-moving-target-SALD", "ASTIS-SALD-001 cycle 62"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.guided_general.cycle62_five_backend_check"
      interface := "Explicit cycle-62 check before middle/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 endpoint/conditional-law Fokker-Planck are all named source-cited or obligation interfaces."
      source := saldGeneralMovingTargetSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.saldGronwallEndpointCalculusContract",
        "SALD.generalMovingTargetGronwallInstantiationContract",
        "SALD.generalMovingTargetGronwallSideConditionContract",
        "dvVariationalFormulaInterface saldDvVariationSource",
        "SALD.saldDvFiniteLogMgfContract",
        "SALD.generalMovingTargetDvFiniteLogMgfWitnessContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.generalMovingTargetDerivativeCandidateContract",
        "SALD.discreteForwardKlEmInterpolationSideConditionContract",
        "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract"
      ]
      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.guided_general.cycle62_upper_route"
      interface := "Upper route for appendix.tex:619-951 after cycle 61: route guided residual through normalizer/centered identity, route continuous general SALD through derivative, LSI, residual DV, Gronwall, and pure-contraction interfaces, and keep unified reuse as the source specialization."
      source := saldGeneralMovingTargetSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle62GuidedGeneralSkeletonObligation",
        "SALD.guidedResidualIdentityContract",
        "sald.guided_path_residual.identity",
        "SALD.generalMovingTargetStatementContract",
        "SALD.generalMovingTargetDerivativeCandidateContract",
        "sald.general_moving_target.kl_derivative",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.generalMovingTargetDvFiniteLogMgfWitnessContract",
        "SALD.generalMovingTargetGronwallSideConditionContract",
        "sald.general_moving_target.pure_contraction",
        "SALD.unifiedForwardKlSpecializationContract"
      ]
      reusedBy := ["prop:guided_path_residual", "thm:general-moving-target-SALD", "thm:unified-forward-KL"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.guided_general.cycle62_middle_route_audit"
      interface := "Middle source-to-Lean audit for cycle 62: verify appendix.tex:619-951 in paper order after the upper wrapper, keep guided residual and continuous general theorem statements fixed, and route proof-producing lower work to sald.general_moving_target.kl_derivative while guided residual, LSI, residual DV, Gronwall, pure contraction, unified specialization, and EM reuse remain separate obligations."
      source := saldGeneralMovingTargetSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle62GuidedGeneralSkeletonMiddleContract",
        "SALD.cycle62GuidedGeneralSkeletonMiddleObligation",
        "SALD.cycle62GuidedGeneralSkeletonObligation",
        "SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation",
        "SALD.cycle57GuidedGeneralSkeletonMiddleObligation",
        "SALD.guidedResidualIdentityContract",
        "SALD.generalMovingTargetStatementContract",
        "SALD.generalMovingTargetDerivativeCandidateContract",
        "SALD.generalMovingTargetDerivativeObligation",
        "sald.general_moving_target.kl_derivative",
        "SALD.generalMovingTargetDvFiniteLogMgfWitnessContract",
        "SALD.generalMovingTargetGronwallSideConditionContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.saldGronwallEndpointCalculusContract",
        "SALD.unifiedForwardKlSpecializationContract",
        "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract"
      ]
      reusedBy := ["prop:guided_path_residual", "thm:general-moving-target-SALD", "cycle62 lower derivative packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.guided_general.cycle62_lower_packet.route_audit"
      interface := "Selected lower packet for cycle 62 after the middle audit: narrow proof-producing work to the continuous general Fokker-Planck/KL derivative backend over appendix.tex:765-884."
      source := saldGeneralMovingTargetDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle62GuidedGeneralSkeletonObligation",
        "SALD.cycle62GuidedGeneralSkeletonMiddleObligation",
        "SALD.cycle57GuidedGeneralDerivativeSplitLowerObligation",
        "SALD.generalMovingTargetDerivativeCandidateContract",
        "SALD.generalMovingTargetDerivativeObligation",
        "sald.general_moving_target.kl_derivative",
        "SALD.generalMovingTargetKlDerivativeResidualSplitScalar",
        "SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar",
        "SALD.saldLsiKlFiDensityTestContract",
        "sald.forward_kl.schedule_time_change"
      ]
      reusedBy := ["sald.general_moving_target.kl_derivative", "thm:general-moving-target-SALD", "thm:unified-forward-KL"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.general_moving_target.cycle62_scaled_residual_lower"
      interface := "Lower proof-producing scalar core for appendix.tex:813-835: preserve the tilde-v dot{t}(s) scaling and rewrite c_t-v_t into the source residual sign -dot{t}(s)*m_t before the Young step."
      source := saldGeneralMovingTargetDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle62GuidedGeneralScaledResidualLowerObligation",
        "SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar",
        "SALD.generalMovingTargetKlDerivativeResidualSplitScalar",
        "SALD.generalMovingTargetDerivativeCandidateContract",
        "SALD.generalMovingTargetDerivativeObligation",
        "sald.general_moving_target.kl_derivative",
        "TransportVelocityContract"
      ]
      reusedBy := ["sald.general_moving_target.kl_derivative", "thm:general-moving-target-SALD", "thm:unified-forward-KL"]
      status := ProofStatus.obligation
    }
  ]

/-- Cycle-63 upper packet for the unified and discrete general theorem route.

This is workflow data only.  It records the required upper phase judgment,
rechecks the five slow analytic interfaces before assigning follow-up work,
wires `thm:unified-forward-KL` and
`thm:general-moving-target-SALD-discrete` through the accepted continuous and
general skeletons, and permits exactly one narrow measure-theory backfill below
the EM endpoint-law interface.
-/

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