import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998

example : ∀ (f : PionInclusiveRGFlow) (mu p : Real), 0 < p ->
    f.pionDiagramDenominator mu p ≠ 0 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.real_dressing_cannot_vanish_at_positive_momentum

example : ∀ (f : PionInclusiveRGFlow) (m mu p : Real),
    f.pionLogPrefactor m mu p =
      ((m ^ 2 * f.pionLogCountertermSlope mu : Real) : Complex) /
        f.pionDiagramDenominator mu p ^ 2 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.pion_log_prefactor_is_dressed_mass_slope

example : ∀ (f : PionInclusiveRGFlow) (m mu p d shift : Real),
    f.pionLogPrefactor m mu p * (shift : Complex) +
      f.dressedMassInsertion m mu p (d + f.pionLogCountertermSlope mu * shift) =
    f.dressedMassInsertion m mu p d :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.pion_log_counterterm_shift_cancels

example : ∀ (f : PionInclusiveRGFlow) (mu : Real),
    f.beta .d2 mu = f.mass / (2 * Real.pi) * f.d2 mu * f.c0 mu * mu +
      f.pionLogCountertermSlope mu :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.pion_log_slope_is_the_inhomogeneous_beta

example : ∀ (m mu p : Real), 0 < m -> 0 < mu ->
    Real.log ((m ^ 2 + 4 * p ^ 2) / mu ^ 2) =
      Real.log (m ^ 2 + 4 * p ^ 2) - 2 * Real.log mu :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.pion_log_kernel_at_positive_scale

example : ∀ (f : PionInclusiveRGFlow) (m mu p : Real), 0 < m -> 0 < mu ->
    f.twoLoopPionAmplitude m mu p =
      f.pionLogPrefactor m mu p *
        (-((((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) : Complex) + 1) +
        f.pionLogPrefactor m mu p * (Real.log mu : Complex) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.two_loop_formula_exposes_log_scale

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.pion_log_counterterm_shift_cancels

example {C S P K T O R F : Type} : ∀
    (f : NuclearScatteringFramework C S P K T O R F)
    (c : C) (s : S) (p : P),
    f.pionScaleMomentum p -> f.KSWMixedExpansionAt c s p ->
    f.ExplicitPionSubleadingCalculation c s p -> f.PionCountertermInsertionAt c p :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.explicit_pions_identify_the_mass_counterterm_insertion

example {C S P K T O R F : Type} : ∀
    (f : NuclearScatteringFramework C S P K T O R F)
    (c : C) (s : S) (p : P),
    f.pionScaleMomentum p -> f.KSWMixedExpansionAt c s p ->
    f.ExplicitPionSubleadingCalculation c s p -> ∀ e : S,
    f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
      (f.subtractionScaleValueAt e) (f.momentumValue p) ->
    (let mu := f.subtractionScaleValueAt e
     let q := f.momentumValue p
     let flow := f.pionInclusiveRetainedFlow
     f.subleadingPionLoopValueAt c e p =
       flow.twoLoopPionAmplitude f.pionMassValue mu q ∧
     f.subleadingPionMassInsertionValueAt c e p =
       flow.dressedMassInsertion f.pionMassValue mu q (flow.d2 mu) ∧
     mu * deriv flow.d2 mu =
       flow.mass / (2 * Real.pi) * flow.d2 mu * flow.c0 mu * mu +
         flow.pionLogCountertermSlope mu) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.explicit_pions_link_logarithm_mass_insertion_and_running