import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998

example {C S P K T O R F : Type} : ∀
    (f : NuclearScatteringFramework C S P K T O R F) (old : PionInclusiveRGFlow),
    old = f.pionInclusiveRetainedFlow ↔
      old.mass = f.nucleonMassValue ∧
      old.axialCoupling = f.pionAxialCouplingValue ∧
      old.pionDecayConstant = f.pionDecayConstantValue ∧
      old.c0 = f.pionInclusiveC0 ∧ old.c2 = f.pionInclusiveC2 ∧ old.d2 = f.pionInclusiveD2 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_flow_eq_iff_calibrated_data

example {C S P K T O R F : Type} : ∀
    (f : NuclearScatteringFramework C S P K T O R F),
    f.PionInclusiveRetainedFlowRepresentsAt ↔
      f.pionInclusiveRetainedFlow.mass = f.nucleonMassValue ∧
        ∀ kind scale, 0 < f.subtractionScaleValueAt scale ->
          f.couplingValueAsReal (f.pionInclusiveCouplingValueAt (f.pionInclusiveContact kind) scale) =
            f.pionInclusiveRetainedFlow.coupling kind (f.subtractionScaleValueAt scale) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_flow_representation_iff_with_mass_calibration

-- One mass now feeds nominal running, the pionless formula, and the fitted
-- graded jet. Equality of their other running functions is not asserted.
example {C S P K T O R F : Type}
    (f : NuclearScatteringFramework C S P K T O R F) (fit : F) :
    f.pionInclusiveRetainedFlow.mass = f.pionlessPDSFormulaReadout.nucleonMassValue ∧
    f.pionInclusiveRetainedFlow.mass = (f.singletFitJet fit).couplings.mass := ⟨rfl, rfl⟩

-- Calibration is substantive: an old model with a different mass is not
-- silently identified with the generated flow, even if every function agrees.
example {C S P K T O R F : Type}
    (f : NuclearScatteringFramework C S P K T O R F) (mass : Real)
    (different : mass ≠ f.nucleonMassValue) :
    ({ f.pionInclusiveRetainedFlow with mass := mass } : PionInclusiveRGFlow) ≠
      f.pionInclusiveRetainedFlow := by
  intro equal
  exact different (congrArg PionInclusiveRGFlow.mass equal)

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_flow_eq_iff_calibrated_data