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) (momentum : Momentum) (component : CoupledAmplitudeComponent) (order : Order) :
    f.formulaCoupledSMatrixMinusIdentityValueAt channel momentum component order =
      Complex.I * ((f.momentumValue momentum * f.nucleonMassValue / (2 * Real.pi) : Real) : Complex) *
        f.formulaCoupledAmplitudeValueAt channel momentum component order := rfl

-- The mass and momentum are shared data, not a second numerical assignment.
example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) :
    f.coupledSMatrixFormulaReadout =
      ({ nucleonMassValue := f.nucleonMassValue
         momentumValueAt := f.momentumValue
         amplitudeComponentValueAt := f.formulaCoupledAmplitudeValueAt
         sMatrixMinusIdentityComponentValueAt := f.formulaCoupledSMatrixMinusIdentityValueAt
         phaseObservableValueAt := f.formulaCoupledPhaseObservableValueAt } :
        CoupledSMatrixFormulaReadout Channel Momentum Order) := rfl

-- Amplitudes and phases are the actual momentum-indexed numerical values.
-- No arbitrary abstract zero or representation predicate can replace them.
example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (order : Order) :
    f.DisplayedCoupledSMatrixFormulaAt channel order ↔
      (0 < f.nucleonMassValue ∧
       ∀ momentum component,
         f.formulaCoupledSMatrixMinusIdentityValueAt channel momentum component order =
           Complex.I * ((f.momentumValue momentum * f.nucleonMassValue / (2 * Real.pi) : Real) : Complex) *
             f.formulaCoupledAmplitudeValueAt channel momentum component order ∧
         f.formulaCoupledSMatrixMinusIdentityValueAt channel momentum component order =
           f.coupledSMatrixFormulaReadout.phaseMatrixEntryValueAt channel momentum component order) := Iff.rfl

-- The former five-field readout is retained under exact data identification.
example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (old : CoupledSMatrixFormulaReadout Channel Momentum Order) :
    old = f.coupledSMatrixFormulaReadout ↔
      (old.nucleonMassValue = f.nucleonMassValue ∧
        old.momentumValueAt = f.momentumValue ∧
        old.amplitudeComponentValueAt = f.formulaCoupledAmplitudeValueAt ∧
        old.sMatrixMinusIdentityComponentValueAt = f.formulaCoupledSMatrixMinusIdentityValueAt ∧
        old.phaseObservableValueAt = f.formulaCoupledPhaseObservableValueAt) := by
  cases old
  simp only [NuclearScatteringFramework.coupledSMatrixFormulaReadout,
    CoupledSMatrixFormulaReadout.mk.injEq]

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (old : CoupledSMatrixFormulaReadout Channel Momentum Order)
    (mass : old.nucleonMassValue = f.nucleonMassValue)
    (momentum : old.momentumValueAt = f.momentumValue)
    (amplitude : old.amplitudeComponentValueAt = f.formulaCoupledAmplitudeValueAt)
    (matrix : old.sMatrixMinusIdentityComponentValueAt = f.formulaCoupledSMatrixMinusIdentityValueAt)
    (phase : old.phaseObservableValueAt = f.formulaCoupledPhaseObservableValueAt)
    (channel : Channel) (order : Order) :
    old.EquationCoupledSMatrixAt channel order ↔
      f.coupledSMatrixFormulaReadout.EquationCoupledSMatrixAt channel order := by
  cases old
  simp_all only [NuclearScatteringFramework.coupledSMatrixFormulaReadout]

-- Generated normalization leaves mass positivity and phase agreement as inputs.
example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (order : Order)
    (formula : f.DisplayedCoupledSMatrixFormulaAt channel order) :
    0 < f.nucleonMassValue ∧ ∀ momentum component,
      Complex.I * ((f.momentumValue momentum * f.nucleonMassValue / (2 * Real.pi) : Real) : Complex) *
          f.formulaCoupledAmplitudeValueAt channel momentum component order =
        f.coupledSMatrixFormulaReadout.phaseMatrixEntryValueAt channel momentum component order := by
  refine ⟨formula.1, ?_⟩
  intro momentum component
  exact (formula.2 momentum component).1.symm.trans (formula.2 momentum component).2

-- Zero momentum was not excluded by the source contract. It annihilates
-- the normalization factor; it does not determine a phase branch.
example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (order : Order) (momentum : Momentum)
    (zero : f.momentumValue momentum = 0) :
    ∀ component, f.formulaCoupledSMatrixMinusIdentityValueAt channel momentum component order = 0 := by
  intro component
  simp [NuclearScatteringFramework.formulaCoupledSMatrixMinusIdentityValueAt, zero]

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (newMass : Real) (newMomentum : Momentum -> Real) :
    ({ f with nucleonMassValue := newMass, momentumValue := newMomentum }.coupledSMatrixFormulaReadout) =
      { f.coupledSMatrixFormulaReadout with
        nucleonMassValue := newMass
        momentumValueAt := newMomentum
        sMatrixMinusIdentityComponentValueAt := fun c p k o =>
          Complex.I * ((newMomentum p * newMass / (2 * Real.pi) : Real) : Complex) *
            f.formulaCoupledAmplitudeValueAt c p k o } := rfl

-- Actual nonzero normalization, with unrelated framework data left arbitrary.
-- This is an algebraic diagnostic, not a fitted nuclear amplitude.
example (f : NuclearScatteringFramework Unit Unit Unit Unit Unit Unit Unit Unit) :
    let r := { f with
      nucleonMassValue := 2 * Real.pi
      momentumValue := fun _ => 1
      formulaCoupledAmplitudeValueAt := fun _ _ _ _ => (1 : Complex)
      formulaCoupledPhaseObservableValueAt := fun _ _ _ _ => 0 }
    r.formulaCoupledSMatrixMinusIdentityValueAt () () .sToS () = Complex.I ∧
      ¬r.DisplayedCoupledSMatrixFormulaAt () () := by
  dsimp only
  have normalized : ((2 * Real.pi) / (2 * Real.pi) : Real) = 1 := div_self (by positivity)
  constructor
  · simp [NuclearScatteringFramework.formulaCoupledSMatrixMinusIdentityValueAt]
  · intro formula
    have entry := (formula.2 () .sToS).2
    have imaginary := congrArg Complex.im entry
    norm_num [NuclearScatteringFramework.coupledSMatrixFormulaReadout,
      NuclearScatteringFramework.formulaCoupledSMatrixMinusIdentityValueAt,
      CoupledSMatrixFormulaReadout.phaseMatrixEntryValueAt, normalized] at imaginary

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) :
    f.leadingCoupledAmplitudeOnlySComponent channel ↔
      (∀ p, f.formulaCoupledAmplitudeValueAt channel p .sToD f.leadingOrder = 0 ∧
        f.formulaCoupledAmplitudeValueAt channel p .dToS f.leadingOrder = 0 ∧
        f.formulaCoupledAmplitudeValueAt channel p .dToD f.leadingOrder = 0) := Iff.rfl

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) :
    f.leadingMixingAngleZero channel ↔
      (∀ p, f.formulaCoupledPhaseObservableValueAt channel p .mixingAngle f.leadingOrder = 0) := Iff.rfl

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) :
    f.leadingDWavePhaseZero channel ↔
      (∀ p, f.formulaCoupledPhaseObservableValueAt channel p .dWave f.leadingOrder = 0) := Iff.rfl

-- The input now supplies a numerical branch, never the target implication.
example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) :
    f.LeadingAmplitudeDeterminesPhaseCalculation channel ↔
      (f.DisplayedCoupledSMatrixFormulaAt channel f.leadingOrder ∧ ∀ p,
        -Real.pi / 4 < f.formulaCoupledPhaseObservableValueAt channel p .mixingAngle f.leadingOrder ∧
        f.formulaCoupledPhaseObservableValueAt channel p .mixingAngle f.leadingOrder < Real.pi / 4 ∧
        -Real.pi / 2 < f.formulaCoupledPhaseObservableValueAt channel p .dWave f.leadingOrder ∧
        f.formulaCoupledPhaseObservableValueAt channel p .dWave f.leadingOrder < Real.pi / 2) := Iff.rfl

example (r : CoupledSMatrixFormulaReadout Channel Momentum Order) (c : Channel) (o : Order)
    (formula : r.EquationCoupledSMatrixAt c o)
    (branch : ∀ p,
      -Real.pi / 4 < r.phaseObservableValueAt c p .mixingAngle o ∧
      r.phaseObservableValueAt c p .mixingAngle o < Real.pi / 4 ∧
      -Real.pi / 2 < r.phaseObservableValueAt c p .dWave o ∧
      r.phaseObservableValueAt c p .dWave o < Real.pi / 2)
    (zeros : ∀ p, r.amplitudeComponentValueAt c p .sToD o = 0 ∧
      r.amplitudeComponentValueAt c p .dToD o = 0) :
    ∀ p, r.phaseObservableValueAt c p .mixingAngle o = 0 ∧
      r.phaseObservableValueAt c p .dWave o = 0 :=
  r.zero_amplitudes_determine_phases_on_branch c o formula branch zeros

-- The same positive-momentum, zero-amplitude S matrix also admits nonzero
-- phase representatives. Each branch restriction is substantive.
noncomputable def shiftedPhase (shift : CoupledObservable) :
    CoupledSMatrixFormulaReadout Unit Unit Unit where
  nucleonMassValue := 1
  momentumValueAt := fun _ => 1
  amplitudeComponentValueAt := fun _ _ _ _ => 0
  sMatrixMinusIdentityComponentValueAt := fun _ _ _ _ => 0
  phaseObservableValueAt := fun _ _ observable _ =>
    match shift, observable with
    | .sWave, .sWave | .mixingAngle, .mixingAngle | .dWave, .dWave => Real.pi
    | _, _ => 0

example (shift : CoupledObservable) :
    (shiftedPhase shift).EquationCoupledSMatrixAt () () := by
  refine ⟨by norm_num [CoupledSMatrixFormulaReadout.PositiveMassAt, shiftedPhase], ?_⟩
  intro p component
  cases shift <;> cases component <;>
    norm_num [CoupledSMatrixFormulaReadout.amplitudeSideValueAt,
      CoupledSMatrixFormulaReadout.phaseMatrixEntryValueAt, shiftedPhase,
      mul_comm Complex.I, Complex.ofReal_mul, Complex.exp_two_pi_mul_I]

-- The retained assumptions are jointly realizable, with no S-wave phase bound.
example : (shiftedPhase .sWave).ZeroPhaseBranchAt () () := by
  intro p
  dsimp [shiftedPhase]
  exact ⟨by linarith [Real.pi_pos], by linarith [Real.pi_pos],
    by linarith [Real.pi_pos], by linarith [Real.pi_pos]⟩

example : (shiftedPhase .mixingAngle).phaseObservableValueAt () () .mixingAngle () ≠ 0 ∧
    ¬ (shiftedPhase .mixingAngle).ZeroPhaseBranchAt () () := by
  constructor
  · exact Real.pi_ne_zero
  · intro branch
    have upper := (branch ()).2.1
    norm_num [shiftedPhase] at upper
    linarith [Real.pi_pos]

example : (shiftedPhase .dWave).phaseObservableValueAt () () .dWave () ≠ 0 ∧
    ¬ (shiftedPhase .dWave).ZeroPhaseBranchAt () () := by
  constructor
  · exact Real.pi_ne_zero
  · intro branch
    have upper := (branch ()).2.2.2
    norm_num [shiftedPhase] at upper
    linarith [Real.pi_pos]

#print axioms CoupledSMatrixFormulaReadout.zero_amplitudes_determine_phases_on_branch