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}

-- The leading nonrelativistic energy is determined, not separately stored.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) :
    f.pionlessOnShellEnergyValueAt = fun p => f.momentumValue p ^ 2 / f.nucleonMassValue := rfl

-- Every selected value and retained datum is visible in the construction.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) :
    f.pionlessPDSFormulaReadout =
      { nucleonMassValue := f.nucleonMassValue
        subtractionScaleValueAt := f.subtractionScaleValueAt
        momentumValueAt := f.momentumValue
        centerOfMassEnergyValueAt := f.pionlessOnShellEnergyValueAt
        contactPolynomialValueAt := f.pionlessContactPolynomialValueAt
        pdsLoopValueAt := f.pionlessPDSLoopValueAt
        pdsAmplitudeValueAt := f.pionlessPDSAmplitudeValueAt } := rfl

-- The two external interpretation obligations remain; the kinematic values
-- are no longer independently chosen data requiring three equalities.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) :
    f.PionlessPDSFormulaReadoutRepresentsSelectedPhysicsAt =
      (f.formulaOnShellEnergyFamilyRepresentsAt f.pionlessPDSFormulaReadout.centerOfMassEnergyValueAt ∧
       f.formulaContactPolynomialRepresentsAt f.pionlessPDSFormulaReadout.contactPolynomialValueAt) := rfl

-- Exact preservation of the former five-clause boundary for the generated
-- readout. This is not an equivalence for an arbitrary unrelated old readout.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit) :
    f.PionlessPDSFormulaReadoutRepresentsSelectedPhysicsAt ↔
      (f.pionlessPDSFormulaReadout.nucleonMassValue = f.nucleonMassValue ∧
       f.pionlessPDSFormulaReadout.subtractionScaleValueAt = f.subtractionScaleValueAt ∧
       f.pionlessPDSFormulaReadout.momentumValueAt = f.momentumValue ∧
       f.formulaOnShellEnergyFamilyRepresentsAt f.pionlessPDSFormulaReadout.centerOfMassEnergyValueAt ∧
       f.formulaContactPolynomialRepresentsAt f.pionlessPDSFormulaReadout.contactPolynomialValueAt) := by
  simp [NuclearScatteringFramework.PionlessPDSFormulaReadoutRepresentsSelectedPhysicsAt,
    NuclearScatteringFramework.pionlessPDSFormulaReadout]

-- An old on-shell record has no further energy choice after M and p agree.
-- Equality transports every old loop, bubble and normalization claim.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (old : PionlessPDSFormulaReadout Channel Scale Momentum)
    (massNonzero : f.nucleonMassValue ≠ 0)
    (interaction : old.contactPolynomialValueAt = f.pionlessContactPolynomialValueAt)
    (loop : old.pdsLoopValueAt = f.pionlessPDSLoopValueAt)
    (amplitude : old.pdsAmplitudeValueAt = f.pionlessPDSAmplitudeValueAt) :
    old = f.pionlessPDSFormulaReadout ↔
      old.nucleonMassValue = f.nucleonMassValue ∧
        old.subtractionScaleValueAt = f.subtractionScaleValueAt ∧
        old.momentumValueAt = f.momentumValue ∧ old.OnShellEnergyAt := by
  constructor
  · intro same
    rw [same]
    refine ⟨rfl, rfl, rfl, ?_⟩
    intro p
    dsimp [NuclearScatteringFramework.pionlessPDSFormulaReadout,
      NuclearScatteringFramework.pionlessOnShellEnergyValueAt]
    field_simp
  · rintro ⟨mass, scale, momentum, shell⟩
    have energy : old.centerOfMassEnergyValueAt = f.pionlessOnShellEnergyValueAt := by
      funext p
      apply (eq_div_iff massNonzero).mpr
      simpa [mass, momentum, mul_comm] using shell p
    cases old
    simp_all [NuclearScatteringFramework.pionlessPDSFormulaReadout]

example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum) :
    f.pdsLoopIntegralObtained 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))) := rfl

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.EquationFivePDSLoopFormulaAt) := rfl

-- The formula target is computed, not an independently assignable value.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum) :
    f.pdsAmplitudeFormulaValue c s p =
      -f.pionlessPDSFormulaReadout.contactPolynomialValueAt c s p /
        f.pionlessPDSFormulaReadout.bubbleDenominatorValueAt c s p := rfl

example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum) :
    f.pdsAmplitudeObtained c s p =
      (f.pionlessPDSFormulaReadout.bubbleDenominatorValueAt c s p ≠ 0 ∧
        f.pionlessPDSFormulaReadout.pdsAmplitudeValueAt c s p =
          f.pdsAmplitudeFormulaValue c s p) := rfl

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.EquationSixPDSAmplitudeFormulaAt) := rfl

-- Altering the later abstract pion-inclusive family cannot change this result.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (other : Channel -> Scale -> Momentum -> f.AmplitudeValue)
    (c : Channel) (s : Scale) (p : Momentum) :
    ({f with fullAmplitudeValueAt := other}.pdsAmplitudeObtained c s p =
      f.pdsAmplitudeObtained c s p) := rfl

-- Faithful numerical readback of both sides suffices for this equivalence.
-- An arbitrary representation predicate did not guarantee it.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (s : Scale) (p : Momentum)
    {Loop : Type} (computed target : Loop) (encode : Loop -> Complex)
    (faithful : Function.Injective encode)
    (computedReadback : encode computed = f.pionlessPDSFormulaReadout.pdsLoopValueAt 0 c s p)
    (targetReadback : encode target =
      -((f.nucleonMassValue / (4 * Real.pi) : Real) : Complex) *
        ((f.subtractionScaleValueAt s : Complex) + Complex.I * (f.momentumValue p : Complex))) :
    computed = target ↔ f.pdsLoopIntegralObtained c s p := by
  unfold NuclearScatteringFramework.pdsLoopIntegralObtained
  rw [← computedReadback, ← targetReadback]
  exact faithful.eq_iff.symm

-- On-shell kinematics and positivity refer to the selected physical values,
-- not a second mass or momentum hidden behind an arbitrary marker.
example (f : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (formula : f.EquationFivePDSLoopFormulaAt) :
    0 < f.nucleonMassValue ∧ ∀ p,
      f.nucleonMassValue * f.pionlessPDSFormulaReadout.centerOfMassEnergyValueAt p =
        f.momentumValue p ^ 2 := by
  constructor
  · exact formula.2.1
  · intro p
    exact formula.2.2.1 p

example (framework : NuclearScatteringFramework
    Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum) :
    framework.PionlessUnitarityCalculation channel scale momentum =
      (framework.EquationSixPDSAmplitudeFormulaAt →
          framework.pionlessPDSFormulaReadout.ElasticContactDomainAt channel scale momentum ∧
          (framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale momentum ≠ 0 →
            (framework.momentumTimesPhaseShiftCotangentValueAt channel momentum : Complex) =
              Complex.I *
                  (framework.pionlessPDSFormulaReadout.momentumValueAt momentum : Complex) +
                (framework.pionlessPDSFormulaReadout.reducedAmplitudeValueAt
                  channel scale momentum)⁻¹)) := rfl