import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998 Filter
open scoped Topology

-- The primary contract uses the contact germ fixed by K and mu. No free
-- contact function, inverse-amplitude flag or project-defined physics predicate.
example : forall (flow : PionlessRGFlow) (phase : Real -> Real) (p cutoff bound : Real),
    0 < flow.mass ->
    Tendsto (fun q => (phase q - (-flow.inverseScatteringLength)) / q ^ 2)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds (flow.effectiveRange / 2)) ->
    (forall mu, -mu + flow.inverseScatteringLength ≠ 0 ->
      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 < p -> 0 < cutoff -> |cutoff * (flow.effectiveRange / 2)| <= bound ->
    (forall 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) ∧
    (forall mu (leading correction : Complex), -mu + flow.inverseScatteringLength ≠ 0 ->
      let g0 := flow.mass / (4 * Real.pi) * flow.c0 mu
      let g2 := flow.mass / (4 * Real.pi) * flow.c2 mu
      (leading + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) *
          leading = -(g0 : Complex) ∧
        correction + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) *
          correction = -((g2 * p ^ 2 : Real) : Complex) *
            (1 + ((mu : Complex) + Complex.I * (p : Complex)) * leading)) ->
      leading = (-(flow.inverseScatteringLength : Complex) - Complex.I * (p : Complex))⁻¹ ∧
      correction = -((flow.effectiveRange / 2 * p ^ 2 : Real) : Complex) * leading ^ 2 ∧
      ‖correction‖ <= (bound * p / cutoff) * ‖leading‖ ∧
      (bound * p < cutoff -> ‖correction‖ < ‖leading‖) ∧
      Complex.normSq (1 + 2 * Complex.I * (p : Complex) * leading) = 1 ∧
      correction.im = 2 * p * (star leading * correction).re ∧
      (forall t : Real,
        (leading + (t : Complex) * correction).im -
            p * Complex.normSq (leading + (t : Complex) * correction) =
          -p * t ^ 2 * Complex.normSq correction) ∧
      (forall n : Nat,
        let loopSum := (Finset.range (n + 1)).sum (fun j =>
          -(g0 : Complex) * (-(g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ^ j)
        ‖loopSum - leading‖ =
          (|g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖) ^ (n + 1) * ‖leading‖ ∧
        (1 <= |g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖ ->
          ‖leading‖ <= ‖loopSum - leading‖)) ∧
      (forall rho : Real, 0 < mu -> rho < 1 ->
        |flow.inverseScatteringLength| <= rho * mu ->
        1 / (1 + rho) <= |mu * g0| ∧ |mu * g0| <= 1 / (1 - rho))) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_matching_controls_the_complete_first_order_argument

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_matching_controls_the_complete_first_order_argument