import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998
set_option backward.isDefEq.respectTransparency false
noncomputable section

-- Printed equations (13), (15 IV), (15 V), and their finite formula domain.
-- The corresponding author-TeX labels are 14 and 17, not printed numbers.
example (f : PionInclusiveRGFlow) (m mu p d : Real) :
    f.pionDiagramLeadingAmplitude mu p =
      -(f.c0 mu : Complex) /
        (1 + ((f.c0 mu * f.mass / (4 * Real.pi) : Real) : Complex) *
          ((mu : Complex) + Complex.I * (p : Complex))) ∧
    f.twoLoopPionAmplitude m mu p =
      ((f.axialCoupling ^ 2 / (2 * f.pionDecayConstant ^ 2) : Real) : Complex) *
        (((m * f.mass : Real) : Complex) * f.pionDiagramLeadingAmplitude mu p /
          ((4 * Real.pi : Real) : Complex)) ^ 2 *
        (-((((mu : Complex) + Complex.I * (p : Complex)) / (m : Complex)) ^ 2) +
          Complex.I * (Real.arctan (2 * p / m) : Complex) -
          (1 / 2 : Complex) * (Real.log ((m ^ 2 + 4 * p ^ 2) / mu ^ 2) : Complex) + 1) ∧
    f.dressedMassInsertion m mu p d =
      -((d * m ^ 2 : Real) : Complex) /
        (1 + ((f.c0 mu * f.mass / (4 * Real.pi) : Real) : Complex) *
          ((mu : Complex) + Complex.I * (p : Complex))) ^ 2 ∧
    (f.PionDiagramDomainAt m mu p ↔
      0 < f.mass ∧ 0 < f.pionDecayConstant ∧ 0 < m ∧ 0 < mu ∧ 0 <= p ∧
        f.pionDiagramDenominator mu p ≠ 0) := by
  refine ⟨rfl, rfl, rfl, ?_⟩
  simp only [PionInclusiveRGFlow.PionDiagramDomainAt, PionInclusiveRGFlow.PhysicalAt,
    and_assoc]

example (f : PionInclusiveRGFlow) (mu : Real) :
    f.pionLogCountertermSlope mu =
      f.mass ^ 2 * f.axialCoupling ^ 2 /
        (32 * Real.pi ^ 2 * f.pionDecayConstant ^ 2) * f.c0 mu ^ 2 := rfl

example (f : PionInclusiveRGFlow) (m mu p : Real) :
    f.PionDiagramDomainAt m mu p =
      (f.PhysicalAt ∧ 0 < m ∧ 0 < mu ∧ 0 <= p ∧ f.pionDiagramDenominator mu p ≠ 0) := rfl

example (f : PionInclusiveRGFlow) : f.PhysicalAt =
    (0 < f.mass ∧ 0 < f.pionDecayConstant) := rfl

private def diagnostic : PionInclusiveRGFlow :=
  ⟨4 * Real.pi, 1, 1, fun _ => -1, fun _ => 0, fun _ => 0⟩

-- At this valid point the log coefficient is -1/2 and a shift by 2
-- needs a D2 increment of +1, whose dressed amplitude is +1.
example : diagnostic.PionDiagramDomainAt 1 1 1 ∧
    diagnostic.pionLogCountertermSlope 1 = 1 / 2 ∧
    diagnostic.pionLogPrefactor 1 1 1 = -1 / 2 ∧
    diagnostic.dressedMassInsertion 1 1 1 1 = 1 := by
  norm_num [diagnostic, PionInclusiveRGFlow.PionDiagramDomainAt,
    PionInclusiveRGFlow.PhysicalAt, PionInclusiveRGFlow.pionDiagramDenominator,
    PionInclusiveRGFlow.pionLogCountertermSlope, PionInclusiveRGFlow.pionLogPrefactor,
    PionInclusiveRGFlow.pionDiagramLeadingAmplitude, PionInclusiveRGFlow.dressedMassInsertion,
    Real.pi_pos, Real.pi_ne_zero, Complex.div_re, Complex.div_im,
    Complex.normSq_apply, Complex.ext_iff, pow_two] <;>
    field_simp [Real.pi_ne_zero] <;> norm_num <;> ring

-- The actual domain admits a finite threshold point, but excludes its
-- contact pole, zero subtraction scale, and the unevaluated chiral limit.
example : diagnostic.PionDiagramDomainAt 1 2 0 ∧
    ¬diagnostic.PionDiagramDomainAt 1 1 0 ∧
    ¬diagnostic.PionDiagramDomainAt 1 0 1 ∧
    ¬diagnostic.PionDiagramDomainAt 0 1 1 := by
  norm_num [diagnostic, PionInclusiveRGFlow.PionDiagramDomainAt,
    PionInclusiveRGFlow.PhysicalAt, PionInclusiveRGFlow.pionDiagramDenominator,
    Real.pi_pos, Real.pi_ne_zero]

-- A printed logarithm does not ensure variation if its coefficient vanishes.
example (f : PionInclusiveRGFlow) (m mu p : Real) :
    ({ f with axialCoupling := 0 } : PionInclusiveRGFlow).twoLoopPionAmplitude m mu p = 0 := by
  simp [PionInclusiveRGFlow.twoLoopPionAmplitude, PionInclusiveRGFlow.pionLogPrefactor]