import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
open PhysicsLogic.Papers.KaplanSavageWise1998

example :
    let j := PionAmplitudeJet.Diagnostics.unitaryJet
    (j.AdmissibleOn 1 1 (Set.Ioi 0) ∧
      (∀ mu > 0, j.RunsAt mu) ∧
      (∀ left > 0, ∀ right > 0,
        j.leadingCoefficient 1 left = j.leadingCoefficient 1 right ∧
        j.firstCoefficient 1 1 left = j.firstCoefficient 1 1 right) ∧
      (∃ other > 0, j.withoutMassInsertion.firstCoefficient 1 1 other ≠
        j.withoutMassInsertion.firstCoefficient 1 1 1) ∧
      j.leadingCoefficient 1 2 ≠ 0 ∧
      j.firstCoefficient 1 1 2 ≠ j.withoutMassInsertion.firstCoefficient 1 1 2) ∧
    Filter.Tendsto
      (fun Q : Real => ‖(j.firstCoefficient 1 1 2 - j.withoutMassInsertion.firstCoefficient 1 1 2) /
        (j.leadingCoefficient 1 2 / (Q : Complex))‖)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.Countermodels.scale_independence_requirement_alone_does_not_fix_relative_power_counting

-- Without the relative power of Q the ratio is a nonzero constant, not a vanishing one.
example :
    let j := PionAmplitudeJet.Diagnostics.unitaryJet
    ¬Filter.Tendsto
      (fun _Q : Real => ‖(j.firstCoefficient 1 1 2 - j.withoutMassInsertion.firstCoefficient 1 1 2) /
        j.leadingCoefficient 1 2‖)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by
  dsimp only
  have witness := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.Countermodels.scale_independence_requirement_alone_does_not_fix_relative_power_counting
  have nonzero := div_ne_zero (sub_ne_zero.mpr witness.1.2.2.2.2.2) witness.1.2.2.2.2.1
  intro vanishes
  exact (norm_ne_zero_iff.mpr nonzero) (tendsto_nhds_unique tendsto_const_nhds vanishes)

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.Countermodels.scale_independence_requirement_alone_does_not_fix_relative_power_counting