import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
open PhysicsLogic.Papers.KaplanSavageWise1998

universe uC uS uP uK uT uO uR uF
variable {Channel : Type uC} {Scale : Type uS} {Momentum : Type uP}
  {Coupling : Type uK} {Term : Type uT} {Order : Type uO}
  {Regime : Type uR} {Fit : Type uF}

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) :
    f.minimalSubtractionRangeRestricted channel ↔
      ∃ p, f.pionlessMomentum p ∧ ¬f.ordinaryMSCountingValid channel p := Iff.rfl

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) :
    f.LargeLengthMSRestrictionCalculation channel scale ↔
      (f.largeScatteringLength channel -> f.subtractionScaleValueAt scale = 0 ->
        (∀ p, f.pionlessMomentum p -> f.ordinaryMSCountingValid channel p ->
          f.momentumSmallComparedWithInverseScatteringLength channel p) ∧
        (∃ p, f.pionlessMomentum p ∧
          ¬f.momentumSmallComparedWithInverseScatteringLength channel p)) := Iff.rfl

-- A necessary inverse-length window need not be sufficient. A second
-- restriction can exclude momenta even inside that window. Both domains
-- are inhabited; the example does not assert a particular nuclear model.
example :
    (∀ p : Real, 0 < p ∧ p < 3 -> p < 1 / 2 -> p < 1) ∧
    (∃ p : Real, 0 < p ∧ p < 3 ∧ p < 1 / 2) ∧
    (∃ p : Real, 0 < p ∧ p < 3 ∧ ¬p < 1) ∧
    (∃ p : Real, 0 < p ∧ p < 3 ∧ p < 1 ∧ ¬p < 1 / 2) := by
  refine ⟨?_, ⟨1 / 4, by norm_num⟩, ⟨2, by norm_num⟩, ⟨3 / 4, by norm_num⟩⟩
  intro p _ smaller
  linarith