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)
    (old : CoupledSMatrixFormulaReadout Channel Momentum Order),
    (old = f.coupledSMatrixFormulaReadout ↔
      old.nucleonMassValue = f.nucleonMassValue ∧
      old.momentumValueAt = f.momentumValue ∧
      old.amplitudeComponentValueAt = f.formulaCoupledAmplitudeValueAt ∧
      old.phaseObservableValueAt = f.formulaCoupledPhaseObservableValueAt ∧
      (∀ c p k o, old.sMatrixMinusIdentityComponentValueAt c p k o =
        old.amplitudeSideValueAt c p k o)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_readout_eq_generated_iff_normalized

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (order : Order),
    (f.DisplayedCoupledSMatrixFormulaAt channel order ↔
      0 < f.nucleonMassValue ∧
      (∀ p k, f.formulaCoupledSMatrixMinusIdentityValueAt channel p k order =
        f.coupledSMatrixFormulaReadout.phaseMatrixEntryValueAt channel p k order)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.displayed_coupled_formula_iff_phase_matrix

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (old : CoupledSMatrixFormulaReadout Channel Momentum Order) (c : Channel) (o : Order),
    old.nucleonMassValue = f.nucleonMassValue ->
    old.momentumValueAt = f.momentumValue ->
    old.amplitudeComponentValueAt = f.formulaCoupledAmplitudeValueAt ->
    old.phaseObservableValueAt = f.formulaCoupledPhaseObservableValueAt ->
    (old.EquationCoupledSMatrixAt c o ↔
      f.DisplayedCoupledSMatrixFormulaAt c o ∧
      (∀ p k, old.sMatrixMinusIdentityComponentValueAt c p k o = old.amplitudeSideValueAt c p k o)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.old_coupled_formula_iff_generated_and_normalized

-- All source-route outputs retain their original hypotheses and scope.
example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (channel : Channel),
    f.largeScatteringLength channel -> f.coupledPowerCountingAnalogous channel ->
    f.CoupledChannelCalculation fit channel ->
    f.leadingCoupledAmplitudeOnlySComponent channel ∧
      f.leadingMixingAngleZero channel ∧ f.leadingDWavePhaseZero channel :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_channel_leading_order_forces_zero_mixing_and_d_wave

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (channel : Channel),
    f.largeScatteringLength channel -> f.coupledPowerCountingAnalogous channel ->
    f.CoupledChannelCalculation fit channel ->
    f.DisplayedCoupledSMatrixFormulaAt channel f.leadingOrder :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_channel_calculation_retains_displayed_s_matrix_formula

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (channel : Channel),
    f.largeScatteringLength channel -> f.coupledPowerCountingAnalogous channel ->
    f.CoupledChannelCalculation fit channel ->
    f.subleadingSPhaseCalculated channel ∧ f.mixingAndDWaveOnlyLeadingOrder channel ∧
      f.analyticSubleadingCoupledFormulaDeferred channel ∧ f.coupledSPhaseFitted fit channel ∧
      f.mixingAndDWaveParameterFreeAtDeclaredOrder fit channel :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_channel_predictions_are_parameter_free_after_s_wave_fit

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (channel : Channel),
    f.largeScatteringLength channel -> f.coupledPowerCountingAnalogous channel ->
    f.CoupledChannelCalculation fit channel ->
    f.coupledObservableCalculatedThrough channel .sWave 1 ∧
      ¬∀ observable, f.coupledObservableCalculatedThrough channel observable (observable.leadingPhaseDegree + 1) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_channel_calculation_has_nonuniform_observable_order

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (channel : Channel),
    f.largeScatteringLength channel -> f.coupledPowerCountingAnalogous channel ->
    f.CoupledChannelCalculation fit channel ->
    ∀ observable, f.coupledObservableCalculatedThrough channel observable 1 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_calculation_reaches_common_phase_degree_one

example (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (channel : Channel) :
    (f.postCalibrationPredictionModel fit channel).regime = (1 : Nat) := rfl

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (o : CoupledObservable) (lower upper : Nat),
    lower <= upper -> f.coupledObservableCalculatedThrough c o upper ->
    f.coupledObservableCalculatedThrough c o lower :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_coverage_is_downward_closed

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (o : CoupledObservable) (n : Nat),
    (f.coupledObservableCalculatedThrough c o (n + 1) ↔
      f.coupledObservableCalculatedThrough c o n ∧ f.coupledPhaseCoefficientAvailable c o (n + 1)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_coverage_successor_iff

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (o : CoupledObservable),
    ((∀ n, f.coupledObservableCalculatedThrough c o n ↔ f.coupledPhaseCoefficientAvailable c o n) ↔
      (∀ lower upper, lower <= upper -> f.coupledPhaseCoefficientAvailable c o upper ->
        f.coupledPhaseCoefficientAvailable c o lower)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_coverage_matches_input_iff_downward_closed

example : ∀ (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (fit : Fit) (c : Channel),
    f.largeScatteringLength c -> f.coupledPowerCountingAnalogous c ->
    f.CoupledChannelCalculation fit c ->
    ¬f.coupledPhaseCoefficientAvailable c .mixingAngle 2 ∧
      ¬f.coupledPhaseCoefficientAvailable c .dWave 2 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.coupled_calculation_leaves_second_degree_coefficients_unavailable

example : ∀ (r : CoupledSMatrixFormulaReadout Channel Real Order)
    (c : Channel) (o : Order) (slope : CoupledObservable -> Real),
    (∀ observable, HasDerivAt (fun t => r.phaseObservableValueAt c t observable o) (slope observable) 0) ->
    (r.phaseObservableValueAt c 0 .mixingAngle o = 0 ∧ r.phaseObservableValueAt c 0 .dWave o = 0) ->
    ∀ component, HasDerivAt (fun t => r.phaseMatrixEntryValueAt c t component o)
      (match component with
       | .sToS => 2 * Complex.I * (slope .sWave : Complex) *
           Complex.exp (Complex.I * (2 * r.phaseObservableValueAt c 0 .sWave o : Real))
       | .sToD | .dToS => 2 * Complex.I * (slope .mixingAngle : Complex) *
           Complex.exp (Complex.I * (r.phaseObservableValueAt c 0 .sWave o : Real))
       | .dToD => 2 * Complex.I * (slope .dWave : Complex)) 0 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.CoupledSMatrixFormulaReadout.phase_matrix_first_variation_at_unmixed_background

-- An actual differentiable phase family has zero background mixing and
-- D-wave phase but nonzero first variations. The parameter is not momentum.
private noncomputable def phasePerturbation (delta : Real) :
    CoupledSMatrixFormulaReadout Unit Real Unit where
  nucleonMassValue := 1
  momentumValueAt := fun _ => 1
  amplitudeComponentValueAt := fun _ _ _ _ => 0
  sMatrixMinusIdentityComponentValueAt := fun _ _ _ _ => 0
  phaseObservableValueAt := fun _ t observable _ =>
    match observable with
    | .sWave => delta + t
    | .mixingAngle => t
    | .dWave => 2 * t

example (delta : Real) :
    let r := phasePerturbation delta
    r.phaseMatrixEntryValueAt () 0 .sToD () = 0 ∧
    deriv (fun t => r.phaseMatrixEntryValueAt () t .sToD ()) 0 =
      2 * Complex.I * Complex.exp (Complex.I * (delta : Complex)) ∧
    deriv (fun t => r.phaseMatrixEntryValueAt () t .sToD ()) 0 ≠ 0 ∧
    deriv (fun t => r.phaseMatrixEntryValueAt () t .dToD ()) 0 = 4 * Complex.I := by
  dsimp only
  let slope : CoupledObservable -> Real := fun observable =>
    match observable with | .sWave | .mixingAngle => 1 | .dWave => 2
  have derivatives : ∀ observable, HasDerivAt
      (fun t => (phasePerturbation delta).phaseObservableValueAt () t observable ()) (slope observable) 0 := by
    intro observable
    cases observable with
    | sWave => simpa [phasePerturbation, slope] using (hasDerivAt_id (0 : Real)).const_add delta
    | mixingAngle => simpa [phasePerturbation, slope] using hasDerivAt_id (0 : Real)
    | dWave => simpa [phasePerturbation, slope] using (hasDerivAt_id (0 : Real)).const_mul 2
  have variation := (phasePerturbation delta).phase_matrix_first_variation_at_unmixed_background
    () () slope derivatives (by simp [phasePerturbation])
  have off : deriv (fun t => (phasePerturbation delta).phaseMatrixEntryValueAt () t .sToD ()) 0 =
      2 * Complex.I * Complex.exp (Complex.I * (delta : Complex)) := by
    simpa [slope, phasePerturbation] using (variation .sToD).deriv
  refine ⟨by simp [phasePerturbation, CoupledSMatrixFormulaReadout.phaseMatrixEntryValueAt], off, ?_, ?_⟩
  · rw [off]
    exact mul_ne_zero (mul_ne_zero (by norm_num) Complex.I_ne_zero) (Complex.exp_ne_zero _)
  · convert (variation .dToD).deriv using 1 <;> norm_num [slope] <;> ring