import PhysicsLogic.Papers.KaplanSavageWise1998

set_option backward.isDefEq.respectTransparency false
open Filter PhysicsLogic.Papers.KaplanSavageWise1998

-- Every represented positive scale retains its equation and physical
-- coupling readout. Global continuation and nonconstant running are separate.
example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit),
    f.pionInclusiveRGControlledCouplings ->
    ∀ scale, 0 < f.subtractionScaleValueAt scale ->
    let mu := f.subtractionScaleValueAt scale
    ∀ kind,
      mu * deriv (f.pionInclusiveRetainedFlow.coupling kind) mu =
        f.pionInclusiveRetainedFlow.beta kind mu :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.controlled_pion_running_retains_actual_weighted_equations

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit),
    f.pionInclusiveRGControlledCouplings ->
    ∀ 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.controlled_pion_running_identifies_sampled_values

example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} : ∀
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit),
    (∀ mu : Real, 0 < mu -> ∃ scale, f.subtractionScaleValueAt scale = mu) ->
    (f.pionInclusiveRGControlledCouplings ↔
      f.pionInclusiveRetainedFlow.PhysicalAt ∧
      (∀ mu, 0 < mu -> f.pionInclusiveRetainedFlow.RetainedBetaEquationsAt mu) ∧
      f.PionInclusiveRetainedFlowRepresentsAt) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_rg_control_iff_global_on_positive_scale_coverage

-- The old encoded equality has exactly the numerical meaning when the
-- encoding is faithful. The comparison is at intrinsic source-contact
-- indices; it does not identify different operators through an aliased label.
example {Value Scale : Type} (flow : PionInclusiveRGFlow) (mu : Scale -> Real)
    (decode : Value -> Real) (faithful : Function.Injective decode)
    (beta slope : PionInclusiveContact -> Scale -> Value)
    (betaReadout : ∀ kind scale, 0 < mu scale ->
      decode (beta kind scale) = flow.beta kind (mu scale))
    (slopeReadout : ∀ kind scale, 0 < mu scale ->
      decode (slope kind scale) = mu scale * deriv (flow.coupling kind) (mu scale)) :
    (∀ kind scale, 0 < mu scale -> slope kind scale = beta kind scale) ↔
      (∀ kind scale, 0 < mu scale ->
        mu scale * deriv (flow.coupling kind) (mu scale) = flow.beta kind (mu scale)) := by
  constructor
  · intro encoded kind scale positive
    rw [← slopeReadout kind scale positive, ← betaReadout kind scale positive,
      encoded kind scale positive]
  · intro numerical kind scale positive
    apply faithful
    rw [slopeReadout kind scale positive, betaReadout kind scale positive]
    exact numerical kind scale positive

-- Restoring all three formerly duplicated numerical clauses changes
-- nothing about the reduced full RG contract.
example {Channel Scale Momentum Coupling Term Order Regime Fit : Type}
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) :
    f.pionInclusiveRGControlledCouplings ↔
      f.pionInclusiveRetainedBetaFunction .c0 ∧
      f.pionInclusiveRetainedBetaFunction .c2 ∧
      f.pionInclusiveRetainedBetaFunction .d2 ∧
      f.pionInclusiveRetainedFlow.PhysicalAt ∧
      (∃ scale, 0 < f.subtractionScaleValueAt scale) ∧
      (∀ scale, 0 < f.subtractionScaleValueAt scale ->
        ∀ᶠ mu in nhds (f.subtractionScaleValueAt scale),
          f.pionInclusiveRetainedFlow.RetainedBetaEquationsAt mu) ∧
      f.PionInclusiveRetainedFlowRepresentsAt := by
  constructor
  · intro controlled
    have sampled (kind : PionInclusiveContact) : f.pionInclusiveRetainedBetaFunction kind := by
      intro scale positive
      exact f.controlled_pion_running_retains_actual_weighted_equations
        controlled scale positive kind
    exact ⟨sampled .c0, sampled .c2, sampled .d2, controlled⟩
  · intro former
    exact former.2.2.2

-- A local, nonzero pion-inclusive jet. It is not asserted to solve the
-- retained equations away from mu=1 or to describe an observed nuclear fit.
private noncomputable def crossingJet : PionInclusiveRGFlow :=
  ⟨4 * Real.pi, 1, 1, fun mu => 2 + 6 * (mu - 1),
    fun mu => 2 + 8 * (mu - 1), fun mu => 2 * (mu - 1)⟩

private theorem crossingEquations : crossingJet.RetainedBetaEquationsAt 1 := by
  refine ⟨by norm_num, ?_⟩
  intro kind
  cases kind with
  | c0 =>
    convert (((hasDerivAt_id (1 : Real)).sub_const 1).const_mul 6).const_add 2 using 1 <;>
      norm_num [crossingJet, PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta, Real.pi_ne_zero]
  | c2 =>
    convert (((hasDerivAt_id (1 : Real)).sub_const 1).const_mul 8).const_add 2 using 1 <;>
      norm_num [crossingJet, PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta, Real.pi_ne_zero] <;>
      field_simp <;> ring
  | d2 =>
    convert ((hasDerivAt_id (1 : Real)).sub_const 1).const_mul 2 using 1 <;>
      norm_num [crossingJet, PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta, Real.pi_ne_zero] <;>
      field_simp <;> ring

-- Equal sampled coupling numbers need not identify their operator labels
-- or beta functions. An arbitrary label alias must not force 6=8.
example : crossingJet.RetainedBetaEquationsAt 1 ∧
    crossingJet.c0 1 = crossingJet.c2 1 ∧
    crossingJet.beta .c0 1 ≠ crossingJet.beta .c2 1 := by
  refine ⟨crossingEquations, ?_, ?_⟩
  · norm_num [crossingJet]
  · norm_num [crossingJet, PionInclusiveRGFlow.beta, Real.pi_ne_zero]
    field_simp
    norm_num

-- Noninjective readback cannot justify equality of arbitrary stored tags,
-- even though the physical numerical beta equation is satisfied.
example :
    let slope : Real × Bool := (deriv crossingJet.c0 1, true)
    let beta : Real × Bool := (crossingJet.beta .c0 1, false)
    slope.1 = beta.1 ∧ slope ≠ beta := by
  refine ⟨?_, ?_⟩
  · simpa [PionInclusiveRGFlow.coupling] using
      crossingJet.retained_derivatives_give_the_printed_weighted_equations 1 crossingEquations .c0
  · intro equality
    have tags := congrArg Prod.snd equality
    contradiction

example : ∀ (f : PionInclusiveRGFlow) (mu : Real), f.RetainedBetaEquationsAt mu →
    ({ f with c2 := fun _ => 0 } : PionInclusiveRGFlow).RetainedBetaEquationsAt mu :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.zero_derivative_contact_preserves_the_retained_rg_system

-- Zeroing C2 preserves an entire supplied RG trajectory, including the
-- actual C0 and D2 values. It does not require either of them to vanish.
example (f : PionInclusiveRGFlow) (equations : ∀ mu, 0 < mu → f.RetainedBetaEquationsAt mu) :
    let zeroC2 : PionInclusiveRGFlow := { f with c2 := fun _ => 0 }
    (∀ mu, 0 < mu → zeroC2.RetainedBetaEquationsAt mu) ∧
      (∀ mu, zeroC2.c0 mu = f.c0 mu ∧ zeroC2.d2 mu = f.d2 mu) ∧
      ¬(∃ left right, zeroC2.c2 left ≠ zeroC2.c2 right) := by
  refine ⟨fun mu positive => ?_, fun _ => ⟨rfl, rfl⟩, ?_⟩
  · exact f.zero_derivative_contact_preserves_the_retained_rg_system mu (equations mu positive)
  · simp

-- A globally realized retained-system boundary, not a nuclear-data fit:
-- positive mass and decay constant, nonzero axial coupling, constant D2.
example :
    let f : PionInclusiveRGFlow := ⟨4 * Real.pi, 1, 1, fun _ => 0, fun _ => 0, fun _ => 7⟩
    f.PhysicalAt ∧ f.axialCoupling ≠ 0 ∧
      (∀ mu, 0 < mu → f.RetainedBetaEquationsAt mu) ∧
      ¬(∃ contact left right, f.coupling contact left ≠ f.coupling contact right) := by
  refine ⟨⟨by positivity, by norm_num⟩, by norm_num, ?_, ?_⟩
  · intro mu positive
    refine ⟨positive, ?_⟩
    intro contact
    cases contact with
    | c0 => simpa [PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta] using
        hasDerivAt_const mu (0 : Real)
    | c2 => simpa [PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta] using
        hasDerivAt_const mu (0 : Real)
    | d2 => simpa [PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta] using
        hasDerivAt_const mu (7 : Real)
  · rintro ⟨contact, left, right, different⟩
    cases contact <;> exact different rfl

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.pionInclusiveRGControlledCouplings → f.SampledPionParameterVariation →
      (f.amplitudeScaleMatchingContext channel momentum).ParametersRun :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.sampled_pion_parameter_variation_realizes_rg_parameter_flow

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.pionScaleMomentum momentum → f.KSWMixedExpansionAt channel scale momentum →
      f.ExplicitPionSubleadingCalculation channel scale momentum →
      f.pionInclusiveRetainedBetaFunction .c0 ∧
      f.pionInclusiveRetainedBetaFunction .c2 ∧
      f.pionInclusiveRetainedBetaFunction .d2 :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.explicit_pions_expose_pion_inclusive_rg_equations

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.pionScaleMomentum momentum -> f.KSWMixedExpansionAt channel scale momentum ->
    f.ExplicitPionSubleadingCalculation channel scale momentum ->
    ∀ evaluationScale, 0 < f.subtractionScaleValueAt evaluationScale ->
    let mu := f.subtractionScaleValueAt evaluationScale
    ∀ kind, mu * deriv (f.pionInclusiveRetainedFlow.coupling kind) mu =
      f.pionInclusiveRetainedFlow.beta kind mu :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.explicit_pions_retain_the_actual_computed_order_beta_equations

-- Exact scale cancellation still needs no nonconstant-running witness.
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.fullAmplitudeScaleIndependent channel momentum :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_inclusive_rg_control_leaves_physical_amplitude_scale_independent

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.pionInclusiveRGControlledCouplings → f.SampledPionParameterVariation →
      f.fullAmplitudeScaleIndependent channel momentum →
      (f.toRenormalizedPredictionContext channel momentum).EstablishedRenormalizedPredictionAt
        (f.pionInclusiveRenormalizationModel channel momentum) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_inclusive_renormalization_realizes_shared_prediction

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.zero_derivative_contact_preserves_the_retained_rg_system
#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pion_inclusive_renormalization_realizes_shared_prediction