import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (p : Momentum), f.PionAmplitudeCoefficientAgreementAt c p :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_amplitude_coefficient_agreement_is_derived

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (c : Channel) (p : Momentum),
    f.quarkMassCountertermRequired c p ↔
      (∀ a b n, n <= 1 ->
        f.amplitudeExpansionCoefficient (f.truncatedAmplitudeValueWithTermAt f.quarkMassContact c a p) n =
        f.amplitudeExpansionCoefficient (f.truncatedAmplitudeValueWithTermAt f.quarkMassContact c b p) n) ∧
      (∃ a b n, n <= 1 ∧
        f.amplitudeExpansionCoefficient (f.truncatedAmplitudeValueWithoutTermAt f.quarkMassContact c a p) n ≠
        f.amplitudeExpansionCoefficient (f.truncatedAmplitudeValueWithoutTermAt f.quarkMassContact c b p) n) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.quark_mass_counterterm_required_iff_coefficient_witness

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (momentum : Momentum),
    (f.pionAmplitudeScaleExpansion channel momentum).CompletesAt :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_amplitude_scale_expansion_is_complete

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (momentum : Momentum) (old : PionAmplitudeScaleExpansion Scale),
    (old = f.pionAmplitudeScaleExpansion channel momentum ↔
      old.retained = (f.pionAmplitudeScaleExpansion channel momentum).retained ∧
      old.full = (f.pionAmplitudeScaleExpansion channel momentum).full ∧ old.CompletesAt) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_amplitude_readout_eq_generated_iff

-- The entire former source calculation is recovered, not just a selected
-- coefficient consequence, after completeness has its coefficient meaning.
example {Channel Scale Momentum Coupling Term Order Regime Fit : Type}
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum) :
    f.ScaleCancellationCalculation channel scale momentum ↔
      (f.pionInclusiveRGControlledCouplings ->
        f.subleadingAmplitudeComplete channel scale momentum ->
          f.fullAmplitudeScaleIndependent channel momentum ∧
          (f.pionAmplitudeScaleExpansion channel momentum).CompletesAt ∧
          (f.pionAmplitudeScaleExpansion channel momentum).OmittedBeyondSubleadingAt ∧
          f.PionAmplitudeCoefficientAgreementAt channel momentum) := by
  constructor
  · intro reduced controlled complete
    have invariant := reduced controlled complete
    have low := (f.subleading_complete_iff_omitted_coefficients_vanish channel scale momentum).mp complete
    exact ⟨invariant, f.pion_amplitude_scale_expansion_is_complete channel momentum, low,
      f.pion_amplitude_coefficient_agreement_is_derived channel momentum⟩
  · intro former controlled complete
    exact (former controlled complete).1

example {C S P G T O R F : Type} (f : NuclearScatteringFramework C S P G T O R F)
    (c : C) (s : S) (p : P) :
    f.subleadingAmplitudeComplete c s p ↔
      (f.pionAmplitudeScaleExpansion c p).OmittedBeyondSubleadingAt :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.subleading_complete_iff_omitted_coefficients_vanish
    f c s p

example {C S P G T O R F : Type} (f : NuclearScatteringFramework C S P G T O R F)
    (c : C) (p : P) :
    f.radiationPionsAbsentAtSubleadingOrder c p ↔
      ∀ s, f.radiationPionAmplitudeCoefficientAt c s p 0 = 0 ∧
        f.radiationPionAmplitudeCoefficientAt c s p 1 = 0 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.radiation_absence_iff_zero_leading_and_first_coefficients
    f c p

example {C S P G T O R F : Type} (f : NuclearScatteringFramework C S P G T O R F)
    (c : C) (s : S) (p : P) (old : Prop)
    (meaning : old ↔ f.subleadingAmplitudeComplete c s p) :
    f.ScaleCancellationCalculation c s p ↔
      (f.pionInclusiveRGControlledCouplings -> old ->
        f.fullAmplitudeScaleIndependent c p ∧
          (f.pionAmplitudeScaleExpansion c p).OmittedBeyondSubleadingAt) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.scale_cancellation_iff_identified_legacy_contract
    f c s p old meaning

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum),
    f.pionInclusiveRGControlledCouplings -> f.subleadingAmplitudeComplete channel scale momentum ->
    f.ScaleCancellationCalculation channel scale momentum ->
      f.truncatedAmplitudeScaleIndependentThroughSubleading channel momentum ∧
        f.residualScaleDependenceIsHigherOrder channel momentum :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_inclusive_rg_control_makes_truncated_amplitude_scale_independent_through_computed_order

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum),
    f.pionInclusiveRGControlledCouplings -> f.subleadingAmplitudeComplete channel scale momentum ->
    f.ScaleCancellationCalculation channel scale momentum ->
      ∀ left right n,
        (f.pionAmplitudeScaleExpansion channel momentum).retained left n -
          (f.pionAmplitudeScaleExpansion channel momentum).retained right n =
        -((f.pionAmplitudeScaleExpansion channel momentum).omitted left n -
          (f.pionAmplitudeScaleExpansion channel momentum).omitted right n) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.source_scale_cancellation_retains_the_actual_higher_order_compensation

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_amplitude_scale_expansion_is_complete
#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_amplitude_readout_eq_generated_iff
#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_inclusive_rg_control_makes_truncated_amplitude_scale_independent_through_computed_order
#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.source_scale_cancellation_retains_the_actual_higher_order_compensation