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 : ∀ (readout : PionlessPDSFormulaReadout Channel Scale Momentum),
    readout.nucleonMassValue ≠ 0 ->
      (readout.OnShellEnergyAt ↔ readout.centerOfMassEnergyValueAt =
        fun p => readout.momentumValueAt p ^ 2 / readout.nucleonMassValue) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionlessPDSFormulaReadout.on_shell_energy_iff_nonrelativistic_dispersion

example : ∀ (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit),
    f.nucleonMassValue ≠ 0 -> f.pionlessPDSFormulaReadout.OnShellEnergyAt :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.generated_pds_readout_has_nonrelativistic_shell

example : ∀ (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (old : PionlessPDSFormulaReadout Channel Scale Momentum),
    f.nucleonMassValue ≠ 0 ->
    old.contactPolynomialValueAt = f.pionlessContactPolynomialValueAt ->
    old.pdsLoopValueAt = f.pionlessPDSLoopValueAt ->
    old.pdsAmplitudeValueAt = f.pionlessPDSAmplitudeValueAt ->
    (old = f.pionlessPDSFormulaReadout ↔
      old.nucleonMassValue = f.nucleonMassValue ∧
        old.subtractionScaleValueAt = f.subtractionScaleValueAt ∧
        old.momentumValueAt = f.momentumValue ∧ old.OnShellEnergyAt) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pds_readout_eq_generated_iff_kinematics_and_shell

private def energyControl (mass momentum energy : Real) : PionlessPDSFormulaReadout Unit Unit Unit where
  nucleonMassValue := mass
  subtractionScaleValueAt := fun _ => 1
  momentumValueAt := fun _ => momentum
  centerOfMassEnergyValueAt := fun _ => energy
  contactPolynomialValueAt := fun _ _ _ => 1
  pdsLoopValueAt := fun _ _ _ _ => 0
  pdsAmplitudeValueAt := fun _ _ _ => 0

-- At zero mass the shell equation does not determine the energy.
example : (energyControl 0 0 1).OnShellEnergyAt ∧
    (energyControl 0 0 1).centerOfMassEnergyValueAt ≠
      (fun p => (energyControl 0 0 1).momentumValueAt p ^ 2 /
        (energyControl 0 0 1).nucleonMassValue) := by
  constructor
  · intro p; norm_num [energyControl]
  · intro same
    have atPoint := congrFun same ()
    norm_num [energyControl] at atPoint

-- Total two-nucleon energy, not the kinetic energy of just one nucleon.
example : (energyControl 2 2 2).OnShellEnergyAt ∧
    ¬(energyControl 2 2 1).OnShellEnergyAt := by
  constructor
  · intro p; norm_num [energyControl]
  · intro shell
    have atPoint := shell ()
    norm_num [energyControl] at atPoint

-- The relativistic kinetic energy is not silently identified with this shell.
example : 2 * (Real.sqrt ((4 : Real) ^ 2 + 3 ^ 2) - 4) = 2 ∧
    ¬(energyControl 4 3 2).OnShellEnergyAt := by
  constructor
  · norm_num
  · intro shell
    have atPoint := shell ()
    norm_num [energyControl] at atPoint

-- The original public route now concludes an actual complex-valued loop,
-- without another supplier of an abstract loop equality.
example : ∀ (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum),
    f.pionlessMomentum p -> f.pdsSubtractionAt s -> f.PDSLoopCalculation c s p ->
    f.pionlessPDSFormulaReadout.pdsLoopValueAt 0 c s p =
      -((f.nucleonMassValue / (4 * Real.pi) : Real) : Complex) *
        ((f.subtractionScaleValueAt s : Complex) + Complex.I * (f.momentumValue p : Complex)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pds_subtraction_yields_loop_integral

-- Once the selected loop means the concrete formula, its former separate
-- supply is logically redundant in the complete imported-loop contract.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum) :
    f.PDSLoopCalculation c s p ↔
      (f.pionlessMomentum p -> f.pdsSubtractionAt s ->
        f.pdsLoopIntegralObtained c s p ∧ f.EquationFivePDSLoopFormulaAt) := by
  constructor
  · intro calculation pionless pds
    exact ⟨PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pds_subtraction_yields_loop_integral
      f c s p pionless pds calculation, calculation pionless pds⟩
  · intro previous pionless pds
    exact (previous pionless pds).2

-- The same public bubble route now concludes the actual non-pole quotient.
example : ∀ (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum),
    f.largeScatteringLength c ->
    (f.pionlessLeadingContactOrderAt c s p = -1 ∧ f.pionlessBubbleLoopOrderAt s p = 1) ->
    f.pdsLoopIntegralObtained c s p -> f.BubbleResummationCalculation c s p ->
    f.pionlessPDSFormulaReadout.bubbleDenominatorValueAt c s p ≠ 0 ∧
      f.pionlessPDSFormulaReadout.pdsAmplitudeValueAt c s p =
        -f.pionlessPDSFormulaReadout.contactPolynomialValueAt c s p /
          f.pionlessPDSFormulaReadout.bubbleDenominatorValueAt c s p :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.bubble_chain_and_loop_yield_full_amplitude

-- A second supplier of the concrete amplitude equality is redundant.
-- This is not an equivalence with arbitrary old abstract amplitude labels.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum) :
    f.BubbleResummationCalculation c s p ↔
      (f.largeScatteringLength c -> f.bubbleChainRequired c s p ->
        f.pdsLoopIntegralObtained c s p ->
          f.pdsAmplitudeObtained c s p ∧ f.EquationSixPDSAmplitudeFormulaAt) := by
  constructor
  · intro calculation large bubbles loop
    exact ⟨PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.bubble_chain_and_loop_yield_full_amplitude
      f c s p large ((f.bubble_chain_required_iff_source_orders c s p).mp bubbles)
        loop calculation, calculation large bubbles loop⟩
  · intro previous large bubbles loop
    exact (previous large bubbles loop).2

-- A correct nonzero complex loop does not force equality of independently
-- assigned abstract labels. Conversely, equal labels do not repair a wrong loop.
example :
    (PionlessPDSFormulaReadout.Countermodels.elasticPDSControl 1).EquationFivePDSLoopAt ∧
    (PionlessPDSFormulaReadout.Countermodels.elasticPDSControl 1).pdsLoopValueAt 0 () () () = -Complex.I ∧
    (false : Bool) ≠ true := by
  refine ⟨PionlessPDSFormulaReadout.Countermodels.real_contact_bubble_sum_realizes_source_unitarity.1.1,
    ?_, by decide⟩
  norm_num [PionlessPDSFormulaReadout.Countermodels.elasticPDSControl,
    PionlessPDSFormulaReadout.Countermodels.elasticPDSSeed,
    PionlessPDSFormulaReadout.pdsLoopRightHandSideValueAt, Real.pi_ne_zero]

example :
    (() : Unit) = () ∧
      ¬(PionlessPDSFormulaReadout.Countermodels.elasticPDSSeed 1).EquationFivePDSLoopAt := by
  refine ⟨rfl, ?_⟩
  intro formula
  have zeroPower := formula.2.2 0 () () ()
  have imaginary := congrArg Complex.im zeroPower
  norm_num [PionlessPDSFormulaReadout.Countermodels.elasticPDSSeed,
    PionlessPDSFormulaReadout.pdsLoopRightHandSideValueAt, Real.pi_ne_zero] at imaginary

example : forall (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum),
    ((framework.pdsAmplitudeObtained channel scale momentum →
        framework.EquationSixPDSAmplitudeFormulaAt) ∧
      framework.PionlessUnitarityCalculation channel scale momentum) ↔
    (framework.pdsAmplitudeObtained channel scale momentum →
      framework.EquationSixPDSAmplitudeFormulaAt ∧
        framework.pionlessPDSFormulaReadout.ElasticContactDomainAt channel scale momentum ∧
        (framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale momentum ≠ 0 →
          framework.momentumTimesPhaseShiftCotangentValueAt channel momentum =
            framework.pionlessPDSFormulaReadout.contactEffectiveRangeValueAt
              channel scale momentum)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.observable_normalization_and_upstream_formula_iff_contact_readout

example : forall (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum),
    framework.EquationSixPDSAmplitudeFormulaAt →
    framework.PionlessUnitarityCalculation channel scale momentum →
    framework.amplitudeConsistentWithUnitarity channel scale momentum :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pds_amplitude_has_unitary_s_wave_form

example : forall (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum),
    framework.amplitudeConsistentWithUnitarity channel scale momentum →
    framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale momentum ≠ 0 →
    ((framework.scatteringLength channel)⁻¹ -
      framework.pionlessPDSFormulaReadout.subtractionScaleValueAt scale -
      (1 / 2 : Real) * framework.effectiveRange channel * framework.momentumValue momentum ^ 2 -
      framework.effectiveRangeExpansionRemainderAt channel momentum) *
      framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale momentum = 1 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pionless_observable_matching_constrains_the_bubble_contact

example : forall (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum),
    framework.pionlessMomentum momentum →
    framework.largeScatteringLength channel →
    framework.pdsSubtractionAt scale →
    (framework.pionlessLeadingContactOrderAt channel scale momentum = -1 ∧
      framework.pionlessBubbleLoopOrderAt scale momentum = 1) →
    framework.PDSLoopCalculation channel scale momentum →
    framework.BubbleResummationCalculation channel scale momentum →
    framework.PionlessUnitarityCalculation channel scale momentum →
    framework.pdsLoopIntegralObtained channel scale momentum ∧
      framework.pdsAmplitudeObtained channel scale momentum ∧
      framework.amplitudeConsistentWithUnitarity channel scale momentum :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pds_bubble_resummation_yields_pionless_amplitude

-- The complete source route supplies unitarity; no extra bubble-formula
-- supplier is required to connect its result to the measured phase function.
example (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum)
    (pionless : framework.pionlessMomentum momentum)
    (largeLength : framework.largeScatteringLength channel)
    (pds : framework.pdsSubtractionAt scale)
    (orders : framework.pionlessLeadingContactOrderAt channel scale momentum = -1 ∧
      framework.pionlessBubbleLoopOrderAt scale momentum = 1)
    (loop : framework.PDSLoopCalculation channel scale momentum)
    (bubble : framework.BubbleResummationCalculation channel scale momentum)
    (normalization : framework.PionlessUnitarityCalculation channel scale momentum)
    (nonzero : framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale momentum ≠ 0) :
    ((framework.scatteringLength channel)⁻¹ -
      framework.pionlessPDSFormulaReadout.subtractionScaleValueAt scale -
      (1 / 2 : Real) * framework.effectiveRange channel * framework.momentumValue momentum ^ 2 -
      framework.effectiveRangeExpansionRemainderAt channel momentum) *
      framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale momentum = 1 := by
  have result := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pds_bubble_resummation_yields_pionless_amplitude
    framework channel scale momentum pionless largeLength pds orders loop bubble normalization
  exact PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pionless_observable_matching_constrains_the_bubble_contact
    framework channel scale momentum result.2.2 nonzero

#print axioms PionlessPDSFormulaReadout.on_shell_energy_iff_nonrelativistic_dispersion
#print axioms NuclearScatteringFramework.generated_pds_readout_has_nonrelativistic_shell
#print axioms NuclearScatteringFramework.pds_readout_eq_generated_iff_kinematics_and_shell
#print axioms NuclearScatteringFramework.observable_normalization_and_upstream_formula_iff_contact_readout
#print axioms NuclearScatteringFramework.pds_subtraction_yields_loop_integral
#print axioms NuclearScatteringFramework.pds_amplitude_has_unitary_s_wave_form
#print axioms NuclearScatteringFramework.pionless_observable_matching_constrains_the_bubble_contact
#print axioms NuclearScatteringFramework.pds_bubble_resummation_yields_pionless_amplitude