AutoSamplingTheory.SALD.cycle204GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSourceTaylorIntegrandSelectedIncrementLower2Dag

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 cycle204GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSourceTaylorIntegrandSelectedIncrementLower2Dag :
    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.cycle204.lower_2_packet.source_taylor_integrand_selected_increment_source_gap

   interface : String (explicit)

   Text describing intended mathematical interface.

   Typed source-cited boundary: hSourceTaylorIntegrandSelectedIncrementDef is not closed by a same-shape wrapper; the existing cycle-189/190 bridges already show that this field is the smaller source contract needed before endpoint-coordinate and endpoint-difference fields can feed hSourceTaylorIntegrandRawDef.

   source : AutoSamplingTheory.SourceAnchor (explicit)

   Source pointer.

   AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteEmSource — 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.cycle204GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSourceTaylorIntegrandSelectedIncrementLower2Obligation
   2. SALD.selectedWeakTestSourceTaylorIntegrandRawDefOfSelectedIncrementAndLineDef
   3. SALD.selectedWeakTestSourceTaylorIntegrandRawDefOfSelectedIncrementEndpointAndLineDef
   4. SALD.selectedWeakTestSelectedIncrementCoordinateLineDefOfEndpointAndLineDef
   5. SALD.cycle202GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSelectedEndpointCoordinateLineLower2Obligation
   6. SALD.cycle203GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSelectedIncrementEndpointLower2Obligation
   7. hSourceTaylorIntegrandSelectedIncrementDef
   8. sourceTaylorIntegrand
   9. sourceSelectedLineIncrement
   10. appendix.tex:958-970
   11. appendix.tex:983-996
   12. appendix.tex:1161-1170
   13. appendix.tex:1379-1387
   14. source_contract_gap_missing_source_taylor_integrand_selected_increment_definition

   reusedBy : List String (explicit)

   Declared consumers as strings, default empty.

   Ordered data items

   1. hSourceTaylorIntegrandRawDef
   2. hBrownianCoordinateGeneratorTaylorIntegralDef
   3. sald.general_moving_target_discrete.em_interpolation_fp
   4. sald.general_moving_target_discrete.kl_derivative
   5. divergence/FI/IBP handoff

   status : AutoSamplingTheory.ProofStatus (explicit)

   Recorded workflow status, default planned.

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

def cycle204GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSourceTaylorIntegrandSelectedIncrementLower2Dag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle204.lower_2_packet.source_taylor_integrand_selected_increment_source_gap"
      interface := "Typed source-cited boundary: hSourceTaylorIntegrandSelectedIncrementDef is not closed by a same-shape wrapper; the existing cycle-189/190 bridges already show that this field is the smaller source contract needed before endpoint-coordinate and endpoint-difference fields can feed hSourceTaylorIntegrandRawDef."
      source := saldGeneralMovingTargetDiscreteEmSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle204GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSourceTaylorIntegrandSelectedIncrementLower2Obligation",
        "SALD.selectedWeakTestSourceTaylorIntegrandRawDefOfSelectedIncrementAndLineDef",
        "SALD.selectedWeakTestSourceTaylorIntegrandRawDefOfSelectedIncrementEndpointAndLineDef",
        "SALD.selectedWeakTestSelectedIncrementCoordinateLineDefOfEndpointAndLineDef",
        "SALD.cycle202GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSelectedEndpointCoordinateLineLower2Obligation",
        "SALD.cycle203GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSelectedIncrementEndpointLower2Obligation",
        "hSourceTaylorIntegrandSelectedIncrementDef",
        "sourceTaylorIntegrand",
        "sourceSelectedLineIncrement",
        "appendix.tex:958-970",
        "appendix.tex:983-996",
        "appendix.tex:1161-1170",
        "appendix.tex:1379-1387",
        "source_contract_gap_missing_source_taylor_integrand_selected_increment_definition"
      ]
      reusedBy := [
        "hSourceTaylorIntegrandRawDef",
        "hBrownianCoordinateGeneratorTaylorIntegralDef",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.general_moving_target_discrete.kl_derivative",
        "divergence/FI/IBP handoff"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 205 lower_2: selected-line raw Taylor split source gap -/

/-- Cycle-205 lower_2 packet for the selected-line raw Taylor split.

The cycle-188 bridge already reduces `hSelectedLineTaylorSplitDef` to the raw
one-dimensional selected-line Taylor identity plus source-term naming fields.
Local inspection found `normalizedRemainder` only as an abstract parameter in
that interface and did not find an original-paper definition of it as the
residual after the first and second scalar Taylor terms, so this packet records
that exact source contract instead of promoting the Taylor split.
-/