import PhysicsLogic.Papers.KaplanSavageWise1998 -- The removed label was unconstrained and unused. Its old payload can be -- restored without a new inhabitation premise; any retained claim ignores it. example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} (f : PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) : ∃ old : (PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) × Term, old.1 = f := ⟨(f, f.firstCorrection), rfl⟩ example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} (f : PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (left right : Term) (claim : PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit → Prop) : claim (f, left).1 ↔ claim (f, right).1 := Iff.rfl open PhysicsLogic.Papers.KaplanSavageWise1998 open Filter open scoped Topology set_option backward.isDefEq.respectTransparency false -- Only the physical-family input and the separately imported full-amplitude -- invariance remain. No beta, solution or nonconstant-running output is supplied. 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.PionlessRGCalculation channel scale momentum ↔ (f.pdsAmplitudeObtained channel scale momentum -> f.effectiveRangeDataMatched channel -> f.physicalAmplitudeRequiredScaleIndependent channel momentum -> f.PionlessObservableMatchingAt channel ∧ f.pionlessAmplitudeScaleIndependent channel momentum) := Iff.rfl -- Pionless scale independence is about the same concrete amplitude, not -- about the separately retained pion-inclusive family or a physical label. 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.pionlessAmplitudeScaleIndependent channel momentum = (∀ left right, f.pionlessPDSFormulaReadout.pdsAmplitudeValueAt channel left momentum = f.pionlessPDSFormulaReadout.pdsAmplitudeValueAt channel right momentum) := rfl example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (reference : Scale) (momentum : Momentum) : f.pionlessAmplitudeScaleIndependent channel momentum ↔ (∀ scale, f.pionlessPDSFormulaReadout.pdsAmplitudeValueAt channel scale momentum = f.pionlessPDSFormulaReadout.pdsAmplitudeValueAt channel reference momentum) := by constructor · intro h scale exact h scale reference · intro h left right exact (h left).trans (h right).symm example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (other : Channel -> Scale -> Momentum -> f.AmplitudeValue) (channel : Channel) (momentum : Momentum) : {f with fullAmplitudeValueAt := other}.pionlessAmplitudeScaleIndependent channel momentum = f.pionlessAmplitudeScaleIndependent channel momentum := rfl -- A one-point sampling type cannot exhibit nonconstant running, even when -- the genuine continuous solution and both beta equations have been derived. example {Channel Momentum Coupling Term Order Regime Fit : Type} (f : NuclearScatteringFramework Channel Unit Momentum Coupling Term Order Regime Fit) (channel : Channel) (matching : f.effectiveRangeDataMatched channel) (families : f.PionlessObservableMatchingAt channel) : (∀ mu, (f.pionlessRGFlow channel).NonpoleAt mu -> (f.pionlessRGFlow channel).ExactBetaDerivativesAt mu) ∧ f.equationElevenPionlessRunningValuesAt channel ∧ ¬(∃ left right : Unit, f.pionlessCouplingValueAt channel f.c2 (f.subtractionScaleValueAt left) ≠ f.pionlessCouplingValueAt channel f.c2 (f.subtractionScaleValueAt right)) := by have values := f.observable_matching_derives_running_values channel matching families refine ⟨f.equation_eleven_values_derive_real_beta_equations channel values, values, ?_⟩ rintro ⟨left, right, different⟩ exact different (congrArg (fun s => f.pionlessCouplingValueAt channel f.c2 (f.subtractionScaleValueAt s)) (Subsingleton.elim left right)) -- Samples are evaluations, not a second coupling family needing a matching -- assumption. The all-real nonpole domain is not weakened to sampled scales. -- The paper adapter still has precisely its former finite-a physical domain. example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) : f.equationElevenPionlessRunningValuesAt channel ↔ (0 < f.nucleonMassValue ∧ f.scatteringLength channel ≠ 0) ∧ ∀ mu, -mu + (f.scatteringLength channel)⁻¹ ≠ 0 -> f.pionlessCouplingValueAt channel f.c0 mu = (4 * Real.pi / f.nucleonMassValue) * (-mu + (f.scatteringLength channel)⁻¹)⁻¹ ∧ f.pionlessCouplingValueAt channel f.c2 mu = (2 * Real.pi / f.nucleonMassValue) * (-mu + (f.scatteringLength channel)⁻¹)⁻¹ ^ 2 * f.effectiveRange channel := by simp only [NuclearScatteringFramework.equationElevenPionlessRunningValuesAt, PionlessRGFlow.EquationElevenAt, PionlessRGFlow.PhysicalAt, PionlessRGFlow.NonpoleAt, PionlessRGFlow.c0Solution, PionlessRGFlow.c2Solution, NuclearScatteringFramework.pionlessRGFlow] tauto 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.equationElevenPionlessRunningValuesAt channel = (f.scatteringLength channel ≠ 0 ∧ (f.pionlessRGFlow channel).EquationElevenAt) ∧ (f.pionlessContactExpansionReadoutAt channel scale momentum).leadingCoupling = f.pionlessCouplingValueAt channel f.c0 (f.subtractionScaleValueAt scale) ∧ (f.pionlessContactExpansionReadoutAt channel scale momentum).derivativeCoupling = f.pionlessCouplingValueAt channel f.c2 (f.subtractionScaleValueAt scale) := ⟨rfl, rfl, rfl⟩ example {Channel Scale Momentum Coupling Term Order Regime Fit : Type} (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (samples : Coupling -> Scale -> f.CouplingValue) (channel : Channel) (scale : Scale) (momentum : Momentum) : ({f with pionInclusiveCouplingValueAt := samples}.PionlessObservableMatchingAt channel = f.PionlessObservableMatchingAt channel) ∧ ({f with pionInclusiveCouplingValueAt := samples}.pionlessContactExpansionReadoutAt channel scale momentum = f.pionlessContactExpansionReadoutAt channel scale momentum) := ⟨rfl, rfl⟩ -- Regression for the former shared field: equating the two theories on a -- positive scale neighborhood is incompatible with their different betas. -- Independent source routes are not contradictory; their identification is. example {Channel Momentum Coupling Term Order Regime Fit : Type} (f : NuclearScatteringFramework Channel Real Momentum Coupling Term Order Regime Fit) (channel : Channel) (scales : f.subtractionScaleValueAt = id) (length : f.scatteringLength channel = -1) (values : f.equationElevenPionlessRunningValuesAt channel) (pions : f.pionInclusiveRGControlledCouplings) (axial : f.pionInclusiveRetainedFlow.axialCoupling ≠ 0) (shared : ∀ t, 0 < t -> f.couplingValueAsReal (f.pionInclusiveCouplingValueAt f.c0 t) = f.pionlessCouplingValueAt channel f.c0 t) : False := by have nonpole (t : Real) (ht : 0 < t) : (f.pionlessRGFlow channel).NonpoleAt t := by simp only [PionlessRGFlow.NonpoleAt, NuclearScatteringFramework.pionlessRGFlow, length, inv_neg, inv_one] linarith have same (t : Real) (ht : 0 < t) : f.pionInclusiveRetainedFlow.c0 t = (f.pionlessRGFlow channel).c0 t := by have hp := f.controlled_pion_running_identifies_sampled_values pions .c0 t (by simpa [scales]) simpa [scales, NuclearScatteringFramework.pionInclusiveContact, NuclearScatteringFramework.pionlessRGFlow, PionInclusiveRGFlow.coupling] using hp.symm.trans (shared t ht) have nearby : f.pionInclusiveRetainedFlow.c0 =ᶠ[𝓝 (1 : Real)] (f.pionlessRGFlow channel).c0 := by filter_upwards [lt_mem_nhds (by norm_num : (0 : Real) < 1)] with t ht exact same t ht have pl := (f.equation_eleven_values_derive_real_beta_equations channel values 1 (nonpole 1 (by norm_num))).1 have pi := f.controlled_pion_running_retains_actual_weighted_equations pions 1 (by simp [scales]) .c0 simp only [scales, id_eq] at pi have mass : f.pionInclusiveRetainedFlow.mass = f.nucleonMassValue := rfl have nonzero : f.pionInclusiveRetainedFlow.c0 1 ≠ 0 := by rw [same 1 (by norm_num), (values.2.2 1 (nonpole 1 (by norm_num))).1] simp only [PionlessRGFlow.c0Solution, NuclearScatteringFramework.pionlessRGFlow, length, inv_neg, inv_one] exact mul_ne_zero (div_ne_zero (mul_ne_zero (by norm_num) Real.pi_ne_zero) (ne_of_gt values.2.1)) (inv_ne_zero (by norm_num)) apply f.pionInclusiveRetainedFlow.the_c0_pion_correction_is_not_the_pionless_beta 1 pions.1 (by norm_num) axial nonzero rw [← pi] change 1 * deriv f.pionInclusiveRetainedFlow.c0 1 = _ rw [(pl.congr_of_eventuallyEq nearby).deriv, same 1 (by norm_num), mass] simp [NuclearScatteringFramework.pionlessRGFlow] -- Both actual derivative laws are realizable with the same mass and the -- same C0 value at one scale. Equality at one point is not equality of flows. -- The former channel-independent field forced this sharing at every scale. -- Even at one common nonpole scale it identifies both matching parameters. private theorem shared_contacts_force_equal_matching_data (left right : PionlessRGFlow) (mu : Real) (leftValues : left.EquationElevenAt) (rightValues : right.EquationElevenAt) (leftNonpole : left.NonpoleAt mu) (rightNonpole : right.NonpoleAt mu) (mass : left.mass = right.mass) (c0 : left.c0 mu = right.c0 mu) (c2 : left.c2 mu = right.c2 mu) : left.inverseScatteringLength = right.inverseScatteringLength ∧ left.effectiveRange = right.effectiveRange := by let g0 := left.mass / (4 * Real.pi) * left.c0 mu let g2 := left.mass / (4 * Real.pi) * left.c2 mu have first := (left.equation_eleven_iff_first_two_matching_equations.mp leftValues).2 mu leftNonpole have second : (-mu + right.inverseScatteringLength) * g0 = 1 ∧ (-mu + right.inverseScatteringLength) * g2 = (right.effectiveRange / 2) * g0 := by simpa only [←mass, ←c0, ←c2] using (right.equation_eleven_iff_first_two_matching_equations.mp rightValues).2 mu rightNonpole have nonzero : g0 ≠ 0 := by intro zero have one : (-mu + left.inverseScatteringLength) * g0 = 1 := first.1 rw [zero, mul_zero] at one norm_num at one have inverse : left.inverseScatteringLength = right.inverseScatteringLength := by have := mul_right_cancel₀ nonzero (first.1.trans second.1.symm) linarith refine ⟨inverse, ?_⟩ rw [←inverse] at second have := mul_right_cancel₀ nonzero (first.2.symm.trans second.2) linarith private noncomputable def channelExample (channel : Bool) : PionlessRGFlow := let alpha : Real := if channel then 1 else -1 let range : Real := if channel then 4 else 2 ⟨4 * Real.pi, alpha, range, fun mu => (-mu + alpha)⁻¹, fun mu => (range / 2) * (-mu + alpha)⁻¹ ^ 2⟩ -- Two channels, one mass and one subtraction scale, with different finite -- scattering lengths and ranges. These are algebraic model data, not fits. example : (∀ channel, (channelExample channel).EquationElevenAt) ∧ (channelExample false).mass = (channelExample true).mass ∧ (channelExample false).NonpoleAt 2 ∧ (channelExample true).NonpoleAt 2 ∧ (channelExample false).c0 2 = -1 / 3 ∧ (channelExample true).c0 2 = -1 ∧ (channelExample false).c2 2 = 1 / 9 ∧ (channelExample true).c2 2 = 2 ∧ ¬((channelExample false).c0 2 = (channelExample true).c0 2 ∧ (channelExample false).c2 2 = (channelExample true).c2 2) := by have values : ∀ channel, (channelExample channel).EquationElevenAt := by intro channel refine ⟨by dsimp [PionlessRGFlow.PhysicalAt, channelExample]; positivity, ?_⟩ intro mu _ cases channel <;> simp [channelExample, PionlessRGFlow.c0Solution, PionlessRGFlow.c2Solution, Real.pi_ne_zero] <;> field_simp <;> ring refine ⟨values, rfl, by norm_num [channelExample, PionlessRGFlow.NonpoleAt], by norm_num [channelExample, PionlessRGFlow.NonpoleAt], by norm_num [channelExample], by norm_num [channelExample], by norm_num [channelExample], by norm_num [channelExample], ?_⟩ rintro ⟨leading, derivative⟩ have equality := shared_contacts_force_equal_matching_data _ _ 2 (values false) (values true) (by norm_num [channelExample, PionlessRGFlow.NonpoleAt]) (by norm_num [channelExample, PionlessRGFlow.NonpoleAt]) rfl leading derivative norm_num [channelExample] at equality private noncomputable def pionlessExample : PionlessRGFlow := ⟨4 * Real.pi, -1, 0, fun mu => (-mu - 1)⁻¹, fun _ => 0⟩ private noncomputable def pionExample : PionInclusiveRGFlow := ⟨4 * Real.pi, 1, 1, fun mu => -1 / 2 - (mu - 1) / 4, fun _ => 0, fun mu => (mu - 1) / 8⟩ example : pionlessExample.EquationElevenAt ∧ pionExample.PhysicalAt ∧ pionExample.RetainedBetaEquationsAt 1 ∧ pionlessExample.c0 1 = pionExample.c0 1 ∧ deriv pionlessExample.c0 1 ≠ deriv pionExample.c0 1 := by have solution : pionlessExample.EquationElevenAt := by refine ⟨by dsimp [PionlessRGFlow.PhysicalAt, pionlessExample]; positivity, ?_⟩ intro mu _ simp [pionlessExample, PionlessRGFlow.c0Solution, PionlessRGFlow.c2Solution, Real.pi_ne_zero, sub_eq_add_neg] have pi : pionExample.RetainedBetaEquationsAt 1 := by refine ⟨by norm_num, ?_⟩ intro kind have linear := ((hasDerivAt_id (1 : Real)).sub_const 1).div_const 4 have eighth := ((hasDerivAt_id (1 : Real)).sub_const 1).div_const 8 cases kind <;> dsimp [pionExample, PionInclusiveRGFlow.coupling, PionInclusiveRGFlow.beta] · convert linear.const_sub (-1 / 2) using 1 <;> norm_num · convert hasDerivAt_const (1 : Real) (0 : Real) using 1 <;> norm_num · convert eighth using 1 <;> norm_num <;> field_simp <;> ring refine ⟨solution, ⟨by dsimp [pionExample]; positivity, by norm_num [pionExample]⟩, pi, by norm_num [pionlessExample, pionExample], ?_⟩ have pl := (pionlessExample.equation_eleven_derives_actual_beta_derivatives solution 1 (by norm_num [PionlessRGFlow.NonpoleAt, pionlessExample])).1.deriv have pd := (pi.2 .c0).deriv change deriv pionExample.c0 1 = _ at pd rw [pl, pd] norm_num [pionlessExample, pionExample, PionInclusiveRGFlow.beta]