import PhysicsLogic.Papers.KaplanSavageWise1998 open PhysicsLogic.Papers.KaplanSavageWise1998 Filter open scoped Topology -- Literal complete contract: one nonempty window, with the same calibrated -- contacts in running, local interactions, optical relations and loop errors. -- The precision concerns the first insertion, not the unknown EFT remainder. example : forall (flow : PionlessRGFlow) (phase : Real -> Real) (cutoff bound rho c epsilon : Real), 0 < flow.mass -> Tendsto (fun q => (phase q - (-flow.inverseScatteringLength)) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (flow.effectiveRange / 2)) -> (forall mu, -mu + flow.inverseScatteringLength ≠ 0 -> Tendsto (fun q => (-1 / (phase q + mu) - flow.mass / (4 * Real.pi) * flow.c0 mu) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (flow.mass / (4 * Real.pi) * flow.c2 mu))) -> 0 < cutoff -> |cutoff * (flow.effectiveRange / 2)| <= bound -> 0 < rho -> 1 <= c -> rho ^ 2 + 2 * c * rho <= 1 -> 0 < epsilon -> epsilon < 1 -> |flow.inverseScatteringLength| * (bound + 1) < rho * epsilon * cutoff -> (forall mu, -mu + flow.inverseScatteringLength ≠ 0 -> flow.c0 mu = (4 * Real.pi / flow.mass) * (-mu + flow.inverseScatteringLength)⁻¹ ∧ flow.c2 mu = (2 * Real.pi / flow.mass) * (-mu + flow.inverseScatteringLength)⁻¹ ^ 2 * flow.effectiveRange ∧ HasDerivAt flow.c0 (flow.mass / (4 * Real.pi) * flow.c0 mu ^ 2) mu ∧ HasDerivAt flow.c2 (flow.mass / (2 * Real.pi) * flow.c0 mu * flow.c2 mu) mu) ∧ (exists p mu : Real, |flow.inverseScatteringLength| / rho < p ∧ p < epsilon * cutoff / (bound + 1) ∧ p <= c * mu ∧ mu <= c * p) ∧ (forall p mu : Real, |flow.inverseScatteringLength| / rho < p -> p < epsilon * cutoff / (bound + 1) -> p <= c * mu -> mu <= c * p -> -mu + flow.inverseScatteringLength ≠ 0 ∧ let g0 := flow.mass / (4 * Real.pi) * flow.c0 mu let g2 := flow.mass / (4 * Real.pi) * flow.c2 mu (∃! pair : Complex × Complex, pair.1 + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * pair.1 = -(g0 : Complex) ∧ pair.2 + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * pair.2 = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * pair.1)) ∧ (forall leading correction : Complex, (leading + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * leading = -(g0 : Complex) ∧ correction + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * correction = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * leading)) -> leading = (-(flow.inverseScatteringLength : Complex) - Complex.I * (p : Complex))⁻¹ ∧ correction = -((flow.effectiveRange / 2 * p ^ 2 : Real) : Complex) * leading ^ 2 ∧ ‖correction‖ <= (bound * p / cutoff) * ‖leading‖ ∧ ‖correction‖ < epsilon * ‖leading‖ ∧ ‖correction‖ < ‖leading‖ ∧ Complex.normSq (1 + 2 * Complex.I * (p : Complex) * leading) = 1 ∧ correction.im = 2 * p * (star leading * correction).re ∧ (forall t : Real, (leading + (t : Complex) * correction).im - p * Complex.normSq (leading + (t : Complex) * correction) = -p * t ^ 2 * Complex.normSq correction) ∧ (forall n : Nat, let loopSum := (Finset.range (n + 1)).sum (fun j => -(g0 : Complex) * (-(g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ^ j) ‖loopSum - leading‖ = (|g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖) ^ (n + 1) * ‖leading‖ ∧ ‖leading‖ <= ‖loopSum - leading‖))) := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_matching_realizes_a_controlled_resummation_window -- Exact feasibility, including zero inverse length. Failure here means this -- sufficient window is empty, not that every EFT treatment is impossible. example (alpha cutoff bound rho epsilon : Real) (boundNonnegative : 0 <= bound) (ratioPositive : 0 < rho) : (exists p : Real, |alpha| / rho < p ∧ p < epsilon * cutoff / (bound + 1)) ↔ |alpha| * (bound + 1) < rho * epsilon * cutoff := by constructor · rintro ⟨p, lower, upper⟩ have cross := (div_lt_div_iff₀ ratioPositive (by positivity : 0 < bound + 1)).mp (lower.trans upper) nlinarith · intro separated apply exists_between apply (div_lt_div_iff₀ ratioPositive (by positivity : 0 < bound + 1)).mpr nlinarith private noncomputable def matchedFlow (alpha : Real) : PionlessRGFlow where mass := 4 * Real.pi inverseScatteringLength := alpha effectiveRange := 1 c0 := fun mu => (alpha - mu)⁻¹ c2 := fun mu => (1 / 2) / (alpha - mu) ^ 2 private theorem matchedObservable (alpha : Real) : Tendsto (fun q : Real => ((-alpha + q ^ 2 / 2) - (-alpha)) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (1 / 2)) := by have positive : ∀ᶠ q : Real in nhdsWithin 0 (Set.Ioi 0), 0 < q := self_mem_nhdsWithin apply tendsto_const_nhds.congr' filter_upwards [positive] with q hq field_simp [ne_of_gt hq] ring private theorem matchedCouplings (alpha mu : Real) (nonpole : -mu + alpha ≠ 0) : Tendsto (fun q => (-1 / ((-alpha + q ^ 2 / 2) + mu) - (matchedFlow alpha).mass / (4 * Real.pi) * (matchedFlow alpha).c0 mu) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((matchedFlow alpha).mass / (4 * Real.pi) * (matchedFlow alpha).c2 mu)) := by apply (ContactMatching.canonical_contact_coefficients_iff_values (fun q => -alpha + q ^ 2 / 2) mu alpha (1 / 2) _ _ (matchedObservable alpha) (by simpa [sub_eq_add_neg, add_comm] using nonpole)).mpr constructor <;> simp [matchedFlow, Real.pi_ne_zero] -- A finite negative scattering length, not just alpha=0. In chosen units -- a=-1000, r0=Lambda=1. The whole open p-window is (1/125, 1/15), -- with p/2 <= mu <= 2p. The complete theorem supplies numerical solutions, -- so the downstream conditional amplitude claims are not vacuous. example (p mu : Real) (lower : 1 / 125 < p) (upper : p < 1 / 15) (lowerScale : p <= 2 * mu) (upperScale : mu <= 2 * p) : let g0 := ((-1 / 1000 : Real) - mu)⁻¹ let g2 := (1 / 2 : Real) / ((-1 / 1000 : Real) - mu) ^ 2 (∃! pair : Complex × Complex, pair.1 + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * pair.1 = -(g0 : Complex) ∧ pair.2 + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * pair.2 = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * pair.1)) ∧ (forall leading correction : Complex, (leading + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * leading = -(g0 : Complex) ∧ correction + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * correction = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * leading)) -> ‖correction‖ < (1 / 10 : Real) * ‖leading‖ ∧ (forall n : Nat, let loopSum := (Finset.range (n + 1)).sum (fun j => -(g0 : Complex) * (-(g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ^ j) ‖leading‖ <= ‖loopSum - leading‖)) := by have full := (PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_matching_realizes_a_controlled_resummation_window : forall (data : PionlessRGFlow), _) (matchedFlow (-1 / 1000)) (fun q => -(-1 / 1000) + q ^ 2 / 2) 1 (1 / 2) (1 / 8) 2 (1 / 10) (by dsimp [matchedFlow]; positivity) (matchedObservable _) (matchedCouplings _) (by norm_num) (by norm_num [matchedFlow]) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num [matchedFlow]) have point := full.2.2 p mu (by norm_num [matchedFlow] at lower ⊢; exact lower) (by norm_num at upper ⊢; exact upper) lowerScale upperScale dsimp only [matchedFlow] at point simp only [div_self (mul_ne_zero (by norm_num : (4 : Real) ≠ 0) Real.pi_ne_zero), one_mul] at point refine ⟨point.2.1, ?_⟩ intro leading correction equations have result := point.2.2 leading correction equations exact ⟨result.2.2.2.1, fun n => (result.2.2.2.2.2.2.2.2 n).2⟩ -- The finite-a enhanced window cannot extend to p=0. A large effective -- range can also empty this chosen joint window despite the same large a. example : ¬(exists p : Real, |(-1 / 1000 : Real)| / (1 / 8) < p ∧ p < (1 / 10 : Real) / (1000 + 1)) := by rintro ⟨p, lower, upper⟩ norm_num at lower upper linarith -- Removing the upper comparison mu<=c*p invalidates the claimed raw-loop -- obstruction, even with matched negative a and momentum in the window. -- This is a scalar-model scale diagnostic, not a nuclear-potential construction. example : let g0 : Real := -10 / 61 let p : Real := 1 let mu : Real := 6 let leading : Complex := -(g0 : Complex) / (1 + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ((-1 / 10 : Real) - mu) * g0 = 1 ∧ (4 / 5 : Real) < p ∧ p < (4 / 3 : Real) ∧ p <= 2 * mu ∧ ¬mu <= 2 * p ∧ ‖-(g0 : Complex) - leading‖ < ‖leading‖ := by dsimp only have square : ‖(6 : Complex) + Complex.I‖ ^ 2 = 37 := by rw [Complex.sq_norm] norm_num [Complex.normSq_apply] have ratio : |(-10 / 61 : Real)| * ‖(6 : Complex) + Complex.I * 1‖ < 1 := by norm_num only [abs_div, abs_neg, mul_one] nlinarith [norm_nonneg ((6 : Complex) + Complex.I)] have error := ContactChains.finite_leading_sum_has_exact_error_at_scale (-10 / 61) 6 1 (-((-10 / 61 : Real) : Complex) / (1 + ((-10 / 61 : Real) : Complex) * ((6 : Complex) + Complex.I * 1))) (by norm_num) rfl 0 have nonzero : -((-10 / 61 : Real) : Complex) / (1 + ((-10 / 61 : Real) : Complex) * ((6 : Complex) + Complex.I * 1)) ≠ 0 := by apply div_ne_zero · norm_num · exact PhysicsLogic.Framework.ElasticSWave.contact_denominator_ne_zero_of_positive_momentum (-10 / 61) 6 1 (by norm_num) refine ⟨by norm_num, by norm_num, by norm_num, by norm_num, by norm_num, ?_⟩ have strict := mul_lt_of_lt_one_left (norm_pos_iff.mpr nonzero) ratio have result := error.trans_lt (by simpa only [Nat.zero_add, pow_one] using strict) simpa using result #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_matching_realizes_a_controlled_resummation_window