import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
open Filter PhysicsLogic.Papers.KaplanSavageWise1998
open scoped Topology

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 (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) (scale : Scale) (momentum : Momentum) :
    framework.scaleComparableToMomentum scale momentum =
      (1 <= framework.pionlessScaleComparisonFactor ∧
        0 < framework.momentumValue momentum ∧
        framework.momentumValue momentum <=
          framework.pionlessScaleComparisonFactor * framework.subtractionScaleValueAt scale ∧
        framework.subtractionScaleValueAt scale <=
          framework.pionlessScaleComparisonFactor * framework.momentumValue momentum) := rfl

example (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) (scale : Scale) :
    framework.minimalSubtractionAt scale ↔ framework.subtractionScaleValueAt scale = 0 := Iff.rfl

example (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) :
    framework.effectiveRangeExpansionRemainderAt channel =
      (fun momentum => framework.momentumTimesPhaseShiftCotangentValueAt channel momentum -
        (-(framework.scatteringLength channel)⁻¹ + (1 / 2 : Real) *
          framework.effectiveRange channel * framework.momentumValue momentum ^ 2)) := rfl

example (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) :
    framework.effectiveRangeDataMatched channel =
      (framework.scatteringLength channel ≠ 0 ∧
      (∃ sample : Real -> Momentum,
        ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach,
          framework.momentumValue (sample p) = p ∧
            framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) ∧
      ∀ tolerance : Real, 0 < tolerance ->
        ∃ radius : Real, 0 < radius ∧
          ∀ momentum, framework.lowMomentumEffectiveRangeExpansionAt channel momentum ->
            0 < framework.momentumValue momentum ->
            framework.momentumValue momentum < radius ->
            |(framework.momentumTimesPhaseShiftCotangentValueAt channel momentum -
                (-(framework.scatteringLength channel)⁻¹)) /
                  framework.momentumValue momentum ^ 2 - framework.effectiveRange channel / 2| < tolerance) := rfl

example (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) :
    framework.PionlessObservableMatchingAt channel =
    ((framework.pionlessRGFlow channel).PhysicalAt ∧
      ∃ sample : Real -> Momentum,
        (∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach,
          framework.momentumValue (sample p) = p ∧
            framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) ∧
        (∀ mu, (framework.pionlessRGFlow channel).NonpoleAt mu ->
          PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients
            (fun p => -1 / (framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p) + mu))
            (framework.nucleonMassValue / (4 * Real.pi) *
              framework.pionlessCouplingValueAt channel framework.c0 mu)
            (framework.nucleonMassValue / (4 * Real.pi) *
              framework.pionlessCouplingValueAt channel framework.c2 mu)) ∧
        (∀ scale, (framework.pionlessRGFlow channel).NonpoleAt
            (framework.subtractionScaleValueAt scale) ->
          ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach,
            -1 / (framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p) +
              framework.subtractionScaleValueAt scale) =
              framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale (sample p))) := rfl