import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998 Filter
open scoped Topology

-- All physical inputs and outputs are explicit. The only project-defined
-- object in this signature is the five-field, proof-free running data.
example : forall (flow : PionlessRGFlow) (phase : Real -> Real)
    (contact : Real -> 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 => (contact mu q - flow.mass / (4 * Real.pi) * flow.c0 mu) / q ^ 2)
        (nhdsWithin 0 (Set.Ioi 0)) (nhds (flow.mass / (4 * Real.pi) * flow.c2 mu))) ->
    (forall mu, -mu + flow.inverseScatteringLength ≠ 0 ->
      ∀ᶠ q in nhdsWithin 0 (Set.Ioi 0), (phase q + mu) * contact mu q = -1) ->
    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 partialSum := (Finset.range (n + 1)).sum (fun j =>
          -(g0 : Complex) * (-(g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ^ j)
        ‖partialSum - leading‖ =
          (|g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖) ^ (n + 1) * ‖leading‖ ∧
        (1 <= |g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖ ->
          ‖leading‖ <= ‖partialSum - leading‖)) ∧
      (forall rho : Real, 0 < mu -> rho < 1 ->
        |flow.inverseScatteringLength| <= rho * mu ->
        1 / (1 + rho) <= |mu * g0| ∧ |mu * g0| <= 1 / (1 - rho))) := by
  intro flow phase contact p cutoff bound physical observable couplings inverseAmplitude
    positive cutoffPositive naturalRange
  have canonical : 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)) := by
    intro mu nonpole
    exact ((ContactMatching.inverse_amplitude_contact_coefficients_iff_germ phase mu _ _).mpr
      ⟨contact mu, couplings mu nonpole, inverseAmplitude mu nonpole⟩).1
  exact (PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_matching_controls_the_complete_first_order_argument :
    forall (data : PionlessRGFlow), _)
    flow phase p cutoff bound
    physical observable canonical positive cutoffPositive naturalRange

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