import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
open PhysicsLogic.Papers.KaplanSavageWise1998

variable {Channel Scale Momentum Coupling Term Order Regime Fit : Type}

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) : f.subleadingSPhaseCalculated c ↔
      f.coupledObservableCalculatedThrough c .sWave 1 := Iff.rfl

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) : f.mixingAndDWaveOnlyLeadingOrder c ↔
      f.coupledObservableCalculatedThrough c .mixingAngle 1 ∧
      ¬f.coupledObservableCalculatedThrough c .mixingAngle 2 ∧
      f.coupledObservableCalculatedThrough c .dWave 1 ∧
      ¬f.coupledObservableCalculatedThrough c .dWave 2 := Iff.rfl

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (c : Channel) : f.mixingAndDWaveParameterFreeAtDeclaredOrder fit c ↔
      ¬f.requiresAdditionalFitParameterAt fit c .mixingAngle 1 ∧
      ¬f.requiresAdditionalFitParameterAt fit c .dWave 1 := Iff.rfl

-- Knowing every phase through the same degree is not uniform relative NLO.
example :
    let available : CoupledObservable -> Nat -> Prop := fun _ n => n <= 1
    (∀ o, available o 1) ∧ ¬(∀ o, available o (o.leadingPhaseDegree + 1)) := by
  refine ⟨fun _ => le_rfl, ?_⟩
  intro uniform
  have impossible := uniform .mixingAngle
  norm_num [CoupledObservable.leadingPhaseDegree] at impossible