import PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJetCalculus set_option autoImplicit false open PhysicsLogic.Papers.KaplanSavageWise1998 open scoped ComplexConjugate example (a p c u : Real) (regular : 1 + (c : Complex) * a * ((u : Complex) + Complex.I * p) ≠ 0) : 1 + 2 * Complex.I * a * p * (-(c : Complex) / (1 + (c : Complex) * a * ((u : Complex) + Complex.I * p))) = conj (1 + (c : Complex) * a * ((u : Complex) + Complex.I * p)) / (1 + (c : Complex) * a * ((u : Complex) + Complex.I * p)) := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJetCalculus.leading_s_matrix_is_conjugate_ratio a p c u regular example (M p : Real) (a b : Complex × Complex) (mass : M ≠ 0) (momentum : p ≠ 0) (regular : (PionAmplitudeJet.retainedScatteringReadout M p a).1 ≠ 0) : PionAmplitudeJet.retainedScatteringReadout M p a = PionAmplitudeJet.retainedScatteringReadout M p b ↔ a = b := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.retained_scattering_readout_eq_iff M p a b mass momentum regular example (j : PionAmplitudeJet) (m p mu : Real) (momentum : 0 < p) : Complex.normSq (PionAmplitudeJet.retainedScatteringReadout j.couplings.mass p (j.leadingCoefficient p mu, j.firstCoefficient m p mu)).1 = 1 := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.retained_scattering_readout_has_unitary_leading_value j m p mu momentum -- These are boundaries of the algebraic readout, not evaluations of the -- printed pion graphs at a physical threshold or an inelastic extension. example : ((0, 0) : Complex × Complex) ≠ (1, 1) ∧ PionAmplitudeJet.retainedScatteringReadout 0 1 (0, 0) = PionAmplitudeJet.retainedScatteringReadout 0 1 (1, 1) ∧ PionAmplitudeJet.retainedScatteringReadout 1 0 (0, 0) = PionAmplitudeJet.retainedScatteringReadout 1 0 (1, 1) := by norm_num [PionAmplitudeJet.retainedScatteringReadout] example : ((Complex.I / 2, 0) : Complex × Complex) ≠ (Complex.I / 2, 1) ∧ (PionAmplitudeJet.retainedScatteringReadout (4 * Real.pi) 1 (Complex.I / 2, 0)).1 = 0 ∧ PionAmplitudeJet.retainedScatteringReadout (4 * Real.pi) 1 (Complex.I / 2, 0) = PionAmplitudeJet.retainedScatteringReadout (4 * Real.pi) 1 (Complex.I / 2, 1) := by have zero : 1 + 2 * Complex.I * (Complex.I / 2) = 0 := by calc 1 + 2 * Complex.I * (Complex.I / 2) = 1 + Complex.I ^ 2 := by ring _ = 0 := by simp norm_num [PionAmplitudeJet.retainedScatteringReadout, Real.pi_ne_zero, zero] example (j : PionAmplitudeJet) (m p mu s d s' d' : Real) : (j.withSubleadingContacts s d).firstCoefficient m p mu - (j.withSubleadingContacts s' d').firstCoefficient m p mu = -((s + d * m ^ 2 - (s' + d' * m ^ 2) : Real) : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.subleading_contact_prediction_difference j m p mu s d s' d' example (j : PionAmplitudeJet) (m p mu s d s' d' : Real) : 0 < p -> ((j.withSubleadingContacts s d).firstCoefficient m p mu = (j.withSubleadingContacts s' d').firstCoefficient m p mu ↔ s + d * m ^ 2 = s' + d' * m ^ 2) := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.subleading_contact_prediction_eq_iff_combination_eq j m p mu s d s' d' example (j : PionAmplitudeJet) (m p mu : Real) : (j.withSubleadingContacts (j.firstC0 mu) (j.couplings.d2 mu)).firstCoefficient m p mu = j.firstCoefficient m p mu := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.evaluating_current_subleading_contacts_preserves_prediction j m p mu example (j : PionAmplitudeJet) (m p : Real) (scales : Set Real) : j.AdmissibleOn m p scales ↔ j.couplings.PhysicalAt ∧ 0 < m ∧ 0 < p ∧ ∀ mu ∈ scales, 0 < mu ∧ j.couplings.pionDiagramDenominator mu p ≠ 0 := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.admissible_on_iff_regular_domain j m p scales example (j : PionAmplitudeJet) (m p : Real) (scales : Set Real) : j.AdmissibleOn m p scales -> IsOpen scales -> IsPreconnected scales -> (∀ mu ∈ scales, j.RunsAt mu) -> ∀ mu : Real, mu ∈ scales -> j.couplings.axialCoupling ≠ 0 -> j.couplings.c0 mu ≠ 0 -> (∀ left ∈ scales, ∀ right ∈ scales, j.leadingCoefficient p left = j.leadingCoefficient p right ∧ j.firstCoefficient m p left = j.firstCoefficient m p right) ∧ (∃ other ∈ scales, j.withoutMassInsertion.firstCoefficient m p other ≠ j.withoutMassInsertion.firstCoefficient m p mu) := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.retained_rg_cancellation_requires_the_mass_insertion j m p scales example (j : PionAmplitudeJet) (m p : Real) (scales : Set Real) : j.AdmissibleOn m p scales -> IsOpen scales -> IsPreconnected scales -> (∀ mu ∈ scales, j.RunsAt mu) -> ∀ left right : Real, left ∈ scales -> right ∈ scales -> j.leadingCoefficient p left = j.leadingCoefficient p right ∧ j.firstCoefficient m p left = j.firstCoefficient m p right := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.coefficients_agree_on_connected_scales j m p scales example (j : PionAmplitudeJet) (m p : Real) (scales : Set Real) : j.AdmissibleOn m p scales -> IsOpen scales -> ∀ mu : Real, mu ∈ scales -> j.RunsAt mu -> j.couplings.axialCoupling ≠ 0 -> j.couplings.c0 mu ≠ 0 -> ∃ other ∈ scales, j.withoutMassInsertion.firstCoefficient m p other ≠ j.withoutMassInsertion.firstCoefficient m p mu := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.mass_insertion_omission_changes_a_retained_prediction j m p scales example (j : PionAmplitudeJet) (p mu : Real) : j.withoutMassInsertion.leadingCoefficient p mu = j.leadingCoefficient p mu := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.removing_the_mass_insertion_preserves_the_leading_coefficient j p mu example (j : PionAmplitudeJet) (m p mu : Real) : 0 < m -> 0 < p -> 0 < mu -> (j.firstPhaseIncrement m p mu).im = 0 := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.first_phase_increment_is_real j m p mu example (j : PionAmplitudeJet) (shift : Real -> Real) (m0 m p mu : Real) : 0 < m -> 0 < mu -> ({ couplings := { j.couplings with d2 := fun v => j.couplings.d2 v + shift v } firstC0 := fun v => j.firstC0 v - shift v * m0 ^ 2 } : PionAmplitudeJet).firstCoefficient m p mu = j.firstCoefficient m p mu - ((shift mu * (m ^ 2 - m0 ^ 2) : Real) : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.mass_reparametrization_changes_the_prediction_by_the_mass_difference j shift m0 m p mu example (m p : Real) (massive : 0 < m) (momentum : 0 < p) : let j := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.Diagnostics.unitaryJet (∀ left > 0, ∀ right > 0, j.leadingCoefficient p left = j.leadingCoefficient p right ∧ j.firstCoefficient m p left = j.firstCoefficient m p right) ∧ (∃ other > 0, j.withoutMassInsertion.firstCoefficient m p other ≠ j.withoutMassInsertion.firstCoefficient m p 1) := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.Diagnostics.the_actual_model_needs_the_mass_insertion m p massive momentum -- The required insertion can vanish at one scale without being absent in the RG family. example (m p : Real) (massive : 0 < m) (momentum : 0 < p) : let j := PionAmplitudeJet.Diagnostics.unitaryJet j.couplings.d2 1 = 0 ∧ j.firstCoefficient m p 1 = j.withoutMassInsertion.firstCoefficient m p 1 ∧ ∃ mu > 0, j.firstCoefficient m p mu ≠ j.withoutMassInsertion.firstCoefficient m p mu := by dsimp only have atOne : PionAmplitudeJet.Diagnostics.unitaryJet.firstCoefficient m p 1 = PionAmplitudeJet.Diagnostics.unitaryJet.withoutMassInsertion.firstCoefficient m p 1 := by simp [PionAmplitudeJet.firstCoefficient, PionAmplitudeJet.withoutMassInsertion, PionAmplitudeJet.Diagnostics.unitaryJet, PionAmplitudeJetCalculus.Diagnostic.unitaryLeadingFlow, PionAmplitudeJet.graphII, PionAmplitudeJet.graphIII, PionAmplitudeJet.leadingCoefficient, PionInclusiveRGFlow.pionDiagramDenominator, PionInclusiveRGFlow.pionDiagramLeadingAmplitude, PionInclusiveRGFlow.twoLoopPionAmplitude, PionInclusiveRGFlow.pionLogPrefactor, PionInclusiveRGFlow.dressedMassInsertion] have argument := PionAmplitudeJet.Diagnostics.the_actual_model_needs_the_mass_insertion m p massive momentum obtain ⟨mu, positive, different⟩ := argument.2 refine ⟨by simp [PionAmplitudeJet.Diagnostics.unitaryJet, PionAmplitudeJetCalculus.Diagnostic.unitaryLeadingFlow], atOne, mu, positive, ?_⟩ intro equal exact different (equal.symm.trans ((argument.1 mu positive 1 (by norm_num)).2.trans atOne)) example (j : PionAmplitudeJet) (m p mu : Real) : 0 < m -> 0 < mu -> let absorbed : PionAmplitudeJet := { couplings := { j.couplings with d2 := fun _ => 0 } firstC0 := fun v => j.firstC0 v + j.couplings.d2 v * m ^ 2 } absorbed.leadingCoefficient p mu = j.leadingCoefficient p mu ∧ absorbed.firstCoefficient m p mu = j.firstCoefficient m p mu := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.absorbing_the_mass_insertion_preserves_the_fixed_mass_prediction j m p mu example (j : PionAmplitudeJet) (m mu : Real) : j.RunsAt mu -> HasDerivAt (fun v => j.firstC0 v + j.couplings.d2 v * m ^ 2) (2 * (j.couplings.mass / (4 * Real.pi)) * j.couplings.c0 mu * (j.firstC0 mu + j.couplings.d2 mu * m ^ 2) + (j.couplings.mass / (4 * Real.pi)) * j.couplings.c0 mu * (j.couplings.axialCoupling ^ 2 / j.couplings.pionDecayConstant ^ 2) + j.couplings.pionLogCountertermSlope mu / mu * m ^ 2) mu := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.absorbed_contact_running_contains_the_mass_source j m mu example (j : PionAmplitudeJet) (mu p m1 m2 : Real) : j.couplings.PhysicalAt -> 0 < p -> j.couplings.axialCoupling ≠ 0 -> j.couplings.c0 mu ≠ 0 -> 0 < m1 -> m1 < m2 -> ¬∃ a b : Real, j.couplings.pionLogPrefactor m1 mu p = ((a + b * p ^ 2 : Real) : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 ∧ j.couplings.pionLogPrefactor m2 mu p = ((a + b * p ^ 2 : Real) : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.mass_independent_contacts_do_not_cancel_the_pion_log_at_two_masses j mu p m1 m2 -- One mass can be matched: the same a is not asserted to work at other masses. example (j : PionAmplitudeJet) (mu p m : Real) : ∃ a b : Real, j.couplings.pionLogPrefactor m mu p = ((a + b * p ^ 2 : Real) : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 := by refine ⟨m ^ 2 * j.couplings.pionLogCountertermSlope mu, 0, ?_⟩ simpa using j.couplings.pion_log_prefactor_is_dressed_mass_slope m mu p -- Without the axial coupling there is no logarithmic source to obstruct. example (f : PionInclusiveRGFlow) (mu p m1 m2 : Real) : let noPions := { f with axialCoupling := 0 } ∃ a b : Real, noPions.pionLogPrefactor m1 mu p = ((a + b * p ^ 2 : Real) : Complex) / noPions.pionDiagramDenominator mu p ^ 2 ∧ noPions.pionLogPrefactor m2 mu p = ((a + b * p ^ 2 : Real) : Complex) / noPions.pionDiagramDenominator mu p ^ 2 := by refine ⟨0, 0, ?_⟩ simp [PionInclusiveRGFlow.pionLogPrefactor] -- The interacting model can have the mass insertion absorbed at one mass -- and still have scale-independent predictions. This changes s, unlike omission. example (m p : Real) (massive : 0 < m) (momentum : 0 < p) : let j := PionAmplitudeJet.Diagnostics.unitaryJet let absorbed : PionAmplitudeJet := { couplings := { j.couplings with d2 := fun _ => 0 } firstC0 := fun v => j.firstC0 v + j.couplings.d2 v * m ^ 2 } absorbed.couplings.d2 = (fun _ => 0) ∧ ∀ left > 0, ∀ right > 0, absorbed.firstCoefficient m p left = absorbed.firstCoefficient m p right := by refine ⟨rfl, ?_⟩ intro left leftPositive right rightPositive have leftEq := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.absorbing_the_mass_insertion_preserves_the_fixed_mass_prediction PionAmplitudeJet.Diagnostics.unitaryJet m p left massive leftPositive have rightEq := PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.absorbing_the_mass_insertion_preserves_the_fixed_mass_prediction PionAmplitudeJet.Diagnostics.unitaryJet m p right massive rightPositive have same := (PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.Diagnostics.the_actual_model_needs_the_mass_insertion m p massive momentum).1 left leftPositive right rightPositive exact leftEq.2.trans (same.2.trans rightEq.2.symm) #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.coefficients_agree_on_connected_scales #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.retained_rg_cancellation_requires_the_mass_insertion #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.mass_insertion_omission_changes_a_retained_prediction #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.first_phase_increment_is_real #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.Diagnostics.the_actual_model_needs_the_mass_insertion #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.absorbing_the_mass_insertion_preserves_the_fixed_mass_prediction #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.absorbed_contact_running_contains_the_mass_source #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.retained_scattering_readout_eq_iff #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.retained_scattering_readout_has_unitary_leading_value #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet.mass_independent_contacts_do_not_cancel_the_pion_log_at_two_masses