import PhysicsLogic.Papers.KaplanSavageWise1998 set_option autoImplicit false set_option backward.isDefEq.respectTransparency false open Filter PhysicsLogic.Papers.KaplanSavageWise1998 open scoped Topology universe uC uS uP uK uT uO uR uF variable {Channel : Type uC} {Scale : Type uS} {Momentum : Type uP} {Coupling : Type uK} {Term : Type uT} {Order : Type uO} {Regime : Type uR} {Fit : Type uF} example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (scale : Scale) (momentum : Momentum), framework.scaleComparableToMomentum scale momentum ↔ 1 <= framework.pionlessScaleComparisonFactor ∧ 0 < framework.momentumValue momentum ∧ 1 / framework.pionlessScaleComparisonFactor <= framework.subtractionScaleValueAt scale / framework.momentumValue momentum ∧ framework.subtractionScaleValueAt scale / framework.momentumValue momentum <= framework.pionlessScaleComparisonFactor := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.scale_comparison_iff_fixed_ratio_bounds example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (scale : Scale) (momentum : Momentum), framework.scaleComparableToMomentum scale momentum -> ¬framework.minimalSubtractionAt scale := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.scale_comparison_excludes_minimal_subtraction example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (remainder : Momentum -> Real), (∀ momentum, framework.lowMomentumEffectiveRangeExpansionAt channel momentum -> framework.momentumTimesPhaseShiftCotangentValueAt channel momentum = -(framework.scatteringLength channel)⁻¹ + framework.effectiveRange channel / 2 * framework.momentumValue momentum ^ 2 + remainder momentum) -> (framework.effectiveRangeDataMatched channel ↔ framework.scatteringLength channel ≠ 0 ∧ (∃ sample : Real -> Momentum, ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumValue (sample p) = p ∧ framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) ∧ ∀ tolerance : Real, 0 < tolerance -> ∃ radius : Real, 0 < radius ∧ ∀ momentum, framework.lowMomentumEffectiveRangeExpansionAt channel momentum -> 0 < framework.momentumValue momentum -> framework.momentumValue momentum < radius -> |remainder momentum / framework.momentumValue momentum ^ 2| < tolerance) := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.effective_range_matching_iff_uniform_remainder example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel), framework.effectiveRangeDataMatched channel -> ∀ sample : Real -> Momentum, (∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumValue (sample p) = p ∧ framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients (fun p => framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p)) (-(framework.scatteringLength channel)⁻¹) (framework.effectiveRange channel / 2) := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.effective_range_matching_identifies_observable_coefficients example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel), framework.effectiveRangeDataMatched channel -> ∀ sample : Real -> Momentum, (∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumValue (sample p) = p ∧ framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) -> Tendsto (fun p => framework.effectiveRangeExpansionRemainderAt channel (sample p) / p ^ 2) PhysicsLogic.Framework.EffectiveRangeExpansion.approach (nhds 0) := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.effective_range_matching_controls_sampled_remainder -- The complete former contact contract, including both removed clauses, -- is recovered under the same ERE input used by the source deductions. example (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (matching : framework.effectiveRangeDataMatched channel) : framework.PionlessObservableMatchingAt channel ↔ (((framework.pionlessRGFlow channel).PhysicalAt ∧ framework.scatteringLength channel ≠ 0) ∧ ∃ sample : Real -> Momentum, (∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumValue (sample p) = p ∧ framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) ∧ (∀ mu, (framework.pionlessRGFlow channel).NonpoleAt mu -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients (fun p => -1 / (framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p) + mu)) (framework.nucleonMassValue / (4 * Real.pi) * framework.pionlessCouplingValueAt channel framework.c0 mu) (framework.nucleonMassValue / (4 * Real.pi) * framework.pionlessCouplingValueAt channel framework.c2 mu) ∧ ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p) + mu ≠ 0) ∧ (∀ scale, (framework.pionlessRGFlow channel).NonpoleAt (framework.subtractionScaleValueAt scale) -> ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, -1 / (framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p) + framework.subtractionScaleValueAt scale) = framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale (sample p))) := by constructor · rintro ⟨physical, sample, domain, couplings, readout⟩ have observable := framework.effective_range_matching_identifies_observable_coefficients channel matching sample domain refine ⟨⟨physical, matching.1⟩, sample, domain, ?_, readout⟩ intro mu nonpole refine ⟨couplings mu nonpole, ?_⟩ have limitNonzero : -(framework.scatteringLength channel)⁻¹ + mu ≠ 0 := by change -mu + (framework.scatteringLength channel)⁻¹ ≠ 0 at nonpole intro zero apply nonpole linarith exact (observable.constant_limit.add_const mu).eventually_ne limitNonzero · rintro ⟨physical, sample, domain, couplings, readout⟩ exact ⟨physical.1, sample, domain, fun mu nonpole => (couplings mu nonpole).1, readout⟩ -- Contact-family elimination is exact under physical ERE matching, which -- supplies the finite-length domain and the eventually nonzero denominator. example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (_matching : framework.effectiveRangeDataMatched channel), framework.PionlessObservableMatchingAt channel ↔ (((framework.pionlessRGFlow channel).PhysicalAt ∧ framework.scatteringLength channel ≠ 0) ∧ ∃ sample : Real -> Momentum, ∃ contact : Real -> Real -> Real, (∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumValue (sample p) = p ∧ framework.lowMomentumEffectiveRangeExpansionAt channel (sample p)) ∧ (∀ mu, (framework.pionlessRGFlow channel).NonpoleAt mu -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients (contact mu) (framework.nucleonMassValue / (4 * Real.pi) * framework.pionlessCouplingValueAt channel framework.c0 mu) (framework.nucleonMassValue / (4 * Real.pi) * framework.pionlessCouplingValueAt channel framework.c2 mu) ∧ ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, (framework.momentumTimesPhaseShiftCotangentValueAt channel (sample p) + mu) * contact mu p = -1) ∧ (∀ scale, (framework.pionlessRGFlow channel).NonpoleAt (framework.subtractionScaleValueAt scale) -> ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, contact (framework.subtractionScaleValueAt scale) p = framework.pionlessPDSFormulaReadout.scaledContactValueAt channel scale (sample p))) := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pionless_observable_matching_iff_contact_family #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pionless_observable_matching_iff_contact_family example : ∀ (flow : PionlessRGFlow) (phase : Real -> Real) (contact : Real -> Real -> Real), flow.PhysicalAt -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients phase (-flow.inverseScatteringLength) (flow.effectiveRange / 2) -> (∀ mu, flow.NonpoleAt mu -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients (contact mu) (flow.mass / (4 * Real.pi) * flow.c0 mu) (flow.mass / (4 * Real.pi) * flow.c2 mu)) -> (∀ mu, flow.NonpoleAt mu -> ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, (phase p + mu) * contact mu p = -1) -> flow.EquationElevenAt := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_family_derives_equation_eleven example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel), framework.effectiveRangeDataMatched channel -> framework.PionlessObservableMatchingAt channel -> framework.equationElevenPionlessRunningValuesAt channel := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.observable_matching_derives_running_values example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (scale : Scale) (momentum : Momentum), framework.pdsAmplitudeObtained channel scale momentum -> framework.effectiveRangeDataMatched channel -> framework.physicalAmplitudeRequiredScaleIndependent channel momentum -> framework.PionlessRGCalculation channel scale momentum -> (∀ mu, (framework.pionlessRGFlow channel).NonpoleAt mu -> (framework.pionlessRGFlow channel).ExactBetaDerivativesAt mu) ∧ framework.equationElevenPionlessRunningValuesAt channel ∧ framework.pionlessAmplitudeScaleIndependent channel momentum := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.scale_independence_yields_running_couplings_and_rg_equations -- The revised source calculation still yields the actual ordinary beta -- derivatives, including mu=0 when it is not the contact pole. example (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (scale : Scale) (momentum : Momentum) (amplitude : framework.pdsAmplitudeObtained channel scale momentum) (matching : framework.effectiveRangeDataMatched channel) (independence : framework.physicalAmplitudeRequiredScaleIndependent channel momentum) (calculation : framework.PionlessRGCalculation channel scale momentum) (mu : Real) (nonpole : (framework.pionlessRGFlow channel).NonpoleAt mu) : HasDerivAt (framework.pionlessRGFlow channel).c0 (framework.nucleonMassValue / (4 * Real.pi) * (framework.pionlessRGFlow channel).c0 mu ^ 2) mu ∧ HasDerivAt (framework.pionlessRGFlow channel).c2 (framework.nucleonMassValue / (2 * Real.pi) * (framework.pionlessRGFlow channel).c0 mu * (framework.pionlessRGFlow channel).c2 mu) mu := by have result := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.scale_independence_yields_running_couplings_and_rg_equations framework channel scale momentum amplitude matching independence calculation exact result.1 mu nonpole -- The original displayed beta and running-solution outputs now refer to -- real derivatives and real functions on their nonpole domain. example : ∀ (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (scale : Scale) (momentum : Momentum), framework.pdsAmplitudeObtained channel scale momentum -> framework.effectiveRangeDataMatched channel -> framework.physicalAmplitudeRequiredScaleIndependent channel momentum -> framework.PionlessRGCalculation channel scale momentum -> let flow := framework.pionlessRGFlow channel (∀ mu, flow.NonpoleAt mu -> mu * deriv flow.c0 mu = flow.beta0 mu) ∧ (∀ mu, flow.NonpoleAt mu -> mu * deriv flow.c2 mu = flow.beta2 mu) ∧ (∀ mu, flow.NonpoleAt mu -> flow.c0 mu = flow.c0Solution mu) ∧ (∀ mu, flow.NonpoleAt mu -> flow.c2 mu = flow.c2Solution mu) ∧ framework.equationElevenPionlessRunningValuesAt channel := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.pionless_rg_exposes_derivative_equations_and_running_solutions -- A singleton momentum index cannot pretend to be a threshold neighborhood. -- This deliberately rejects a degeneracy allowed by the former contract. example (framework : NuclearScatteringFramework Channel Scale Unit Coupling Term Order Regime Fit) (channel : Channel) : ¬framework.PionlessObservableMatchingAt channel := by rintro ⟨_, sample, domain, _⟩ letI : PhysicsLogic.Framework.EffectiveRangeExpansion.approach.NeBot := PhysicsLogic.Framework.EffectiveRangeExpansion.the_positive_energy_approach_is_nontrivial have coordinate : ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, framework.momentumValue () = p := domain.mono (fun p hp => by have unit : sample p = () := Subsingleton.elim _ _ simpa only [unit] using hp.1) have limiting := PhysicsLogic.Framework.EffectiveRangeExpansion.the_approach_really_tends_to_zero.congr' (coordinate.mono (fun _ h => h.symm)) have zero : framework.momentumValue () = 0 := tendsto_nhds_unique tendsto_const_nhds limiting have positive : ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, 0 < p := self_mem_nhdsWithin obtain ⟨p, equality, hp⟩ := (coordinate.and positive).exists exact (ne_of_gt hp) (equality.symm.trans zero) -- A nonzero-range model realizes all real-scale premises. The contact can -- have a finite-momentum pole; only the positive threshold neighborhood is -- used, separately at each non-pole subtraction scale. noncomputable def diagnosticFlow (inverseLength : Real) : PionlessRGFlow where mass := 4 * Real.pi inverseScatteringLength := inverseLength effectiveRange := 1 c0 := fun mu => (-mu + inverseLength)⁻¹ c2 := fun mu => (1 / 2) / (-mu + inverseLength) ^ 2 private theorem diagnosticSolution (inverseLength : Real) : (diagnosticFlow inverseLength).EquationElevenAt := by let phase := fun p : Real => -inverseLength + (1 / 2) * p ^ 2 let contact := fun mu p : Real => (-mu + inverseLength - (1 / 2) * p ^ 2)⁻¹ have limits (mu : Real) (nonpole : (diagnosticFlow inverseLength).NonpoleAt mu) : PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients (contact mu) ((-mu + inverseLength)⁻¹) ((1 / 2) / (-mu + inverseLength) ^ 2) ∧ (∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, (phase p + mu) * contact mu p = -1) := by have hn : -mu + inverseLength ≠ 0 := by simpa [PionlessRGFlow.NonpoleAt, diagnosticFlow, sub_eq_add_neg] using nonpole have denominator : Tendsto (fun p : Real => -mu + inverseLength - (1 / 2) * p ^ 2) PhysicsLogic.Framework.EffectiveRangeExpansion.approach (𝓝 (-mu + inverseLength)) := by simpa using ((PhysicsLogic.Framework.EffectiveRangeExpansion.the_approach_really_tends_to_zero.pow 2).const_mul (1 / 2 : Real)).const_sub (-mu + inverseLength) have away := denominator.eventually (eventually_ne_nhds hn) have positive : ∀ᶠ p in PhysicsLogic.Framework.EffectiveRangeExpansion.approach, 0 < p := self_mem_nhdsWithin refine ⟨?_, ?_⟩ · have numerator : Tendsto (fun _ : Real => (1 / 2 : Real)) PhysicsLogic.Framework.EffectiveRangeExpansion.approach (𝓝 (1 / 2 : Real)) := tendsto_const_nhds have limit := numerator.div (denominator.mul_const (-mu + inverseLength)) (mul_ne_zero hn hn) have equal : (fun p : Real => (1 / 2 : Real) / ((-mu + inverseLength - (1 / 2) * p ^ 2) * (-mu + inverseLength))) =ᶠ[ PhysicsLogic.Framework.EffectiveRangeExpansion.approach] (fun p => (contact mu p - (-mu + inverseLength)⁻¹) / p ^ 2) := by filter_upwards [away, positive] with p hp positiveP dsimp [contact] rw [inv_sub_inv hp hn, show (-mu + inverseLength) - (-mu + inverseLength - (1 / 2) * p ^ 2) = (1 / 2) * p ^ 2 by ring, div_right_comm ((1 / 2 : Real) * p ^ 2) ((-mu + inverseLength - (1 / 2) * p ^ 2) * (-mu + inverseLength)) (p ^ 2), mul_div_cancel_right₀ (1 / 2 : Real) (pow_ne_zero 2 (ne_of_gt positiveP))] simpa only [PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients, pow_two] using limit.congr' equal · filter_upwards [away] with p hp dsimp [phase, contact] rw [show -inverseLength + (1 / 2 : Real) * p ^ 2 + mu = -(-mu + inverseLength - (1 / 2) * p ^ 2) by ring] rw [neg_mul, mul_inv_cancel₀ hp] refine (PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_family_controls_running_and_resummed_terms (diagnosticFlow inverseLength) phase contact (1 / 4) 1 (1 / 2) ?_ ?_ ?_ ?_ (by norm_num) (by norm_num) (by norm_num [diagnosticFlow])).1 · norm_num [PionlessRGFlow.PhysicalAt, diagnosticFlow, Real.pi_pos] · have observable := ContactMatching.negligible_remainder_identifies_observable_coefficients phase (fun _ => 0) inverseLength (1 / 2) (Eventually.of_forall (fun _ => by dsimp [phase]; ring)) (by simpa using tendsto_const_nhds) norm_num [diagnosticFlow] at observable ⊢ exact observable · intro mu nonpole simpa [diagnosticFlow, Real.pi_ne_zero] using (limits mu nonpole).1 · intro mu nonpole exact (limits mu nonpole).2 -- The original finite-a example and the unitary limit use the same observable -- argument. Zero inverse length is admitted; the zero subtraction scale is not. example : (diagnosticFlow (-1 / 2)).EquationElevenAt := diagnosticSolution (-1 / 2) example : (diagnosticFlow 0).EquationElevenAt ∧ ¬(diagnosticFlow 0).NonpoleAt 0 ∧ (∀ mu : Real, mu ≠ 0 -> (diagnosticFlow 0).ExactBetaDerivativesAt mu) ∧ (∀ mu : Real, 0 < mu -> -mu * ((diagnosticFlow 0).mass / (4 * Real.pi)) * (diagnosticFlow 0).c0 mu = 1) := by have values := diagnosticSolution 0 refine ⟨values, by simp [PionlessRGFlow.NonpoleAt, diagnosticFlow], ?_, ?_⟩ · intro mu nonzero exact (diagnosticFlow 0).equation_eleven_derives_actual_beta_derivatives values mu (by simpa [PionlessRGFlow.NonpoleAt, diagnosticFlow] using nonzero) · intro mu positive obtain ⟨_, lower, upper⟩ := (diagnosticFlow 0).scale_window_derives_leading_contact_bounds values mu 0 positive (by norm_num) (by simp [diagnosticFlow]) norm_num at lower upper simpa only [neg_mul] using le_antisymm upper lower #print axioms PionlessRGFlow.observable_family_derives_equation_eleven #print axioms NuclearScatteringFramework.observable_matching_derives_running_values #print axioms NuclearScatteringFramework.scale_independence_yields_running_couplings_and_rg_equations