import PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains example : forall (g0 mu p : Real) (leading : Complex), 0 < p -> leading = -(g0 : Complex) / (1 + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) -> forall n : Nat, ‖(Finset.range (n + 1)).sum (fun j => -(g0 : Complex) * (-(g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ^ j) - leading‖ = (|g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖) ^ (n + 1) * ‖leading‖ := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.finite_leading_sum_has_exact_error_at_scale set_option backward.isDefEq.respectTransparency false open PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains open Filter PhysicsLogic.Framework.EffectiveRangeExpansion open scoped Topology example : forall (last : Nat) (leading correction : Complex), let context := firstOrderCountingContext last leading correction (forall n q, context.retainedThrough n q ↔ n <= last ∧ q <= 0 ∧ (n : Int) - 1 <= q) ∧ (forall n, context.resummedAt n () ↔ n = 0) ∧ (forall n, context.perturbativeAt n () ↔ n ≠ 0 ∧ n <= last) ∧ (context.NonvacuousSoundAt () ↔ 1 <= last ∧ ‖correction‖ < ‖leading‖) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.first_order_counting_context_characterization -- The whole generated API output is equivalent to the numerical conclusion -- already present in the complete value contract, not an extra physics input. example : forall (last : Nat) (leading correction : Complex) (p cutoff bound : Real), 1 <= last -> ((let context := firstOrderCountingContext last leading correction context.HasResummedLeadingSector () (-1) ∧ ¬context.UniformlyPerturbativeThrough () 0 ∧ context.TreatmentsAreSeparatedAt () 0 ∧ (forall n, context.retainedThrough n 0 ↔ n <= 1) ∧ (bound * p < cutoff -> context.NonvacuousSoundAt ())) ↔ (bound * p < cutoff -> ‖correction‖ < ‖leading‖)) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.first_order_treatment_contract_iff_numerical_suppression -- Identical allowed grades and treatments do not certify numerical suppression. example : let context := firstOrderCountingContext 1 (1 : Complex) (2 : Complex) context.resummedAt 0 () ∧ context.perturbativeAt 1 () ∧ ¬context.NonvacuousSoundAt () := by have meaning := first_order_counting_context_characterization 1 (1 : Complex) (2 : Complex) exact ⟨(meaning.2.1 0).mpr rfl, (meaning.2.2.1 1).mpr (by decide), by rw [meaning.2.2.2] norm_num⟩ -- Zero coefficients remain allowed interactions, not exact nonzero orders. example : let context := firstOrderCountingContext 1 (1 : Complex) (0 : Complex) context.contributesAt 1 () 0 ∧ context.perturbativeAt 1 () ∧ context.NonvacuousSoundAt () ∧ ¬context.retainedThrough 2 0 := by have meaning := first_order_counting_context_characterization 1 (1 : Complex) (0 : Complex) refine ⟨by norm_num [firstOrderCountingContext], (meaning.2.2.1 1).mpr (by decide), meaning.2.2.2.mpr (by norm_num), ?_⟩ rw [meaning.1] norm_num -- A leading-only jet does not certify a first-correction comparison. example : let context := firstOrderCountingContext 0 (1 : Complex) (0 : Complex) context.resummedAt 0 () ∧ ¬context.contributesAt 1 () 0 ∧ ¬context.perturbativeAt 1 () ∧ ¬context.NonvacuousSoundAt () := by have meaning := first_order_counting_context_characterization 0 (1 : Complex) (0 : Complex) refine ⟨(meaning.2.1 0).mpr rfl, by norm_num [firstOrderCountingContext], ?_, ?_⟩ · rw [meaning.2.2.1] norm_num · rw [meaning.2.2.2] norm_num example : forall (g k : Nat -> Real) (last : Nat) (phase contact : Real -> Real) (p cutoff inverseLength rho bound : Real) (leading correction : Complex), 1 <= last -> 0 < p -> p <= cutoff -> |inverseLength| <= rho * p -> rho < 1 -> HasFirstTwoCoefficients phase (-inverseLength) (k 1) -> HasFirstTwoCoefficients contact (g 0) (g 1) -> (∀ᶠ q in approach, (phase q + p) * contact q = -1) -> (forall n, 2 <= n -> n <= last -> PowerSeries.coeff n (PowerSeries.mk g * (PowerSeries.C (inverseLength - p) - PowerSeries.X * PowerSeries.mk (fun j => k (j + 1)))) = PowerSeries.coeff n (1 : PowerSeries Real)) -> (forall j, 0 < j -> j <= last -> |cutoff ^ (2 * j - 1) * k j| <= bound) -> (leading + (g 0 : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * leading = -(g 0 : Complex) ∧ correction + (g 0 : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * correction = -(g 1 : Complex) * (p : Complex) ^ 2 * (1 + ((p : Complex) + Complex.I * (p : Complex)) * leading)) -> let context := firstOrderCountingContext last leading correction context.HasResummedLeadingSector () (-1) ∧ ¬context.UniformlyPerturbativeThrough () 0 ∧ context.TreatmentsAreSeparatedAt () 0 ∧ (forall n, context.retainedThrough n 0 ↔ n <= 1) ∧ (bound * p < cutoff -> context.NonvacuousSoundAt ()) := by intro g k last phase contact p cutoff inverseLength rho bound leading correction firstRetained positive below window ratio observable couplings inverseAmplitude higher natural localEquations exact ((PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_derives_first_order_treatment_and_amplitudes : forall (g k : Nat -> Real), _) g k last phase contact p cutoff inverseLength rho bound leading correction firstRetained positive below window ratio observable couplings inverseAmplitude higher natural localEquations).2 example : forall (interaction result : PowerSeries Complex) (loop : Complex), (forall n : Nat, n <= 1 -> PowerSeries.coeff n (result + interaction * PowerSeries.C loop * result + interaction) = 0) ↔ (PowerSeries.coeff 0 result + PowerSeries.coeff 0 interaction * loop * PowerSeries.coeff 0 result = -PowerSeries.coeff 0 interaction ∧ PowerSeries.coeff 1 result + PowerSeries.coeff 0 interaction * loop * PowerSeries.coeff 1 result = -PowerSeries.coeff 1 interaction * (1 + loop * PowerSeries.coeff 0 result)) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.graded_scattering_equation_iff_first_two_terms example : forall (g : Nat -> Real) (mu p : Real) (vertices : List Nat), -((vertices.map (fun n => PowerSeries.C ((g n : Complex) * (p : Complex) ^ (2 * n)) * (PowerSeries.X : PowerSeries Complex) ^ n)).prod * PowerSeries.C (-((mu : Complex) + Complex.I * (p : Complex))) ^ (vertices.length - 1)) = PowerSeries.C (amplitude g mu p vertices) * PowerSeries.X ^ vertices.sum := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.graded_chain_is_actual_amplitude_monomial -- Actual higher-derivative chains have no coefficient through the first -- correction. This does not assert nonzero coefficients for retained chains. example (g : Nat -> Real) (mu p : Real) (vertices : List Nat) (higher : 2 <= vertices.sum) (n : Nat) (retained : n <= 1) : PowerSeries.coeff n (-((vertices.map (fun j => PowerSeries.C ((g j : Complex) * (p : Complex) ^ (2 * j)) * (PowerSeries.X : PowerSeries Complex) ^ j)).prod * PowerSeries.C (-((mu : Complex) + Complex.I * (p : Complex))) ^ (vertices.length - 1))) = 0 := by rw [graded_chain_is_actual_amplitude_monomial, PowerSeries.coeff_C_mul_X_pow] exact if_neg (by omega) -- No project-defined predicate is needed on the readable side of this contract. -- The threshold variable q approaches zero from above at fixed mu=p. -- The quadratic limit derives the formerly separate constant limit. example (phase : Real -> Real) (constant quadratic : Real) : (Tendsto phase (nhdsWithin 0 (Set.Ioi 0)) (𝓝 constant) ∧ Tendsto (fun q => (phase q - constant) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (𝓝 quadratic)) ↔ Tendsto (fun q => (phase q - constant) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (𝓝 quadratic) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactMatching.first_two_coefficients_iff_quadratic_limit phase constant quadratic example : forall (phase contact : Real -> Real) (g0 g1 k1 p cutoff inverseLength rho bound : Real) (leading correction : Complex), 0 < p -> p <= cutoff -> |inverseLength| <= rho * p -> rho < 1 -> Tendsto (fun q => (phase q - (-inverseLength)) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (𝓝 k1) -> Tendsto (fun q => (contact q - g0) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (𝓝 g1) -> Filter.Eventually (fun q => (phase q + p) * contact q = -1) (nhdsWithin 0 (Set.Ioi 0)) -> |cutoff * k1| <= bound -> (leading + (g0 : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * leading = -(g0 : Complex) ∧ correction + (g0 : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * correction = -(g1 : Complex) * (p : Complex) ^ 2 * (1 + ((p : Complex) + Complex.I * (p : Complex)) * leading)) -> (forall loopCut : Nat, let loopSum := (Finset.range (loopCut + 1)).sum (fun loops => -(g0 : Complex) * (-(g0 : Complex) * ((p : Complex) + Complex.I * (p : Complex))) ^ loops) ‖loopSum - leading‖ = (‖(1 : Complex) + Complex.I‖ * |p * g0|) ^ (loopCut + 1) * ‖leading‖ ∧ (1 + rho <= ‖(1 : Complex) + Complex.I‖ -> ‖leading‖ <= ‖loopSum - leading‖)) ∧ leading = (-(inverseLength : Complex) - Complex.I * (p : Complex))⁻¹ ∧ correction = -((k1 * p ^ 2 : Real) : Complex) * leading ^ 2 ∧ ‖correction‖ <= (bound * p / cutoff) * ‖leading‖ ∧ (bound * p < cutoff -> ‖correction‖ < ‖leading‖) ∧ (forall parameter : Real, (leading + (parameter : Complex) * correction) + ((g0 + parameter * (g1 * p ^ 2) : Real) : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * (leading + (parameter : Complex) * correction) + ((g0 + parameter * (g1 * p ^ 2) : Real) : Complex) = (parameter : Complex) ^ 2 * ((g1 * p ^ 2 : Real) : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * correction) ∧ (forall msCoupling : Real, inverseLength * msCoupling = 1 -> forall loopCut : Nat, let msLoopSum := (Finset.range (loopCut + 1)).sum (fun loops => -(msCoupling : Complex) * (-(msCoupling : Complex) * (Complex.I * (p : Complex))) ^ loops) ‖msLoopSum - leading‖ = (p / |inverseLength|) ^ (loopCut + 1) * ‖leading‖ ∧ ‖leading‖ < ‖msLoopSum - leading‖) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.observable_matching_separates_loop_and_derivative_expansions #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.observable_matching_separates_loop_and_derivative_expansions -- The same observable, not a new independent resummed answer, fixes the -- exact MS error and strict loop-series radius. No full-EFT validity flag. example : forall (g alpha p : Real) (f : Complex), 0 < p -> alpha * g = 1 -> f = (-(alpha : Complex) - Complex.I * (p : Complex))⁻¹ -> let loopSum := fun cut : Nat => (Finset.range (cut + 1)).sum (fun n => amplitude (fun _ => g) 0 p (List.replicate (n + 1) 0)) (forall cut, ‖loopSum cut - f‖ = (p / |alpha|) ^ (cut + 1) * ‖f‖) ∧ (Tendsto (fun cut => ‖loopSum cut - f‖) atTop (𝓝 0) ↔ p < |alpha|) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.minimal_subtraction_matching_fixes_loop_series_radius -- A natural-size inverse length can permit a genuinely convergent leading -- MS series. This does not assert bounds for derivative terms or full physics. example : Tendsto (fun cut : Nat => ‖(Finset.range (cut + 1)).sum (fun n => amplitude (fun _ => 1 / 2) 0 1 (List.replicate (n + 1) 0)) - (-2 - Complex.I)⁻¹‖) atTop (𝓝 0) := by simpa using (minimal_subtraction_matching_fixes_loop_series_radius (1 / 2) 2 1 ((-2 - Complex.I)⁻¹) (by norm_num) (by norm_num) (by norm_num)).2.mpr (by norm_num) -- At the radius boundary the exact error stays equal to the answer's norm. example (cut : Nat) : ‖(Finset.range (cut + 1)).sum (fun n => amplitude (fun _ => 1) 0 1 (List.replicate (n + 1) 0)) - (-1 - Complex.I)⁻¹‖ = ‖(-1 - Complex.I : Complex)⁻¹‖ := by simpa using (minimal_subtraction_matching_fixes_loop_series_radius 1 1 1 ((-1 - Complex.I)⁻¹) (by norm_num) (by norm_num) (by norm_num)).1 cut -- Alpha=0 is the unitary limit, not a finite zero MS coupling. example : ¬ ∃ g : Real, (0 : Real) * g = 1 := by norm_num #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.minimal_subtraction_matching_fixes_loop_series_radius -- Exact coefficients, elastic unitarity and leading-loop convergence do not -- bound a higher shape term. This is a diagnostic, not a nuclear potential. example : let phase : Real -> Real := fun q => -1 + 16 * q ^ 4 let leading : Complex := (-1 - Complex.I * (1 / 2))⁻¹ let full : Complex := ((phase (1 / 2) : Complex) - Complex.I * (1 / 2))⁻¹ (Tendsto phase (nhdsWithin 0 (Set.Ioi 0)) (𝓝 (-1)) ∧ Tendsto (fun q => (phase q - (-1)) / q ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (𝓝 0)) ∧ (forall q : Real, 0 < q -> Complex.normSq (1 + 2 * Complex.I * (q : Complex) * ((phase q : Complex) - Complex.I * (q : Complex))⁻¹) = 1) ∧ Tendsto (fun cut : Nat => ‖(Finset.range (cut + 1)).sum (fun n => amplitude (fun _ => 1) 0 (1 / 2) (List.replicate (n + 1) 0)) - leading‖) atTop (𝓝 0) ∧ ‖full - leading‖ = 2 * ‖leading‖ ∧ 0 < ‖leading‖ := by have witness : let phase : Real -> Real := fun q => -1 + 16 * q ^ 4 let leading : Complex := (-1 - Complex.I * (1 / 2))⁻¹ let full : Complex := ((phase (1 / 2) : Complex) - Complex.I * (1 / 2))⁻¹ HasFirstTwoCoefficients phase (-1) 0 ∧ (forall q : Real, 0 < q -> Complex.normSq (1 + 2 * Complex.I * (q : Complex) * ((phase q : Complex) - Complex.I * (q : Complex))⁻¹) = 1) ∧ Tendsto (fun cut : Nat => ‖(Finset.range (cut + 1)).sum (fun n => amplitude (fun _ => 1) 0 (1 / 2) (List.replicate (n + 1) 0)) - leading‖) atTop (𝓝 0) ∧ ‖full - leading‖ = 2 * ‖leading‖ ∧ 0 < ‖leading‖ := by simpa only [PhysicsLogic.Framework.ElasticSWave.reducedAmplitude, PhysicsLogic.Framework.ElasticSWave.denominator, PhysicsLogic.Framework.ElasticSWave.ElasticUnitaryAt, PhysicsLogic.Framework.ElasticSWave.sMatrix, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_ofNat] using PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.ms_leading_convergence_does_not_control_an_uncontrolled_shape_term have preserved := And.intro (And.intro witness.1.constant_limit witness.1) witness.2 simpa only [PhysicsLogic.Framework.ElasticSWave.reducedAmplitude, PhysicsLogic.Framework.ElasticSWave.denominator, PhysicsLogic.Framework.ElasticSWave.ElasticUnitaryAt, PhysicsLogic.Framework.ElasticSWave.sMatrix, HasFirstTwoCoefficients, approach, Complex.ofReal_div, Complex.ofReal_one, Complex.ofReal_neg, Complex.ofReal_ofNat] using preserved #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.ms_leading_convergence_does_not_control_an_uncontrolled_shape_term example : forall (g : Nat -> Real) (mu p : Real) (evaluate : List Nat -> Complex), (forall vertices, vertices ≠ [] -> evaluate vertices = amplitude g mu p vertices) ↔ ((forall n, evaluate [n] = -(g n : Complex) * (p : Complex) ^ (2 * n)) ∧ (forall n tail, tail ≠ [] -> evaluate (n :: tail) = (g n : Complex) * (p : Complex) ^ (2 * n) * (-((mu : Complex) + Complex.I * (p : Complex))) * evaluate tail)) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.chain_evaluation_iff_tree_and_pds_composition -- All nonempty chain rules leave the empty-list value arbitrary. example (g : Nat -> Real) (mu p : Real) (emptyValue : Complex) : let evaluate := fun vertices => if vertices = [] then emptyValue else amplitude g mu p vertices evaluate [] = emptyValue ∧ (forall n, evaluate [n] = -(g n : Complex) * (p : Complex) ^ (2 * n)) ∧ (forall n tail, tail ≠ [] -> evaluate (n :: tail) = (g n : Complex) * (p : Complex) ^ (2 * n) * (-((mu : Complex) + Complex.I * (p : Complex))) * evaluate tail) := by dsimp refine ⟨by simp, ?_⟩ apply (chain_evaluation_iff_tree_and_pds_composition g mu p (fun vertices => if vertices = [] then emptyValue else amplitude g mu p vertices)).mp intro vertices nonempty simp [nonempty] -- Correct trees alone do not fix the loop phase. Reversing the absorptive -- sign changes the two-leading-vertex chain from 1+i to 1-i. example : amplitude (fun _ => 1) 1 1 [0, 0] = 1 + Complex.I ∧ amplitude (fun _ => 1) 1 1 [0, 0] ≠ 1 - Complex.I := by norm_num [amplitude, Complex.ext_iff] example : forall (g : Nat -> Real) (cutoff p : Real) (vertices : List Nat), 0 < cutoff -> 0 < p -> Ne vertices [] -> p * ‖amplitude g p p vertices‖ = ‖(1 : Complex) + Complex.I‖ ^ (vertices.length - 1) * (p / cutoff) ^ vertices.sum * (vertices.map (fun n => |cutoff ^ n * p ^ (n + 1) * g n|)).prod := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.normalized_chain_magnitude example : forall (g : Nat -> Real) (cutoff p a r : Real) (vertices : List Nat), 0 < cutoff -> 0 < p -> Ne vertices [] -> 0 <= a -> 0 <= r -> (forall n, n ∈ vertices -> |cutoff ^ n * p ^ (n + 1) * g n| <= a * r ^ n) -> p * ‖amplitude g p p vertices‖ <= ‖(1 : Complex) + Complex.I‖ ^ (vertices.length - 1) * a ^ vertices.length * (r * p / cutoff) ^ vertices.sum := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.contact_bounds_bound_chain example : forall (g k : Nat -> Real) (last : Nat) (p cutoff inverseLength rho bound : Real), 0 < p -> 0 < cutoff -> p <= cutoff -> |inverseLength| <= rho * p -> rho < 1 -> 0 <= bound -> (inverseLength - p) * g 0 = 1 -> (forall n, n < last -> (inverseLength - p) * g (n + 1) = (Finset.range (n + 1)).sum (fun j => k (n + 1 - j) * g j)) -> (forall j, 0 < j -> j <= last -> |cutoff ^ (2 * j - 1) * k j| <= bound) -> forall vertices : List Nat, Ne vertices [] -> (forall n, n ∈ vertices -> n <= last) -> p * ‖amplitude g p p vertices‖ <= ‖(1 : Complex) + Complex.I‖ ^ (vertices.length - 1) * (1 / (1 - rho)) ^ vertices.length * ((1 + bound / (1 - rho)) * p / cutoff) ^ vertices.sum := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_bounds_every_retained_chain example : forall (g0 p inverseLength rho : Real), 0 < p -> |inverseLength| <= rho * p -> rho < 1 -> (inverseLength - p) * g0 = 1 -> 1 / (1 + rho) <= |p * g0| /\ |p * g0| <= 1 / (1 - rho) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.leading_matching_bounds_normalized_contact example : forall (g : Nat -> Real) (p : Real), 0 < p -> forall loops : Nat, p * ‖amplitude g p p (List.replicate (loops + 1) 0)‖ = ‖(1 : Complex) + Complex.I‖ ^ loops * |p * g 0| ^ (loops + 1) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.leading_chain_magnitude example : forall (g : Nat -> Real) (p : Real) (leadingAmplitude : Complex), 0 < p -> leadingAmplitude = -(g 0 : Complex) / (1 + (g 0 : Complex) * ((p : Complex) + Complex.I * (p : Complex))) -> forall loopCut : Nat, ‖(Finset.range (loopCut + 1)).sum (fun loops => amplitude g p p (List.replicate (loops + 1) 0)) - leadingAmplitude‖ = (‖(1 : Complex) + Complex.I‖ * |p * g 0|) ^ (loopCut + 1) * ‖leadingAmplitude‖ := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.finite_leading_sum_has_exact_error example : forall (g : Nat -> Real) (p inverseLength rho : Real) (leadingAmplitude : Complex), 0 < p -> |inverseLength| <= rho * p -> rho < 1 -> (inverseLength - p) * g 0 = 1 -> leadingAmplitude = -(g 0 : Complex) / (1 + (g 0 : Complex) * ((p : Complex) + Complex.I * (p : Complex))) -> 1 + rho <= ‖(1 : Complex) + Complex.I‖ -> forall loopCut : Nat, ‖leadingAmplitude‖ <= ‖(Finset.range (loopCut + 1)).sum (fun loops => amplitude g p p (List.replicate (loops + 1) 0)) - leadingAmplitude‖ := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_obstructs_finite_leading_loop_approximation example : forall (g : Nat -> Real) (p inverseLength rho : Real), 0 < p -> |inverseLength| <= rho * p -> rho < 1 -> (inverseLength - p) * g 0 = 1 -> forall loops : Nat, ‖(1 : Complex) + Complex.I‖ ^ loops * (1 / (1 + rho)) ^ (loops + 1) <= p * ‖amplitude g p p (List.replicate (loops + 1) 0)‖ /\ p * ‖amplitude g p p (List.replicate (loops + 1) 0)‖ <= ‖(1 : Complex) + Complex.I‖ ^ loops * (1 / (1 - rho)) ^ (loops + 1) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_bounds_leading_chains_on_both_sides example : forall (g : Nat -> Real) (p inverseLength rho : Real), 0 < p -> |inverseLength| <= rho * p -> rho < 1 -> (inverseLength - p) * g 0 = 1 -> forall loopCut : Nat, exists vertices : List Nat, Ne vertices [] /\ loopCut < vertices.length - 1 /\ vertices.sum = 0 /\ 0 < p * ‖amplitude g p p vertices‖ /\ ‖(1 : Complex) + Complex.I‖ ^ (loopCut + 1) * (1 / (1 + rho)) ^ (loopCut + 2) <= p * ‖amplitude g p p vertices‖ := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.every_finite_loop_cut_misses_a_leading_chain example : forall (g : Real -> Nat -> Real) (k : Nat -> Real) (last : Nat) (cutoff inverseLength rho bound : Real), 0 < cutoff -> |inverseLength| <= rho * cutoff -> rho < 1 -> 0 <= bound -> (forall j, 0 < j -> j <= last -> |cutoff ^ (2 * j - 1) * k j| <= bound) -> (forall p, 0 < p -> p <= cutoff -> |inverseLength| <= rho * p -> (inverseLength - p) * g p 0 = 1) -> (forall p, 0 < p -> p <= cutoff -> |inverseLength| <= rho * p -> forall n, n < last -> (inverseLength - p) * g p (n + 1) = (Finset.range (n + 1)).sum (fun j => k (n + 1 - j) * g p j)) -> (exists p : Real, 0 < p /\ p <= cutoff /\ |inverseLength| <= rho * p) /\ (forall p, 0 < p -> p <= cutoff -> |inverseLength| <= rho * p -> (forall vertices : List Nat, Ne vertices [] -> (forall n, n ∈ vertices -> n <= last) -> p * ‖amplitude (g p) p p vertices‖ <= ‖(1 : Complex) + Complex.I‖ ^ (vertices.length - 1) * (1 / (1 - rho)) ^ vertices.length * ((1 + bound / (1 - rho)) * p / cutoff) ^ vertices.sum) /\ (forall loopCut : Nat, exists vertices : List Nat, Ne vertices [] /\ loopCut < vertices.length - 1 /\ vertices.sum = 0 /\ 0 < p * ‖amplitude (g p) p p vertices‖ /\ ‖(1 : Complex) + Complex.I‖ ^ (loopCut + 1) * (1 / (1 + rho)) ^ (loopCut + 2) <= p * ‖amplitude (g p) p p vertices‖)) /\ (forall vertices : List Nat, Ne vertices [] -> (vertices.sum <= 1 <-> vertices = List.replicate vertices.length 0 ∨ exists left right : Nat, vertices = List.replicate left 0 ++ [1] ++ List.replicate right 0)) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.fixed_matching_window_controls_actual_chains -- One finite-a model has nonzero leading chains beyond every loop cutoff. example (loopCut : Nat) : exists vertices : List Nat, Ne vertices [] /\ loopCut < vertices.length - 1 /\ vertices.sum = 0 /\ 0 < ‖amplitude (fun n => if n = 0 then -2 else 0) 1 1 vertices‖ := by obtain ⟨vertices, nonempty, loops, degree, positive, _⟩ := every_finite_loop_cut_misses_a_leading_chain (fun n => if n = 0 then -2 else 0) 1 (1 / 2) (1 / 2) (by norm_num) (by norm_num) (by norm_num) (by norm_num) loopCut exact ⟨vertices, nonempty, loops, degree, by simpa using positive⟩ -- Fixed matching data have a whole window, not a single tuned scale. example (last : Nat) : let g : Real -> Nat -> Real := fun p n => if n = 0 then -1 / p else 0 (forall p : Real, 0 < p -> p <= 1 -> |(0 : Real)| <= 0 * p -> (0 - p) * g p 0 = 1) /\ (forall p : Real, 0 < p -> p <= 1 -> |(0 : Real)| <= 0 * p -> forall n, n < last -> (0 - p) * g p (n + 1) = (Finset.range (n + 1)).sum (fun j => (0 : Real) * g p j)) := by dsimp constructor · intro p positive _ _ field_simp [ne_of_gt positive] ring · intro p _ _ _ n _ simp example : forall (g k : Nat -> Real) (last : Nat) (phase contact : Real -> Real) (p cutoff inverseLength rho bound : Real) (leadingAmplitude correctionAmplitude : Complex), 1 <= last -> 0 < p -> p <= cutoff -> |inverseLength| <= rho * p -> rho < 1 -> HasFirstTwoCoefficients phase (-inverseLength) (k 1) -> HasFirstTwoCoefficients contact (g 0) (g 1) -> (∀ᶠ q in approach, (phase q + p) * contact q = -1) -> (forall n, 2 <= n -> n <= last -> PowerSeries.coeff n (PowerSeries.mk g * (PowerSeries.C (inverseLength - p) - PowerSeries.X * PowerSeries.mk (fun j => k (j + 1)))) = PowerSeries.coeff n (1 : PowerSeries Real)) -> (forall j, 0 < j -> j <= last -> |cutoff ^ (2 * j - 1) * k j| <= bound) -> (leadingAmplitude + (g 0 : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * leadingAmplitude = -(g 0 : Complex) /\ correctionAmplitude + (g 0 : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * correctionAmplitude = -(g 1 : Complex) * (p : Complex) ^ 2 * (1 + ((p : Complex) + Complex.I * (p : Complex)) * leadingAmplitude)) -> (forall vertices : List Nat, Ne vertices [] -> (forall n, n ∈ vertices -> n <= last) -> p * ‖amplitude g p p vertices‖ <= ‖(1 : Complex) + Complex.I‖ ^ (vertices.length - 1) * (1 / (1 - rho)) ^ vertices.length * ((1 + bound / (1 - rho)) * p / cutoff) ^ vertices.sum) /\ (forall loopCut : Nat, ‖(Finset.range (loopCut + 1)).sum (fun loops => amplitude g p p (List.replicate (loops + 1) 0)) - leadingAmplitude‖ = (‖(1 : Complex) + Complex.I‖ * |p * g 0|) ^ (loopCut + 1) * ‖leadingAmplitude‖ /\ (1 + rho <= ‖(1 : Complex) + Complex.I‖ -> ‖leadingAmplitude‖ <= ‖(Finset.range (loopCut + 1)).sum (fun loops => amplitude g p p (List.replicate (loops + 1) 0)) - leadingAmplitude‖)) /\ (forall vertices : List Nat, Ne vertices [] -> (vertices.sum <= 1 <-> vertices = List.replicate vertices.length 0 ∨ exists left right : Nat, vertices = List.replicate left 0 ++ [1] ++ List.replicate right 0)) /\ leadingAmplitude = (-(inverseLength : Complex) - Complex.I * (p : Complex))⁻¹ /\ correctionAmplitude = -((k 1 * p ^ 2 : Real) : Complex) * leadingAmplitude ^ 2 /\ ‖correctionAmplitude‖ <= (bound * p / cutoff) * ‖leadingAmplitude‖ /\ (bound * p < cutoff -> ‖correctionAmplitude‖ < ‖leadingAmplitude‖) /\ (forall parameter : Real, (leadingAmplitude + (parameter : Complex) * correctionAmplitude) + ((g 0 + parameter * (g 1 * p ^ 2) : Real) : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * (leadingAmplitude + (parameter : Complex) * correctionAmplitude) + ((g 0 + parameter * (g 1 * p ^ 2) : Real) : Complex) = (parameter : Complex) ^ 2 * ((g 1 * p ^ 2 : Real) : Complex) * ((p : Complex) + Complex.I * (p : Complex)) * correctionAmplitude) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_and_local_equations_control_the_pionless_expansion -- Actual functions, not assigned coefficient labels, realize both examples. -- Only a small neighborhood at each fixed subtraction scale is required. private theorem rational_contact_coefficients (alpha mu range : Real) (nonpole : alpha - mu ≠ 0) : HasFirstTwoCoefficients (fun q : Real => -alpha + range * q ^ 2) (-alpha) range ∧ HasFirstTwoCoefficients (fun q : Real => (alpha - mu - range * q ^ 2)⁻¹) (alpha - mu)⁻¹ (range / (alpha - mu) ^ 2) ∧ (∀ᶠ q in approach, (-alpha + range * q ^ 2 + mu) * (alpha - mu - range * q ^ 2)⁻¹ = -1) := by have observable := PhysicsLogic.Papers.KaplanSavageWise1998.ContactMatching.negligible_remainder_identifies_observable_coefficients (fun q : Real => -alpha + range * q ^ 2) (fun _ => 0) alpha range (Eventually.of_forall (fun _ => by ring)) (by simpa using tendsto_const_nhds) have denominator : Tendsto (fun q : Real => alpha - mu - range * q ^ 2) approach (𝓝 (alpha - mu)) := by simpa using ((the_approach_really_tends_to_zero.pow 2).const_mul range).const_sub (alpha - mu) have away := denominator.eventually (eventually_ne_nhds nonpole) have positive : ∀ᶠ q in approach, 0 < q := self_mem_nhdsWithin refine ⟨observable, ?_, ?_⟩ · have numerator : Tendsto (fun _ : Real => range) approach (𝓝 range) := tendsto_const_nhds have limit := numerator.div (denominator.mul_const (alpha - mu)) (mul_ne_zero nonpole nonpole) have equal : (fun q : Real => range / ((alpha - mu - range * q ^ 2) * (alpha - mu))) =ᶠ[approach] (fun q => ((alpha - mu - range * q ^ 2)⁻¹ - (alpha - mu)⁻¹) / q ^ 2) := by filter_upwards [away, positive] with q hq positiveQ rw [inv_sub_inv hq nonpole, show (alpha - mu) - (alpha - mu - range * q ^ 2) = range * q ^ 2 by ring, div_right_comm (range * q ^ 2) ((alpha - mu - range * q ^ 2) * (alpha - mu)) (q ^ 2), mul_div_cancel_right₀ range (pow_ne_zero 2 (ne_of_gt positiveQ))] simpa only [HasFirstTwoCoefficients, pow_two] using limit.congr' equal · filter_upwards [away] with q hq rw [show -alpha + range * q ^ 2 + mu = -(alpha - mu - range * q ^ 2) by ring, neg_mul, mul_inv_cancel₀ hq] -- A nonzero first correction satisfies the complete argument, not just the -- degenerate zero-range case. Here a=2, mu=p=1, Lambda=2 and r0=1/8. example : 0 < ‖((3 + 4 * Complex.I) / 100 : Complex)‖ /\ ‖((3 + 4 * Complex.I) / 100 : Complex)‖ < ‖((-2 + 4 * Complex.I) / 5 : Complex)‖ := by have coefficients := rational_contact_coefficients (1 / 2) 1 (1 / 16) (by norm_num) have result := matching_and_local_equations_control_the_pionless_expansion (fun n => if n = 0 then -2 else 1 / 4) (fun _ => 1 / 16) 1 (fun q => -(1 / 2) + (1 / 16) * q ^ 2) (fun q => ((1 / 2) - 1 - (1 / 16) * q ^ 2)⁻¹) 1 2 (1 / 2) (1 / 2) (1 / 8) ((-2 + 4 * Complex.I) / 5) ((3 + 4 * Complex.I) / 100) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) coefficients.1 (by norm_num at coefficients ⊢; exact coefficients.2.1) coefficients.2.2 (by intro n lower upper; omega) (by intro j positive retained have : j = 1 := by omega subst j norm_num) (by norm_num [Complex.ext_iff, div_eq_mul_inv, Complex.inv_def, Complex.normSq_apply, Complex.mul_re, Complex.mul_im, pow_two]) obtain ⟨_, _, _, _, _, _, smaller, _⟩ := result exact ⟨by norm_num [norm_pos_iff, Complex.ext_iff], smaller (by norm_num)⟩ -- One finite negative scattering length supports both conclusions at once: -- every raw loop cutoff has order-one error, but the derivative correction -- is nonzero and small. This is a matched on-shell model, not a nuclear fit. -- The unmatched index-two coefficient is arbitrary: a first-order jet does -- not certify it, and the scoped API does not label it perturbative. example (loopCut : Nat) (unmatched : Real) : let leading : Complex := (4 + 16 * Complex.I) / 17 let correction : Complex := (15 - 8 * Complex.I) / 289 0 < ‖correction‖ /\ ‖correction‖ < ‖leading‖ /\ ‖leading‖ <= ‖(Finset.range (loopCut + 1)).sum (fun loops => amplitude (fun n => if n = 0 then -4 / 5 else if n = 1 then 1 / 25 else unmatched) 1 1 (List.replicate (loops + 1) 0)) - leading‖ ∧ (firstOrderCountingContext 1 leading correction).HasResummedLeadingSector () (-1) ∧ ¬(firstOrderCountingContext 1 leading correction).UniformlyPerturbativeThrough () 0 ∧ (firstOrderCountingContext 1 leading correction).TreatmentsAreSeparatedAt () 0 ∧ (firstOrderCountingContext 1 leading correction).NonvacuousSoundAt () ∧ ¬(firstOrderCountingContext 1 leading correction).perturbativeAt 2 () ∧ ‖amplitude (fun n => if n = 0 then -4 / 5 else if n = 1 then 1 / 25 else unmatched) 1 1 [2]‖ = |unmatched| := by dsimp have coefficients := rational_contact_coefficients (-1 / 4) 1 (1 / 16) (by norm_num) have complete := matching_derives_first_order_treatment_and_amplitudes (fun n => if n = 0 then -4 / 5 else if n = 1 then 1 / 25 else unmatched) (fun _ => 1 / 16) 1 (fun q => -(-1 / 4) + (1 / 16) * q ^ 2) (fun q => ((-1 / 4) - 1 - (1 / 16) * q ^ 2)⁻¹) 1 2 (-1 / 4) (1 / 4) (1 / 8) ((4 + 16 * Complex.I) / 17) ((15 - 8 * Complex.I) / 289) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) coefficients.1 (by norm_num at coefficients ⊢; exact coefficients.2.1) coefficients.2.2 (by intro n lower upper; omega) (by intro j positive retained have : j = 1 := by omega subst j norm_num) (by norm_num [Complex.ext_iff, div_eq_mul_inv, Complex.inv_def, Complex.normSq_apply, Complex.mul_re, Complex.mul_im, pow_two]) have normSquare : ‖(1 : Complex) + Complex.I‖ ^ 2 = 2 := by norm_num [Complex.sq_norm, Complex.normSq_apply] have result := complete.1 exact ⟨by norm_num [norm_pos_iff, Complex.ext_iff], result.2.2.2.2.2.2.1 (by norm_num), (result.2.1 loopCut).2 (by nlinarith [norm_nonneg ((1 : Complex) + Complex.I)]), complete.2.1, complete.2.2.1, complete.2.2.2.1, complete.2.2.2.2.2 (by norm_num), by norm_num [firstOrderCountingContext], by simp [amplitude]⟩ -- Keeping degree two really uses the separately supplied higher jet. This -- is the same observable as above, now with its nonzero C4 coefficient. example : 0 < ‖amplitude (fun n => if n = 0 then -4 / 5 else if n = 1 then 1 / 25 else -1 / 500) 1 1 [2]‖ ∧ ‖amplitude (fun n => if n = 0 then -4 / 5 else if n = 1 then 1 / 25 else -1 / 500) 1 1 [2]‖ <= (4 / 3 : Real) * ((7 / 6) / 2) ^ 2 := by let g : Nat -> Real := fun n => if n = 0 then -4 / 5 else if n = 1 then 1 / 25 else -1 / 500 let k : Nat -> Real := fun n => if n = 1 then 1 / 16 else 0 have coefficients := rational_contact_coefficients (-1 / 4) 1 (1 / 16) (by norm_num) have jet := (PhysicsLogic.Papers.KaplanSavageWise1998.ContactMatching.finite_inverse_amplitude_jet_iff_matching g k 2 1 (-1 / 4)).mpr (by refine ⟨by norm_num [g], ?_⟩ intro n retained interval_cases n <;> norm_num [g, k, Finset.sum_range_succ]) have result := matching_and_local_equations_control_the_pionless_expansion g k 2 (fun q => -(-1 / 4) + (1 / 16) * q ^ 2) (fun q => ((-1 / 4) - 1 - (1 / 16) * q ^ 2)⁻¹) 1 2 (-1 / 4) (1 / 4) (1 / 8) ((4 + 16 * Complex.I) / 17) ((15 - 8 * Complex.I) / 289) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by simpa [k] using coefficients.1) (by norm_num [g] at coefficients ⊢; exact coefficients.2.1) coefficients.2.2 (fun n _ retained => jet n retained) (by intro j positive retained interval_cases j <;> norm_num [k]) (by norm_num [g, Complex.ext_iff, div_eq_mul_inv, Complex.inv_def, Complex.normSq_apply, Complex.mul_re, Complex.mul_im, pow_two]) refine ⟨?_, ?_⟩ · norm_num [amplitude, norm_pos_iff, Complex.ext_iff] · have bound := result.1 [2] (by simp) (by simp) norm_num [g] at bound ⊢ exact bound -- The weaker rho<1 window alone does not obstruct good raw truncations. -- Here a=-4/3 and p=mu=1; even though all leading chains are nonzero, -- every finite sum has relative error strictly below one. example (loopCut : Nat) : |(-3 / 4 : Real)| <= (3 / 4) * 1 /\ (3 / 4 : Real) < 1 /\ ((-3 / 4 : Real) - 1) * (-4 / 7) = 1 /\ (forall loops : Nat, 0 < ‖amplitude (fun _ => -4 / 7) 1 1 (List.replicate (loops + 1) 0)‖) /\ ‖(Finset.range (loopCut + 1)).sum (fun loops => amplitude (fun _ => -4 / 7) 1 1 (List.replicate (loops + 1) 0)) - ((12 + 16 * Complex.I) / 25)‖ < ‖((12 + 16 * Complex.I) / 25 : Complex)‖ := by refine ⟨by norm_num, by norm_num, by norm_num, ?_, ?_⟩ · intro loops have magnitude := leading_chain_magnitude (fun _ => -4 / 7) 1 (by norm_num) loops have loopPositive : 0 < ‖(1 : Complex) + Complex.I‖ := by norm_num [norm_pos_iff, Complex.ext_iff] norm_num at magnitude simp only [neg_div] rw [magnitude] positivity rw [finite_leading_sum_has_exact_error (fun _ => -4 / 7) 1 ((12 + 16 * Complex.I) / 25) (by norm_num) (by norm_num [Complex.ext_iff, div_eq_mul_inv, Complex.inv_def, Complex.normSq_apply, Complex.mul_re, Complex.mul_im, pow_two]) loopCut] norm_num have normSquare : ‖(1 : Complex) + Complex.I‖ ^ 2 = 2 := by norm_num [Complex.sq_norm, Complex.normSq_apply] have ratio : ‖(1 : Complex) + Complex.I‖ * (4 / 7) < 1 := by nlinarith [norm_nonneg ((1 : Complex) + Complex.I)] have power := pow_lt_one₀ (by positivity : 0 <= ‖(1 : Complex) + Complex.I‖ * (4 / 7)) ratio (by omega : loopCut + 1 ≠ 0) have positive : 0 < ‖((12 + 16 * Complex.I) / 25 : Complex)‖ := by norm_num [norm_pos_iff, Complex.ext_iff] simpa using mul_lt_mul_of_pos_right power positive -- For the very same alpha=-3/4, p=1 and resummed observable used above, -- MS has ratio 4/3 even though the PDS ratio is 4*sqrt(2)/7<1. example (cut : Nat) : ‖((12 + 16 * Complex.I) / 25 : Complex)‖ < ‖(Finset.range (cut + 1)).sum (fun n => amplitude (fun _ => -4 / 3) 0 1 (List.replicate (n + 1) 0)) - ((12 + 16 * Complex.I) / 25)‖ := by have result := minimal_subtraction_matching_fixes_loop_series_radius (-4 / 3) (-3 / 4) 1 ((12 + 16 * Complex.I) / 25) (by norm_num) (by norm_num) (by norm_num [Complex.ext_iff, div_eq_mul_inv, Complex.inv_def, Complex.normSq_apply, Complex.mul_re, Complex.mul_im, pow_two]) rw [result.1 cut] norm_num have grows := one_lt_pow₀ (by norm_num : (1 : Real) < 4 / 3) (by omega : cut + 1 ≠ 0) have positive : 0 < ‖((12 + 16 * Complex.I) / 25 : Complex)‖ := by norm_num [norm_pos_iff, Complex.ext_iff] simpa using mul_lt_mul_of_pos_right grows positive #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.fixed_matching_window_controls_actual_chains #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.chain_evaluation_iff_tree_and_pds_composition #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.finite_leading_sum_has_exact_error #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_obstructs_finite_leading_loop_approximation example : forall (g h mu p : Real) (f0 f1 : Complex), (f0 + (g : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * f0 = -(g : Complex) /\ f1 + (g : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * f1 = -(h : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * f0)) ↔ (PhysicsLogic.Framework.ElasticSWave.contactDenominator g mu p ≠ 0 /\ f0 = PhysicsLogic.Framework.ElasticSWave.contactAmplitude g mu p /\ f1 = PhysicsLogic.Framework.ElasticSWave.contactInsertionAmplitude g h mu p) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.local_interaction_equations_iff_source_amplitudes -- With g=h=p=1, mu=0, the single insertion is i/2, not a one-sided -- dressing or the difference after resumming g+h to all orders. example : let f0 : Complex := (-1 + Complex.I) / 2 let f1 : Complex := Complex.I / 2 f0 + Complex.I * f0 = -1 /\ f1 + Complex.I * f1 = -(1 + Complex.I * f0) /\ f1 ≠ f0 /\ f1 ≠ PhysicsLogic.Framework.ElasticSWave.contactAmplitude 2 0 1 - f0 := by norm_num [PhysicsLogic.Framework.ElasticSWave.contactAmplitude, PhysicsLogic.Framework.ElasticSWave.contactDenominator, Complex.ext_iff, Complex.div_re, Complex.div_im, Complex.normSq_apply, Complex.mul_re, Complex.mul_im] #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.local_interaction_equations_iff_source_amplitudes #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_and_local_equations_control_the_pionless_expansion #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.matching_derives_first_order_treatment_and_amplitudes #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.first_order_counting_context_characterization #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.first_order_treatment_contract_iff_numerical_suppression example : forall (g h mu p : Real) (f0 f1 : Complex), (f0 + (g : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * f0 = -(g : Complex) /\ f1 + (g : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * f1 = -(h : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * f0)) ↔ (forall t : Real, (f0 + (t : Complex) * f1) + ((g + t * h : Real) : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * (f0 + (t : Complex) * f1) + ((g + t * h : Real) : Complex) = (t : Complex) ^ 2 * (h : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * f1) := PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.local_equations_iff_quadratic_scattering_residual -- The actual first-order solution has a nonzero quadratic residual at t=1. example (t : Real) : let f0 : Complex := (-1 + Complex.I) / 2 let f1 : Complex := Complex.I / 2 (f0 + (t : Complex) * f1) + ((1 + t : Real) : Complex) * Complex.I * (f0 + (t : Complex) * f1) + ((1 + t : Real) : Complex) = -(t : Complex) ^ 2 / 2 := by dsimp push_cast apply Complex.ext <;> norm_num [Complex.div_re, Complex.div_im, Complex.normSq_apply, Complex.mul_re, Complex.mul_im, pow_two] <;> ring -- A single test at t=1 can satisfy the full scattering equation while the -- alleged leading term fails already at t=0. Universal coefficient content matters. example : let f0 : Complex := 0 let f1 : Complex := (-1 + Complex.I) / 2 (f0 + f1) + Complex.I * (f0 + f1) + 1 = 0 /\ f0 + Complex.I * f0 + 1 ≠ 0 := by norm_num [Complex.ext_iff, Complex.div_re, Complex.div_im, Complex.normSq_apply, Complex.mul_re, Complex.mul_im] #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.ContactChains.local_equations_iff_quadratic_scattering_residual