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}

-- Both calculation contracts and the restriction conclusion are unfolded.
-- The excluded-validity witness must be derived from the necessary window.
example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (natural large : Channel) (scale : Scale) (p : Momentum),
    f.naturalScatteringLength natural -> f.largeScatteringLength large ->
    f.subtractionScaleValueAt scale = 0 -> f.pionlessMomentum p ->
    f.momentumSmallComparedWithShortRangeScale natural p ->
    (f.naturalScatteringLength natural -> f.subtractionScaleValueAt scale = 0 ->
      f.momentumSmallComparedWithShortRangeScale natural p -> f.ordinaryMSCountingValid natural p) ->
    (f.largeScatteringLength large -> f.subtractionScaleValueAt scale = 0 ->
      (∀ q, f.pionlessMomentum q -> f.ordinaryMSCountingValid large q ->
        f.momentumSmallComparedWithInverseScatteringLength large q) ∧
      (∃ q, f.pionlessMomentum q ∧
        ¬f.momentumSmallComparedWithInverseScatteringLength large q)) ->
    f.ordinaryMSCountingValid natural p ∧
      (f.ordinaryMSCountingValid large p -> f.momentumSmallComparedWithInverseScatteringLength large p) ∧
      (∃ q, f.pionlessMomentum q ∧ ¬f.ordinaryMSCountingValid large q) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.natural_and_large_scattering_lengths_have_distinct_ms_scopes

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.natural_and_large_scattering_lengths_have_distinct_ms_scopes