import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
set_option backward.isDefEq.respectTransparency false
noncomputable section
open PhysicsLogic.Papers.KaplanSavageWise1998

variable {C S P K T O R F : Type}

example (f : NuclearScatteringFramework C S P K T O R F) (fit : F) (old : PionAmplitudeJet) :
    old = f.singletFitJet fit ↔
      old.couplings.mass = f.nucleonMassValue ∧
      old.couplings.axialCoupling = f.pionInclusiveRetainedFlow.axialCoupling ∧
      old.couplings.pionDecayConstant = f.pionInclusiveRetainedFlow.pionDecayConstant ∧
      old.couplings.c0 = f.singletFitLeadingC0 fit ∧
      old.firstC0 = f.singletFitFirstC0 fit ∧
      old.couplings.c2 = f.singletFitC2 fit ∧
      old.couplings.d2 = f.singletFitD2 fit :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.singlet_fit_jet_eq_iff_calibrated_data f fit old

-- Equal contact functions do not excuse a mismatched physical constant.
example (f : NuclearScatteringFramework C S P K T O R F) (fit : F) :
    ({ f.singletFitJet fit with couplings :=
        { (f.singletFitJet fit).couplings with mass := f.nucleonMassValue + 1 } } : PionAmplitudeJet) ≠
      f.singletFitJet fit := by
  intro same
  have mass := congrArg (fun j : PionAmplitudeJet => j.couplings.mass) same
  change f.nucleonMassValue + 1 = f.nucleonMassValue at mass
  linarith

example (f : NuclearScatteringFramework C S P K T O R F)
    (fit : F) (c : C) (s : S) (p : P) :
    f.SingletFitCoefficientReadbackAt fit c s p ->
      f.amplitudeUsesOnlyPionMassCombinationThrough fit f.c0 f.d2 c s p f.subleadingOrder :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.singlet_fit_readback_derives_the_contact_combination f fit c s p

example (f : NuclearScatteringFramework C S P K T O R F)
    (fit : F) (c : C) (s : S) (p : P) :
    f.C0D2CombinationInterpretation fit c s p :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.c0_d2_combination_interpretation_is_derived f fit c s p

example (f : NuclearScatteringFramework C S P K T O R F)
    (fit : F) (c : C) (s : S) (p : P) :
    f.fitUsesNijmegenPhaseShifts fit c -> f.fitOptimizedThroughTwoHundredMeV fit ->
    f.subleadingAmplitudeComplete c s p -> f.SingletFitCalculation fit c s p ->
    f.amplitudeUsesOnlyPionMassCombinationThrough fit f.c0 f.d2 c s p f.subleadingOrder ∧
      f.individualFitValuesNotSeparatelyMeaningfulThrough fit f.c0 f.d2 c s p f.subleadingOrder :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.singlet_fit_retains_c0_d2_combination_scope f fit c s p

example :
    let reported := PionAmplitudeJet.Diagnostics.unitaryJet.withSubleadingContacts (-1 / 2) 1
    let alternative := PionAmplitudeJet.Diagnostics.unitaryJet.withSubleadingContacts (-3 / 2) 2
    (reported.couplings.PhysicalAt ∧ alternative.couplings.PhysicalAt ∧
      reported.couplings.axialCoupling ≠ 0 ∧
      reported.couplings.c0 1 + reported.firstC0 1 ≠ 0 ∧ reported.couplings.d2 1 ≠ 0 ∧
      ∀ p > 0, reported.leadingCoefficient p 1 = alternative.leadingCoefficient p 1 ∧
        reported.firstCoefficient 1 p 1 = alternative.firstCoefficient 1 p 1) ∧
    ¬(reported.couplings.c0 1 + reported.firstC0 1 =
        alternative.couplings.c0 1 + alternative.firstC0 1 ∧
      reported.couplings.d2 1 = alternative.couplings.d2 1) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.Countermodels.reported_c0_and_d2_values_with_combination_only_amplitude_do_not_supply_separate_meaning

-- Without the compensating contact shift, a different D2 changes the curve.
example (p : Real) (positive : 0 < p) :
    (PionAmplitudeJet.Diagnostics.unitaryJet.withSubleadingContacts (-1 / 2) 1).firstCoefficient 1 p 1 ≠
      (PionAmplitudeJet.Diagnostics.unitaryJet.withSubleadingContacts (-1 / 2) 2).firstCoefficient 1 p 1 := by
  rw [ne_eq, PionAmplitudeJet.subleading_contact_prediction_eq_iff_combination_eq
    _ _ _ _ _ _ _ _ positive]
  norm_num

private def jet : PionAmplitudeJet := PionAmplitudeJet.Diagnostics.unitaryJet

-- The compensating pair is indistinguishable only at the selected mass.
example (p : Real) (positive : 0 < p) :
    (jet.withSubleadingContacts (-1 / 2) 1).firstCoefficient 2 p 1 ≠
      (jet.withSubleadingContacts (-3 / 2) 2).firstCoefficient 2 p 1 := by
  rw [ne_eq, PionAmplitudeJet.subleading_contact_prediction_eq_iff_combination_eq
    _ _ _ _ _ _ _ _ positive]
  norm_num

-- A real interacting retained-model readout, not an assertion of a Nijmegen
-- fit or of any unrelated source route. The higher coefficients are unused.
private def data : NuclearScatteringFramework Unit Real Real (Fin 3) (Fin 4) Int Unit Unit where
  singletChannel := ()
  coupledChannel := ()
  c0 := 0
  c2 := 1
  d2 := 2
  leadingContact := 0
  firstCorrection := 1
  quarkMassContact := 2
  onePionExchange := 3
  leadingOrder := -1
  subleadingOrder := 0
  regimeOf := fun _ _ _ => ()
  powerCounting := {
    contributesAt := fun _ _ _ => False
    noLaterThan := fun left right => left <= right
    suppressedRelativeTo := fun _ _ _ => False
    retainedThrough := fun _ _ => False
    resummedAt := fun _ _ => False
    perturbativeAt := fun _ _ => False }
  AmplitudeValue := Nat -> Complex
  CouplingValue := Real
  pionlessContactPolynomialValueAt := fun _ _ _ => 0
  pionlessPDSLoopValueAt := fun _ _ _ _ => 0
  pionlessPDSAmplitudeValueAt := fun _ _ _ => 0
  formulaOnShellEnergyFamilyRepresentsAt := fun _ => False
  formulaContactPolynomialRepresentsAt := fun _ => False
  pionInclusiveCouplingValueAt := fun k mu =>
    if k = 0 then jet.couplings.c0 mu + jet.firstC0 mu
    else if k = 1 then jet.couplings.c2 mu else jet.couplings.d2 mu
  pionlessCouplingValueAt := fun _ _ _ => 0
  pionAxialCouplingValue := jet.couplings.axialCoupling
  pionDecayConstantValue := jet.couplings.pionDecayConstant
  pionInclusiveC0 := fun mu => jet.couplings.c0 mu + jet.firstC0 mu
  pionInclusiveC2 := jet.couplings.c2
  pionInclusiveD2 := jet.couplings.d2
  subtractionScaleValueAt := id
  nucleonMassValue := 4 * Real.pi
  couplingValueAsReal := id
  momentumValue := id
  scatteringLength := fun _ => 0
  effectiveRange := fun _ => 0
  momentumTimesPhaseShiftCotangentValueAt := fun _ _ => 0
  lowMomentumEffectiveRangeExpansionAt := fun _ _ => False
  fullAmplitudeValueAt := fun _ _ _ _ => 0
  physicalAmplitudeValue := fun _ _ _ => 0
  subleadingPionLoopValueAt := fun _ _ _ => 0
  subleadingPionMassInsertionValueAt := fun _ _ _ => 0
  pionMassValue := 1
  truncatedAmplitudeValueWithTermAt := fun _ _ mu p n =>
    if n = 0 then jet.leadingCoefficient p mu
    else if n = 1 then jet.firstCoefficient 1 p mu else 0
  truncatedAmplitudeValueWithoutTermAt := fun _ _ _ _ _ => 0
  amplitudeExpansionCoefficient := fun value n => value n
  formulaCoupledAmplitudeValueAt := fun _ _ _ _ => 0
  formulaCoupledPhaseObservableValueAt := fun _ _ _ _ => 0
  coupledPhaseCoefficientAvailable := fun _ _ _ => False
  analyticCoupledAmplitudeFormulaProvided := fun _ _ _ => False
  fitUsesCoupledObservable := fun _ _ _ => False
  requiresAdditionalFitParameterAt := fun _ _ _ _ => False
  pionlessMomentum := fun _ => False
  pionScaleMomentum := fun _ => False
  naturalScatteringLength := fun _ => False
  largeScatteringLength := fun _ => False
  nearThresholdState := fun _ => False
  pdsSubtractionAt := fun _ => False
  pionlessScaleComparisonFactor := 2
  pionlessContactOrderAt := fun _ _ _ _ => 0
  pionlessBubbleLoopOrderAt := fun _ _ => 0
  physicalAmplitudeRequiredScaleIndependent := fun _ _ => False
  ordinaryMSCountingValid := fun _ _ => False
  momentumSmallComparedWithShortRangeScale := fun _ _ => False
  momentumSmallComparedWithInverseScatteringLength := fun _ _ => False
  pionlessLeadingAmplitudeValueAt := fun _ _ _ => 0
  pionlessDerivativeInsertionAmplitudeValueAt := fun _ _ _ => 0
  radiationPionAmplitudeCoefficientAt := fun _ _ _ n => if n = 1 then 1 else 0
  fitUsesNijmegenPhaseShifts := fun _ _ => False
  fitOptimizedThroughTwoHundredMeV := fun _ => False
  leadingCouplingNearLargeLengthValue := fun _ => False
  derivativeCouplingHasExpectedSize := fun _ => False
  singletFitLeadingC0 := fun _ => jet.couplings.c0
  singletFitFirstC0 := fun _ => jet.firstC0
  singletFitC2 := fun _ => jet.couplings.c2
  singletFitD2 := fun _ => jet.couplings.d2
  phaseShiftAgreementGood := fun _ _ => False
  fitSuggestsExpansionValid := fun _ _ => False
  subleadingLeadingRatioAtLeastHalfAboveHundredMeV := fun _ _ => False
  neglectedQuadraticTermsControlledAboveHundredMeV := fun _ _ => False
  coupledPowerCountingAnalogous := fun _ => False

private theorem calibrated : data.SingletFitCoefficientReadbackAt () () 1 1 := by
  dsimp [NuclearScatteringFramework.SingletFitCoefficientReadbackAt,
    NuclearScatteringFramework.singletFitJet, NuclearScatteringFramework.pionCoefficientJet,
    NuclearScatteringFramework.pionInclusiveRetainedFlow, data]
  norm_num [jet,
    PionAmplitudeJet.Diagnostics.unitaryJet, PionAmplitudeJetCalculus.Diagnostic.unitaryLeadingFlow,
    PionInclusiveRGFlow.PhysicalAt, Real.pi_pos]

example : data.individualFitValuesNotSeparatelyMeaningfulThrough
    () data.c0 data.d2 () 1 1 data.subleadingOrder :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.c0_d2_combination_interpretation_is_derived data () () 1 1
    (PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.singlet_fit_readback_derives_the_contact_combination data () () 1 1 calibrated)

-- Matching c alone to the reported C0 would miss the nonzero s correction.
example : ¬NuclearScatteringFramework.SingletFitCoefficientReadbackAt ({ data with
    pionInclusiveCouplingValueAt := fun k mu =>
      if k = 0 then jet.couplings.c0 mu else data.pionInclusiveCouplingValueAt k mu }
    : NuclearScatteringFramework Unit Real Real (Fin 3) (Fin 4) Int Unit Unit) () () 1 1 := by
  dsimp [NuclearScatteringFramework.SingletFitCoefficientReadbackAt,
    NuclearScatteringFramework.singletFitJet, NuclearScatteringFramework.pionCoefficientJet,
    NuclearScatteringFramework.pionInclusiveRetainedFlow, data]
  norm_num [jet,
    PionAmplitudeJet.Diagnostics.unitaryJet, PionAmplitudeJetCalculus.Diagnostic.unitaryLeadingFlow,
    PionInclusiveRGFlow.PhysicalAt, Real.pi_pos]

example : ¬NuclearScatteringFramework.SingletFitCoefficientReadbackAt ({ data with
    pionInclusiveCouplingValueAt := fun k mu =>
      if k = 2 then (1 : Real)
      else data.pionInclusiveCouplingValueAt k mu }
    : NuclearScatteringFramework Unit Real Real (Fin 3) (Fin 4) Int Unit Unit) () () 1 1 := by
  dsimp [NuclearScatteringFramework.SingletFitCoefficientReadbackAt,
    NuclearScatteringFramework.singletFitJet, NuclearScatteringFramework.pionCoefficientJet,
    NuclearScatteringFramework.pionInclusiveRetainedFlow, data]
  norm_num [jet,
    PionAmplitudeJet.Diagnostics.unitaryJet, PionAmplitudeJetCalculus.Diagnostic.unitaryLeadingFlow,
    PionInclusiveRGFlow.PhysicalAt, Real.pi_pos]

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.c0_d2_combination_interpretation_is_derived
#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.singlet_fit_retains_c0_d2_combination_scope