import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998 PhysicsLogic.Framework.ElasticSWave

example (r : PionlessContactExpansionReadout) : r =
    ⟨r.mass, r.momentum, r.subtractionScale, r.leadingCoupling, r.derivativeCoupling,
      r.leadingAmplitude, r.derivativeInsertionAmplitude⟩ := rfl
example (r : PionlessContactExpansionReadout) : r.scaledLeadingCoupling =
    r.mass / (4 * Real.pi) * r.leadingCoupling := rfl
example (r : PionlessContactExpansionReadout) : r.scaledInsertion =
    r.mass / (4 * Real.pi) * r.derivativeCoupling * r.momentum ^ 2 := rfl
example (r : PionlessContactExpansionReadout) : r.bubbleDenominator =
    contactDenominator r.scaledLeadingCoupling r.subtractionScale r.momentum := rfl
example (r : PionlessContactExpansionReadout) : r.leadingReducedAmplitude =
    (r.mass / (4 * Real.pi) : Real) * r.leadingAmplitude := rfl
example (r : PionlessContactExpansionReadout) : r.correctionReducedAmplitude =
    (r.mass / (4 * Real.pi) : Real) * r.derivativeInsertionAmplitude := rfl
example (r : PionlessContactExpansionReadout) : r.EquationThirteenAt ↔
    0 < r.mass ∧ 0 ≤ r.momentum ∧
      let interaction : PowerSeries Complex :=
        PowerSeries.C (r.scaledLeadingCoupling : Complex) +
          PowerSeries.X * PowerSeries.C (r.scaledInsertion : Complex)
      let result : PowerSeries Complex :=
        PowerSeries.C r.leadingReducedAmplitude +
          PowerSeries.X * PowerSeries.C r.correctionReducedAmplitude
      forall n : Nat, n <= 1 -> PowerSeries.coeff n
        (result + interaction * PowerSeries.C
          ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) *
            result + interaction) = 0 := Iff.rfl

-- The former equations follow without calling the paper's preservation proof.
example (r : PionlessContactExpansionReadout) : r.EquationThirteenAt ↔
    0 < r.mass ∧ 0 ≤ r.momentum ∧
    (r.leadingReducedAmplitude + (r.scaledLeadingCoupling : Complex) *
      ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) *
        r.leadingReducedAmplitude = -(r.scaledLeadingCoupling : Complex) ∧
      r.correctionReducedAmplitude + (r.scaledLeadingCoupling : Complex) *
        ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) *
          r.correctionReducedAmplitude = -(r.scaledInsertion : Complex) *
            (1 + ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) *
              r.leadingReducedAmplitude)) := by
  unfold PionlessContactExpansionReadout.EquationThirteenAt
  dsimp only
  rw [ContactChains.graded_scattering_equation_iff_first_two_terms]
  simp

-- Independently retain the original dimensionful contract, without calling
-- the paper's normalization theorem or assuming its conclusion. The local
-- interaction equivalence is independently checked in the chain fixture.
example (r : PionlessContactExpansionReadout) : r.EquationThirteenAt ↔
    0 < r.mass ∧ 0 ≤ r.momentum ∧ r.bubbleDenominator ≠ 0 ∧
    r.leadingAmplitude = -(r.leadingCoupling : Complex) / r.bubbleDenominator ∧
    r.derivativeInsertionAmplitude = -(r.derivativeCoupling : Complex) * (r.momentum : Complex)^2 /
      r.bubbleDenominator^2 := by
  have first : contactAmplitude r.scaledLeadingCoupling r.subtractionScale r.momentum =
      (r.mass / (4 * Real.pi) : Real) * (-(r.leadingCoupling : Complex) / r.bubbleDenominator) := by
    unfold contactAmplitude PionlessContactExpansionReadout.bubbleDenominator
      PionlessContactExpansionReadout.scaledLeadingCoupling
    push_cast
    ring
  have second : contactInsertionAmplitude r.scaledLeadingCoupling r.scaledInsertion
      r.subtractionScale r.momentum =
      (r.mass / (4 * Real.pi) : Real) *
        (-(r.derivativeCoupling : Complex) * (r.momentum : Complex)^2 / r.bubbleDenominator^2) := by
    unfold contactInsertionAmplitude PionlessContactExpansionReadout.scaledInsertion
      PionlessContactExpansionReadout.bubbleDenominator
    push_cast
    ring
  unfold PionlessContactExpansionReadout.EquationThirteenAt
  dsimp only
  rw [ContactChains.graded_scattering_equation_iff_first_two_terms]
  simp only [map_add, map_mul, PowerSeries.constantCoeff_C, PowerSeries.constantCoeff_X,
    zero_mul, add_zero, PowerSeries.coeff_zero_eq_constantCoeff,
    PowerSeries.coeff_one_mul, PowerSeries.coeff_C, PowerSeries.coeff_X,
    if_pos, ite_false, Nat.one_ne_zero, zero_add, one_mul, mul_zero]
  rw [ContactChains.local_interaction_equations_iff_source_amplitudes]
  change (0 < r.mass ∧ 0 ≤ r.momentum ∧ r.bubbleDenominator ≠ 0 ∧
    r.leadingReducedAmplitude = contactAmplitude r.scaledLeadingCoupling r.subtractionScale r.momentum ∧
    r.correctionReducedAmplitude = contactInsertionAmplitude r.scaledLeadingCoupling r.scaledInsertion
      r.subtractionScale r.momentum) ↔ _
  unfold PionlessContactExpansionReadout.leadingReducedAmplitude
    PionlessContactExpansionReadout.correctionReducedAmplitude
  rw [first, second]
  constructor
  · rintro ⟨mass, momentum, nonpole, leading, insertion⟩
    have normalization : ((r.mass / (4 * Real.pi) : Real) : Complex) ≠ 0 := by
      exact_mod_cast (ne_of_gt (div_pos mass (by positivity : 0 < 4 * Real.pi)))
    exact ⟨mass, momentum, nonpole, mul_left_cancel₀ normalization leading,
      mul_left_cancel₀ normalization insertion⟩
  · rintro ⟨mass, momentum, nonpole, leading, insertion⟩
    exact ⟨mass, momentum, nonpole, congrArg _ leading, congrArg _ insertion⟩