Degree-uniform endgame and verified first-origin/centered extensions

.gitattributes

@@ -0,0 +1,2 @@
+# Preserve captured verification logs verbatim, including trailing blank lines.
+research/**/*.log -whitespace

.github/workflows/lean_action_ci.yml

@@ -20,6 +20,6 @@ jobs:
       # The repository's trust policy, enforced: no `sorry` outside the two
       # deliberate holes in Challenge.lean, no project-defined axiom, no
       # native_decide, no unsafe, no floating point, and the top-level results
-      # depending on the three standard axioms only.  See docs/design.md §8.
+      # depending on the three standard axioms only.  See docs/design.md.
       - name: Trust audit
         run: bash scripts/audit.sh

.gitignore

@@ -1 +1,9 @@
-/.lake
+# Build outputs and local dependency environments (including research stages).
+.lake/
+.venv/
+__pycache__/
+.pytest_cache/
+.mypy_cache/
+.ruff_cache/
+*.pyc
+*.pyo

Sendov.lean

@@ -1,75 +1,2 @@
-import Sendov.Common.Basic
-import Sendov.Common.Rpow
-import Sendov.Common.Quadratic
-import Sendov.Common.Chord
-import Sendov.FiniteRange.Batch
-import Sendov.FiniteRange.Moments
-import Sendov.FiniteRange.OddBound
-import Sendov.FiniteRange.Pack
-import Sendov.FiniteRange.Recurrence
-import Sendov.FiniteRange.PackBridge
-import Sendov.FiniteRange.Reduce
-import Sendov.FiniteRange.Degree5
-import Sendov.FiniteRange.Degree6
-import Sendov.FiniteRange.Degree7
-import Sendov.FiniteRange.Degree8
-import Sendov.FiniteRange.Degree20
-import Sendov.FiniteRange.Degree20Packed
-import Sendov.FiniteRange.Degree53Packed
-import Sendov.FiniteRange.Degree97Packed
-import Sendov.FiniteRange.Degree6_6
-import Sendov.FiniteRange.Degree8_9
-import Sendov.FiniteRange.Degree10_11
-import Sendov.FiniteRange.Degree12_13
-import Sendov.FiniteRange.Degree14_15
-import Sendov.FiniteRange.Degree16_18
-import Sendov.FiniteRange.Degree18_20
-import Sendov.FiniteRange.Degree20_22
-import Sendov.FiniteRange.Degree22_24
-import Sendov.FiniteRange.Degree24_26
-import Sendov.FiniteRange.Degree26_27
-import Sendov.FiniteRange.Degree28_29
-import Sendov.FiniteRange.Degree30_31
-import Sendov.FiniteRange.Degree32_33
-import Sendov.FiniteRange.Degree34_35
-import Sendov.FiniteRange.Degree36_37
-import Sendov.FiniteRange.Degree38_39
-import Sendov.FiniteRange.Degree40_41
-import Sendov.FiniteRange.Degree42_43
-import Sendov.FiniteRange.Degree44_45
-import Sendov.FiniteRange.Degree46_47
-import Sendov.FiniteRange.Degree48_49
-import Sendov.FiniteRange.Degree50_51
-import Sendov.FiniteRange.Degree52_53
-import Sendov.FiniteRange.Degree54_55
-import Sendov.FiniteRange.Degree56_58
-import Sendov.FiniteRange.Degree58_60
-import Sendov.FiniteRange.Degree60_63
-import Sendov.FiniteRange.Degree64_69
-import Sendov.FiniteRange.Degree70_79
-import Sendov.FiniteRange.Degree80_100
-import Sendov.LargeDegree.Tail
-import Sendov.FiniteRange.Cover
-import Sendov.LargeDegree.Monotone
-import Sendov.LargeDegree.Endgame
-import Sendov.Main
-import Sendov.Common.Sinh
-import Sendov.Reduction.Setup
-import Sendov.Reduction.Polar
-import Sendov.Reduction.BetaBound
-import Sendov.Reduction.Stat
-import Sendov.Reduction.Simplified
-import Sendov.Reduction.Alpha17
-import Sendov.Reduction.Main
-import Sendov.Analytic.Maclaurin
-import Sendov.Analytic.Defect
-import Sendov.Counterexample.Factor
-import Sendov.Counterexample.Identities
-import Sendov.Analytic.Polar
-import Sendov.Analytic.Origin
-import Sendov.Analytic.Jsum
-import Sendov.Analytic.OriginExact
-import Sendov.Analytic.LowDegree
-import Sendov.Interior
-import Sendov.Boundary
 import Sendov.Conjecture
+import Sendov.Collinear.Moment

Sendov/Analytic/Defect.lean

@@ -47,24 +47,14 @@ open Multiset
 /-! ### Products of norms -/
 
 lemma prod_norm_nonneg (s : Multiset ℂ) : 0 ≤ (s.map (fun z => ‖z‖)).prod := by
-  refine Multiset.prod_nonneg ?_
-  intro y hy
-  obtain ⟨z, _, rfl⟩ := Multiset.mem_map.1 hy
-  exact norm_nonneg z
+  exact Multiset.prod_map_nonneg (fun z _ => norm_nonneg z)
 
 lemma prod_norm_le_one : ∀ (s : Multiset ℂ), (∀ z ∈ s, ‖z‖ ≤ 1) →
     (s.map (fun z => ‖z‖)).prod ≤ 1 := by
-  intro s
-  induction s using Multiset.induction_on with
-  | empty => intro _; simp
-  | cons w t ih =>
-    intro hs
-    have hw : ‖w‖ ≤ 1 := hs w (mem_cons_self w t)
-    have ht : ∀ z ∈ t, ‖z‖ ≤ 1 := fun z hz => hs z (mem_cons_of_mem hz)
-    have hIH := ih ht
-    have hP0 : 0 ≤ (t.map (fun z => ‖z‖)).prod := prod_norm_nonneg t
-    simp only [Multiset.map_cons, Multiset.prod_cons]
-    nlinarith [norm_nonneg w]
+  intro s hs
+  simpa [normHom] using
+    (Multiset.prod_map_le_pow_card (f := (normHom : ℂ →*₀ ℝ))
+      (fun z _ => norm_nonneg z) hs)
 
 /-! ### The pointwise fact -/
 
@@ -74,18 +64,12 @@ lemma norm_mul_norm_inv_sub_conj_le {w : ℂ} (hw : ‖w‖ ≤ 1) :
     ‖w‖ * ‖w⁻¹ - (starRingEnd ℂ) w‖ ≤ 1 - ‖w‖ ^ 2 := by
   rcases eq_or_ne w 0 with rfl | hne
   · simp
-  · have hkey : w * (w⁻¹ - (starRingEnd ℂ) w) = 1 - ((‖w‖ : ℝ) : ℂ) ^ 2 := by
-      rw [mul_sub, mul_inv_cancel₀ hne, Complex.mul_conj]
-      norm_cast
-      rw [Complex.normSq_eq_norm_sq]
-    have h1 : ‖w‖ * ‖w⁻¹ - (starRingEnd ℂ) w‖ = ‖(1 : ℂ) - ((‖w‖ : ℝ) : ℂ) ^ 2‖ := by
-      rw [← norm_mul, hkey]
-    rw [h1]
-    have h2 : ((1 : ℂ) - ((‖w‖ : ℝ) : ℂ) ^ 2) = ((1 - ‖w‖ ^ 2 : ℝ) : ℂ) := by
+  · have hkey : w * (w⁻¹ - (starRingEnd ℂ) w) = ((1 - ‖w‖ ^ 2 : ℝ) : ℂ) := by
+      rw [mul_sub, mul_inv_cancel₀ hne, Complex.mul_conj, Complex.normSq_eq_norm_sq]
       push_cast
-      ring
-    rw [h2, Complex.norm_real, Real.norm_eq_abs,
-      abs_of_nonneg (by nlinarith [norm_nonneg w])]
+      rfl
+    rw [← norm_mul, hkey, Complex.norm_real, Real.norm_eq_abs,
+      abs_of_nonneg (sub_nonneg.2 (pow_le_one₀ (norm_nonneg w) hw))]
 
 /-! ### The lemma -/
 

Sendov/Analytic/FirstOriginAlgebra.lean

@@ -0,0 +1,122 @@
+import Sendov.Analytic.Origin
+
+/-! Finite polynomial integrals and positive decompositions for degrees five and six.
+No sampling, general Bernstein framework, or endpoint strictness assumptions. -/
+
+namespace Sendov.FirstOriginSmall
+
+noncomputable def B (a t : ℝ) : ℝ := 1 - a * (1 + a) * t + a ^ 2 * t ^ 2
+noncomputable def Q (a : ℝ) : ℝ :=
+  120 + 170 * a + 102 * a ^ 2 - 29 * a ^ 3 - 117 * a ^ 4 - 93 * a ^ 5 - 61 * a ^ 6 + 13 * a ^ 7 + 25 * a ^ 8 + 9 * a ^ 9 + a ^ 10
+
+lemma integral_quadratic_cube (c d e : ℝ) :
+    (∫ t in (0 : ℝ)..1, (c + d * t + e * t ^ 2) ^ 3) =
+      c ^ 3 + 3 * c ^ 2 * d / 2 + (3 * c ^ 2 * e + 3 * c * d ^ 2) / 3 + (6 * c * d * e + d ^ 3) / 4 + (3 * c * e ^ 2 + 3 * d ^ 2 * e) / 5 + 3 * d * e ^ 2 / 6 + e ^ 3 / 7 := by
+  have hex : (fun t : ℝ => (c + d * t + e * t ^ 2) ^ 3) =
+      (fun t => c ^ 3 + (3 * c ^ 2 * d) * t ^ 1 + (3 * c ^ 2 * e + 3 * c * d ^ 2) * t ^ 2 + (6 * c * d * e + d ^ 3) * t ^ 3 + (3 * c * e ^ 2 + 3 * d ^ 2 * e) * t ^ 4 + (3 * d * e ^ 2) * t ^ 5 + e ^ 3 * t ^ 6) := by
+    funext t; ring
+  rw [hex]
+  simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _)
+    only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul,
+      intervalIntegral.integral_const, integral_pow, integral_id]
+  norm_num
+  <;> ring
+
+lemma integral_t_quadratic_sq (c d e : ℝ) :
+    (∫ t in (0 : ℝ)..1, t * (c + d * t + e * t ^ 2) ^ 2) =
+      c ^ 2 / 2 + 2 * c * d / 3 + (2 * c * e + d ^ 2) / 4 + 2 * d * e / 5 + e ^ 2 / 6 := by
+  have hex : (fun t : ℝ => t * (c + d * t + e * t ^ 2) ^ 2) =
+      (fun t => c ^ 2 * t ^ 1 + (2 * c * d) * t ^ 2 + (2 * c * e + d ^ 2) * t ^ 3 + (2 * d * e) * t ^ 4 + e ^ 2 * t ^ 5) := by
+    funext t; ring
+  rw [hex]
+  simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _)
+    only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow, integral_id]
+  norm_num
+  <;> ring
+
+lemma integral_t_linear_fifth (a : ℝ) :
+    (∫ t in (0 : ℝ)..1, t * (1 - a * t) ^ 5) =
+      1 / 2 - 5 * a / 3 + 5 * a ^ 2 / 2 - 2 * a ^ 3 + 5 * a ^ 4 / 6 - a ^ 5 / 7 := by
+  have hex : (fun t : ℝ => t * (1 - a * t) ^ 5) =
+      (fun t => t + (-5 * a) * t ^ 2 + (10 * a ^ 2) * t ^ 3 + (-10 * a ^ 3) * t ^ 4 + (5 * a ^ 4) * t ^ 5 + (-a ^ 5) * t ^ 6) := by
+    funext t; ring
+  rw [hex]
+  simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _)
+    only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow, integral_id]
+  norm_num
+  <;> ring
+
+lemma integral_sq_linear_cube (a : ℝ) :
+    (∫ t in (0 : ℝ)..1, t ^ 2 * (1 - a * t) ^ 3) = 1 / 3 - 3 * a / 4 + 3 * a ^ 2 / 5 - a ^ 3 / 6 := by
+  have hex : (fun t : ℝ => t ^ 2 * (1 - a * t) ^ 3) =
+      (fun t => t ^ 2 + (-3 * a) * t ^ 3 + (3 * a ^ 2) * t ^ 4 + (-a ^ 3) * t ^ 5) := by
+    funext t; ring
+  rw [hex]
+  simp (disch := exact Continuous.intervalIntegrable (by fun_prop) _ _)
+    only [intervalIntegral.integral_add, intervalIntegral.integral_const_mul, integral_pow]
+  norm_num
+  <;> ring
+
+lemma polar_cube_integral (a : ℝ) :
+    1 - (∫ t in (0 : ℝ)..1, Ppolar a ((1 + a) / 2) t ^ (3 : ℕ)) = (1 - a) ^ 2 * Q a / 140 := by
+  have hp : (fun t => Ppolar a ((1 + a) / 2) t) =
+      (fun t => a ^ 2 + (a * (1 - a ^ 2) * (1 + a)) * t + (1 - a ^ 2) ^ 2 * t ^ 2) := by
+    funext t; unfold Ppolar; ring
+  simp_rw [hp]
+  rw [integral_quadratic_cube]
+  unfold Q
+  ring
+
+lemma Q_lower {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) : 92 ≤ Q a := by
+  have h3 : a ^ 3 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 3)
+  have h4 : a ^ 4 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 4)
+  have h5 : a ^ 5 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 5)
+  have h6 : a ^ 6 ≤ a ^ 2 := pow_le_pow_of_le_one ha0 ha1 (by omega : 2 ≤ 6)
+  have h2 : a ^ 2 ≤ a := by nlinarith
+  unfold Q
+  nlinarith [pow_nonneg ha0 7, pow_nonneg ha0 8, pow_nonneg ha0 9, pow_nonneg ha0 10]
+
+lemma polar_cube_lt_one {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    (∫ t in (0 : ℝ)..1, Ppolar a ((1 + a) / 2) t ^ (3 : ℕ)) < 1 := by
+  have hQ := Q_lower ha0.le ha1.le
+  have h := polar_cube_integral a
+  have hg : 0 < (1 - a) ^ 2 * Q a := mul_pos (sq_pos_of_pos (by linarith)) (by linarith)
+  linarith
+
+lemma fifth_sixth_majorant {y : ℝ} (hy : 0 ≤ y) : 6 * y ^ 5 ≤ 1 + 5 * y ^ 6 := by
+  have hid : 1 + 5 * y ^ 6 - 6 * y ^ 5 = (y - 1) ^ 2 * (5 * y ^ 4 + 4 * y ^ 3 + 3 * y ^ 2 + 2 * y + 1) := by ring
+  have hp : 0 ≤ (y - 1) ^ 2 * (5 * y ^ 4 + 4 * y ^ 3 + 3 * y ^ 2 + 2 * y + 1) := by positivity
+  linarith
+
+lemma five_halves_majorant {u w : ℝ} (hu : 0 ≤ u) (huw : u ≤ w) (hw : w ≤ 1) :
+    w ^ 5 ≤ u ^ 5 + (5 / 2 : ℝ) * u ^ 3 * (w ^ 2 - u ^ 2) + (15 / 8 : ℝ) * (w ^ 2 - u ^ 2) ^ 2 := by
+  have hid : u ^ 5 + (5 / 2 : ℝ) * u ^ 3 * (w ^ 2 - u ^ 2) + (15 / 8 : ℝ) * (w ^ 2 - u ^ 2) ^ 2 - w ^ 5 =
+      (15 / 8 : ℝ) * (1 - w) * (w ^ 2 - u ^ 2) ^ 2 + (w - u) ^ 3 * (5 * u ^ 2 + (35 / 8 : ℝ) * u * (w - u) + (7 / 8 : ℝ) * (w - u) ^ 2) := by ring
+  have hd : 0 ≤ w - u := sub_nonneg.mpr huw
+  have hp : 0 ≤ (15 / 8 : ℝ) * (1 - w) * (w ^ 2 - u ^ 2) ^ 2 + (w - u) ^ 3 * (5 * u ^ 2 + (35 / 8 : ℝ) * u * (w - u) + (7 / 8 : ℝ) * (w - u) ^ 2) := by
+    have : 0 ≤ 1 - w := sub_nonneg.mpr hw
+    positivity
+  linarith
+
+lemma upper_five_gap {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    (1 - a) ^ 2 + 5 * a ^ 2 * (∫ t in (0 : ℝ)..1, t * (B a t) ^ 2) < 1 - 5 * a / 6 := by
+  have he : (fun t => B a t) = (fun t => 1 + (-a * (1 + a)) * t + a ^ 2 * t ^ 2) := by
+    funext t; unfold B; ring
+  simp_rw [he]
+  rw [integral_t_quadratic_sq]
+  have hh : 0 < 1 - a := by linarith
+  have hp : 0 < a * (1 - a) * (14 * (1 - a) ^ 4 + 28 * a * (1 - a) ^ 3 + 12 * a ^ 2 * (1 - a) ^ 2 + 3 * a ^ 3 * (1 - a) + 6 * a ^ 4) / 12 := by positivity
+  have hid : 1 - 5 * a / 6 - ((1 - a) ^ 2 + 5 * a ^ 2 * (1 ^ 2 / 2 + 2 * 1 * (-a * (1 + a)) / 3 + (2 * 1 * a ^ 2 + (-a * (1 + a)) ^ 2) / 4 + 2 * (-a * (1 + a)) * a ^ 2 / 5 + (a ^ 2) ^ 2 / 6)) =
+      a * (1 - a) * (14 * (1 - a) ^ 4 + 28 * a * (1 - a) ^ 3 + 12 * a ^ 2 * (1 - a) ^ 2 + 3 * a ^ 3 * (1 - a) + 6 * a ^ 4) / 12 := by ring
+  linarith
+
+lemma upper_six_gap {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
+    (1 - a) ^ 3 + 6 * a ^ 2 * ((∫ t in (0 : ℝ)..1, t * (1 - a * t) ^ 5) + (5 / 2 : ℝ) * a * (1 - a) * (∫ t in (0 : ℝ)..1, t ^ 2 * (1 - a * t) ^ 3) + (15 / 32 : ℝ) * a ^ 2 * (1 - a) ^ 2) < 1 - 6 * a / 7 := by
+  rw [integral_t_linear_fifth, integral_sq_linear_cube]
+  have hh : 0 < 1 - a := by linarith
+  have hp : 0 < a * (1 - a) * (240 * (1 - a) ^ 5 + 768 * a * (1 - a) ^ 4 + 912 * a ^ 2 * (1 - a) ^ 3 + 593 * a ^ 3 * (1 - a) ^ 2 + 93 * a ^ 4 * (1 - a) + 68 * a ^ 5) / 112 := by positivity
+  have hid : 1 - 6 * a / 7 - ((1 - a) ^ 3 + 6 * a ^ 2 * ((1 / 2 - 5 * a / 3 + 5 * a ^ 2 / 2 - 2 * a ^ 3 + 5 * a ^ 4 / 6 - a ^ 5 / 7) + (5 / 2 : ℝ) * a * (1 - a) * (1 / 3 - 3 * a / 4 + 3 * a ^ 2 / 5 - a ^ 3 / 6) + (15 / 32 : ℝ) * a ^ 2 * (1 - a) ^ 2)) =
+      a * (1 - a) * (240 * (1 - a) ^ 5 + 768 * a * (1 - a) ^ 4 + 912 * a ^ 2 * (1 - a) ^ 3 + 593 * a ^ 3 * (1 - a) ^ 2 + 93 * a ^ 4 * (1 - a) + 68 * a ^ 5) / 112 := by ring
+  linarith
+
+end Sendov.FirstOriginSmall