AutoSamplingTheory.SALD.cycle201GeneralMovingTargetDiscreteEmInterpolationSelectedTestLaplacianContinuityLower2Dag

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.

def cycle201GeneralMovingTargetDiscreteEmInterpolationSelectedTestLaplacianContinuityLower2Dag :
    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.cycle201.lower_2_packet.selected_test_laplacian_continuity_source_gap

   interface : String (explicit)

   Text describing intended mathematical interface.

   Typed source-cited boundary: hSelectedTestLaplacianMeasurable is not closed directly; it is reduced to the smaller source-facing field hSelectedTestLaplacianContinuous. The source audit did not find that field in the original SALD assumptions, so the weak-FP Laplacian measurability backend remains blocked exactly there.

   source : AutoSamplingTheory.SourceAnchor (explicit)

   Source pointer.

   AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpSource — 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.cycle201GeneralMovingTargetDiscreteEmInterpolationSelectedTestLaplacianContinuityLower2Obligation
   2. SALD.generalMovingTargetDiscreteSelectedTestLaplacianMeasurableOfContinuous
   3. SALD.generalMovingTargetDiscreteSourceLaplacianFieldMeasOfSelectedTestLaplacianMeasurable
   4. hSelectedTestLaplacianContinuous
   5. hSelectedTestLaplacianMeasurable
   6. hsourceLaplacianFieldMeas
   7. appendix.tex:724-727
   8. appendix.tex:1028-1070
   9. appendix.tex:1313-1316
   10. appendix.tex:983-996
   11. appendix.tex:1379-1387
   12. source_contract_gap_missing_selected_test_laplacian_continuity

   reusedBy : List String (explicit)

   Declared consumers as strings, default empty.

   Ordered data items

   1. hsourceLaplacianFieldMeas
   2. sald.general_moving_target_discrete.em_interpolation_fp
   3. sald.general_moving_target_discrete.kl_derivative
   4. divergence/FI/IBP handoff

   status : AutoSamplingTheory.ProofStatus (explicit)

   Recorded workflow status, default planned.

   AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def cycle201GeneralMovingTargetDiscreteEmInterpolationSelectedTestLaplacianContinuityLower2Dag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle201.lower_2_packet.selected_test_laplacian_continuity_source_gap"
      interface := "Typed source-cited boundary: hSelectedTestLaplacianMeasurable is not closed directly; it is reduced to the smaller source-facing field hSelectedTestLaplacianContinuous. The source audit did not find that field in the original SALD assumptions, so the weak-FP Laplacian measurability backend remains blocked exactly there."
      source := saldGeneralMovingTargetDiscreteWeakFpSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle201GeneralMovingTargetDiscreteEmInterpolationSelectedTestLaplacianContinuityLower2Obligation",
        "SALD.generalMovingTargetDiscreteSelectedTestLaplacianMeasurableOfContinuous",
        "SALD.generalMovingTargetDiscreteSourceLaplacianFieldMeasOfSelectedTestLaplacianMeasurable",
        "hSelectedTestLaplacianContinuous",
        "hSelectedTestLaplacianMeasurable",
        "hsourceLaplacianFieldMeas",
        "appendix.tex:724-727",
        "appendix.tex:1028-1070",
        "appendix.tex:1313-1316",
        "appendix.tex:983-996",
        "appendix.tex:1379-1387",
        "source_contract_gap_missing_selected_test_laplacian_continuity"
      ]
      reusedBy := [
        "hsourceLaplacianFieldMeas",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.general_moving_target_discrete.kl_derivative",
        "divergence/FI/IBP handoff"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 202 lower_2: selected endpoint coordinate-line source gap -/

/-- Cycle-202 lower_2 packet for the selected endpoint coordinate-line field.

The cycle-190 local bridge already reduces the selected-increment coordinate
line and raw source Taylor integrand leaves to endpoint naming plus the
endpoint coordinate-line identity.  In the current Lean interface,
`sourceSelectedEndpoint` is still an abstract source-facing function rather
than a reducible definition, so lower_2 records the smaller source contract
instead of adding another wrapper for the same equality.
-/