import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
open PhysicsLogic.Papers.KaplanSavageWise1998

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type}
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (o : CoupledObservable) (degree : Nat) :
    f.coupledObservableCalculatedThrough c o degree ↔
      ∀ n, n <= degree -> f.coupledPhaseCoefficientAvailable c o n := Iff.rfl

-- Knowing one isolated coefficient is not a completed lower-order expansion.
example (f : NuclearScatteringFramework Unit Unit Unit Unit Unit Unit Unit Unit) :
    let sparse := { f with coupledPhaseCoefficientAvailable := fun _ _ n => n = 1 }
    sparse.coupledPhaseCoefficientAvailable () .mixingAngle 1 ∧
      ¬sparse.coupledObservableCalculatedThrough () .mixingAngle 1 := by
  refine ⟨rfl, ?_⟩
  intro covered
  have zero := covered 0 (by omega)
  change (0 : Nat) = 1 at zero
  omega

-- A later isolated calculation remains available without filling an earlier
-- gap. Availability is not a claim that an unknown coefficient is zero.
example (f : NuclearScatteringFramework Unit Unit Unit Unit Unit Unit Unit Unit) :
    let gap := { f with coupledPhaseCoefficientAvailable := fun _ _ n => n ≠ 2 }
    gap.coupledObservableCalculatedThrough () .dWave 1 ∧
      ¬gap.coupledObservableCalculatedThrough () .dWave 2 ∧
      gap.coupledPhaseCoefficientAvailable () .dWave 3 ∧
      ¬gap.coupledObservableCalculatedThrough () .dWave 3 := by
  refine ⟨?_, ?_, by change (3 : Nat) ≠ 2; omega, ?_⟩
  · intro n hn
    change n ≠ 2
    omega
  · intro covered
    exact covered 2 le_rfl rfl
  · intro covered
    exact covered 2 (by omega) rfl