2607.19268v1 / CoreAlgebra.lean
all files
import Mathlib
/-!
# Checked algebra from the core extremal argument
These lemmas formalize sign computations used in Lemma 4.1 and the
`n = 15`, `k ∈ {5,6,7}` subcase of Lemma 5.4. The latter is only
reported as a direct substitution in the paper.
-/
namespace BootsRoyleCaoVince.CoreAlgebra
lemma case2_cubic_one_pos {t : ℝ} (ht : 13 / 2 < t) :
0 < 17 * t ^ 3 - 127 * t ^ 2 + 321 * t - 390 := by
have hu : 0 < t - 13 / 2 := by linarith
calc
17 * t ^ 3 - 127 * t ^ 2 + 321 * t - 390 =
17 * (t - 13 / 2) ^ 3 + (409 / 2) * (t - 13 / 2) ^ 2 +
(3299 / 4) * (t - 13 / 2) + 7995 / 8 := by ring
_ > 0 := by positivity
lemma case2_cubic_two_pos {t : ℝ} (ht : 13 / 2 < t) :
0 < 5 * t ^ 3 - 46 * t ^ 2 + 120 * t - 174 := by
have hu : 0 < t - 13 / 2 := by linarith
calc
5 * t ^ 3 - 46 * t ^ 2 + 120 * t - 174 =
5 * (t - 13 / 2) ^ 3 + (103 / 2) * (t - 13 / 2) ^ 2 +
(623 / 4) * (t - 13 / 2) + 285 / 8 := by ring
_ > 0 := by positivity
lemma coefficient_case_boundary_pos {t : ℝ} (ht : 13 / 2 < t) :
0 < t ^ 3 - 5 * t ^ 2 - 11 * t + 10 := by
have hu : 0 < t - 13 / 2 := by linarith
calc
t ^ 3 - 5 * t ^ 2 - 11 * t + 10 =
(t - 13 / 2) ^ 3 + (29 / 2) * (t - 13 / 2) ^ 2 +
(203 / 4) * (t - 13 / 2) + 15 / 8 := by ring
_ > 0 := by positivity
lemma case3_discriminant_factor_pos {t : ℝ} (ht : 13 / 2 < t) :
0 < 5 * t ^ 4 - 26 * t ^ 3 - 43 * t ^ 2 + 96 * t - 480 := by
have hu : 0 < t - 13 / 2 := by linarith
calc
5 * t ^ 4 - 26 * t ^ 3 - 43 * t ^ 2 + 96 * t - 480 =
5 * (t - 13 / 2) ^ 4 + 104 * (t - 13 / 2) ^ 3 +
(1435 / 2) * (t - 13 / 2) ^ 2 + 1734 * (t - 13 / 2) + 1797 / 16 := by ring
_ > 0 := by positivity
lemma case4_discriminant_factor_pos {t : ℝ} (ht : 13 / 2 < t) :
0 < 47 * t ^ 6 - 516 * t ^ 5 + 988 * t ^ 4 + 5652 * t ^ 3 -
25720 * t ^ 2 + 39744 * t - 26244 := by
have hu : 0 < t - 13 / 2 := by linarith
calc
47 * t ^ 6 - 516 * t ^ 5 + 988 * t ^ 4 + 5652 * t ^ 3 -
25720 * t ^ 2 + 39744 * t - 26244 =
47 * (t - 13 / 2) ^ 6 + 1317 * (t - 13 / 2) ^ 5 +
(56017 / 4) * (t - 13 / 2) ^ 4 + (142955 / 2) * (t - 13 / 2) ^ 3 +
(2821697 / 16) * (t - 13 / 2) ^ 2 +
(2778421 / 16) * (t - 13 / 2) + 1205279 / 64 := by ring
_ > 0 := by positivity
/-- The quadratic upper bound `F_t(θ)` introduced in the last case of Lemma 5.4. -/
noncomputable def F (t θ n : ℝ) : ℝ :=
((2 * n - 4) * θ - 1) / (t - 2) *
((t + 2) / (t + 1) - 2 * θ / 3 + 8 / (3 * (2 * n - 4))) +
(n - 6 - ((2 * n - 4) * θ - 1) * t / (t - 2)) *
((1 - 5 * θ / 11) / (t + 1)) +
(n - 5) / (t + 1) - θ - (t - 4)
private lemma common_denominator_pos {t : ℝ} (ht : 13 / 2 < t) :
0 < (t - 2) * (t + 1) := by
have h1 : 0 < t - 2 := by linarith
have h2 : 0 < t + 1 := by linarith
exact mul_pos h1 h2
lemma F_five_twentySixths_neg {t : ℝ} (ht : 13 / 2 < t)
(hrel : t ^ 2 - 3 * t = 23) : F t (5 / 26) 15 < 0 := by
have ht2 : t - 2 ≠ 0 := by linarith
have ht1 : t + 1 ≠ 0 := by linarith
have heq : F t (5 / 26) 15 =
(4661 / 858 - (61 / 66) * t) / ((t - 2) * (t + 1)) := by
apply (eq_div_iff (mul_ne_zero ht2 ht1)).2
dsimp [F]
field_simp
nlinarith
rw [heq]
exact div_neg_of_neg_of_pos (by nlinarith) (common_denominator_pos ht)
lemma F_three_thirteenths_neg {t : ℝ} (ht : 13 / 2 < t)
(hrel : t ^ 2 - 3 * t = 23) : F t (3 / 13) 15 < 0 := by
have ht2 : t - 2 ≠ 0 := by linarith
have ht1 : t + 1 ≠ 0 := by linarith
have heq : F t (3 / 13) 15 =
(2911 / 429 - (488 / 429) * t) / ((t - 2) * (t + 1)) := by
apply (eq_div_iff (mul_ne_zero ht2 ht1)).2
dsimp [F]
field_simp
nlinarith
rw [heq]
exact div_neg_of_neg_of_pos (by nlinarith) (common_denominator_pos ht)
lemma F_seven_twentySixths_neg {t : ℝ} (ht : 13 / 2 < t)
(hrel : t ^ 2 - 3 * t = 23) : F t (7 / 26) 15 < 0 := by
have ht2 : t - 2 ≠ 0 := by linarith
have ht1 : t + 1 ≠ 0 := by linarith
have heq : F t (7 / 26) 15 =
(2313 / 286 - (391 / 286) * t) / ((t - 2) * (t + 1)) := by
apply (eq_div_iff (mul_ne_zero ht2 ht1)).2
dsimp [F]
field_simp
nlinarith
rw [heq]
exact div_neg_of_neg_of_pos (by nlinarith) (common_denominator_pos ht)
/-- The paper's `r₁₅`. -/
noncomputable def r15 : ℝ := (3 + √101) / 2
lemma r15_relation : r15 ^ 2 - 3 * r15 = 23 := by
have hs : (√(101 : ℝ)) ^ 2 = 101 := Real.sq_sqrt (by norm_num)
dsimp [r15]
nlinarith
lemma r15_gt_thirteen_halves : 13 / 2 < r15 := by
have hs : (√(101 : ℝ)) ^ 2 = 101 := Real.sq_sqrt (by norm_num)
have hp : 0 ≤ √(101 : ℝ) := Real.sqrt_nonneg _
dsimp [r15]
nlinarith
theorem omitted_n15_checks :
F r15 (5 / 26) 15 < 0 ∧ F r15 (6 / 26) 15 < 0 ∧ F r15 (7 / 26) 15 < 0 := by
have ht := r15_gt_thirteen_halves
have hr := r15_relation
refine ⟨F_five_twentySixths_neg ht hr, ?_, F_seven_twentySixths_neg ht hr⟩
have hmiddle := F_three_thirteenths_neg ht hr
norm_num at hmiddle ⊢
exact hmiddle
#print axioms omitted_n15_checks
end BootsRoyleCaoVince.CoreAlgebra