Resummation, Unitarity and Expansion Error

Exact root statement

∀ (flow : PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow) (phase : ℝ → ℝ) (cutoff bound rho c epsilon : ℝ),
  0 < flow.mass →
    Filter.Tendsto (fun q => (phase q - -flow.inverseScatteringLength) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0))
        (nhds (flow.effectiveRange / 2)) →
      (∀ (mu : ℝ),
          -mu + flow.inverseScatteringLength ≠ 0 →
            Filter.Tendsto (fun q => (-1 / (phase q + mu) - flow.mass / (4 * Real.pi) * flow.c0 mu) / q ^ 2)
              (nhdsWithin 0 (Set.Ioi 0)) (nhds (flow.mass / (4 * Real.pi) * flow.c2 mu))) →
        0 < cutoff →
          |cutoff * (flow.effectiveRange / 2)| ≤ bound →
            0 < rho →
              1 ≤ c →
                rho ^ 2 + 2 * c * rho ≤ 1 →
                  0 < epsilon →
                    epsilon < 1 →
                      |flow.inverseScatteringLength| * (bound + 1) < rho * epsilon * cutoff →
                        (∀ (mu : ℝ),
                            -mu + flow.inverseScatteringLength ≠ 0 →
                              flow.c0 mu = 4 * Real.pi / flow.mass * (-mu + flow.inverseScatteringLength)⁻¹ ∧
                                flow.c2 mu =
                                    2 * Real.pi / flow.mass * (-mu + flow.inverseScatteringLength)⁻¹ ^ 2 *
                                      flow.effectiveRange ∧
                                  HasDerivAt flow.c0 (flow.mass / (4 * Real.pi) * flow.c0 mu ^ 2) mu ∧
                                    HasDerivAt flow.c2 (flow.mass / (2 * Real.pi) * flow.c0 mu * flow.c2 mu) mu) ∧
                          (∃ p mu,
                              |flow.inverseScatteringLength| / rho < p ∧
                                p < epsilon * cutoff / (bound + 1) ∧ p ≤ c * mu ∧ mu ≤ c * p) ∧
                            ∀ (p mu : ℝ),
                              |flow.inverseScatteringLength| / rho < p →
                                p < epsilon * cutoff / (bound + 1) →
                                  p ≤ c * mu →
                                    mu ≤ c * p →
                                      -mu + flow.inverseScatteringLength ≠ 0 ∧
                                        have g0 := flow.mass / (4 * Real.pi) * flow.c0 mu;
                                        have g2 := flow.mass / (4 * Real.pi) * flow.c2 mu;
                                        (∃! pair,
                                            pair.1 + ↑g0 * (↑mu + Complex.I * ↑p) * pair.1 = -↑g0 ∧
                                              pair.2 + ↑g0 * (↑mu + Complex.I * ↑p) * pair.2 =
                                                -↑(g2 * p ^ 2) * (1 + (↑mu + Complex.I * ↑p) * pair.1)) ∧
                                          ∀ (leading correction : ℂ),
                                            leading + ↑g0 * (↑mu + Complex.I * ↑p) * leading = -↑g0 ∧
                                                correction + ↑g0 * (↑mu + Complex.I * ↑p) * correction =
                                                  -↑(g2 * p ^ 2) * (1 + (↑mu + Complex.I * ↑p) * leading) →
                                              leading = (-↑flow.inverseScatteringLength - Complex.I * ↑p)⁻¹ ∧
                                                correction = -↑(flow.effectiveRange / 2 * p ^ 2) * leading ^ 2 ∧
                                                  ‖correction‖ ≤ bound * p / cutoff * ‖leading‖ ∧
                                                    ‖correction‖ < epsilon * ‖leading‖ ∧
                                                      ‖correction‖ < ‖leading‖ ∧
                                                        Complex.normSq (1 + 2 * Complex.I * ↑p * leading) = 1 ∧
                                                          correction.im = 2 * p * (star leading * correction).re ∧
                                                            (∀ (t : ℝ),
                                                                (leading + ↑t * correction).im -
                                                                    p * Complex.normSq (leading + ↑t * correction) =
                                                                  -p * t ^ 2 * Complex.normSq correction) ∧
                                                              ∀ (n : ℕ),
                                                                have loopSum :=
                                                                  ∑ j ∈ Finset.range (n + 1),
                                                                    -↑g0 * (-↑g0 * (↑mu + Complex.I * ↑p)) ^ j;
                                                                ‖loopSum - leading‖ =
                                                                    (|g0| * ‖↑mu + Complex.I * ↑p‖) ^ (n + 1) *
                                                                      ‖leading‖ ∧
                                                                  ‖leading‖ ≤ ‖loopSum - leading‖