From Scattering Records to Triplet Range

Exact root statement

∀ (lengths : BlattJackson1949.ThresholdExtraction.Lengths) (bindingMomentum effectiveRange residualBound : ℝ),
  BlattJackson1949.ThresholdExtraction.PhysicalSignBranch lengths →
    BlattJackson1949.ThresholdExtraction.coherentAmplitude lengths ≤ 0 →
      0 < bindingMomentum →
        |Framework.NeutralBoundState.effectiveRangeResidual lengths.triplet⁻¹ effectiveRange bindingMomentum| ≤
            residualBound →
          |Framework.NeutralBoundState.extractedRange
                  (IntensityExtraction.negativeBranchTriplet
                      (IntensityExtraction.intensityRecords.recordAt () lengths))⁻¹
                  bindingMomentum -
                effectiveRange| ≤
            2 / bindingMomentum ^ 2 * residualBound