2607.19268v1 / BootsRoyle/Arithmetic.lean

all files

import Mathlib

/-!
# Arithmetic inequalities in the Boots--Royle/Cao--Vince proof

The graph-theoretic part of the argument reduces twice to a two-variable
linear optimization.  This file records the paper's scalar quantities and
kernel-checks the elementary facts about the comparison root

`r n = (3 + √(8n - 19)) / 2`.
-/

namespace BootsRoyle

/-- The comparison value called `r_n` in the paper. -/
noncomputable def comparisonRoot (n : ℕ) : ℝ :=
  (3 + √(8 * (n : ℝ) - 19)) / 2

/-- The lower bound for the total Perron weight on cubic vertices. -/
noncomputable def cubicWeightLowerBound (n k : ℕ) (t : ℝ) : ℝ :=
  (k : ℝ) / (2 * (n : ℝ) - k - 4 + 3 * k / t)

/-- The coefficient `α_k` (with the paper's special values at `k=1,2`). -/
noncomputable def alpha (k : ℕ) : ℝ :=
  if k ≤ 2 then 0 else (2 * (k : ℝ) - 5) / (2 * k + 1)

/-- The nonnegative part of the coefficient `γ_k`. -/
noncomputable def gamma (k : ℕ) : ℝ :=
  if k ≤ 6 then 0 else 2 * ((k : ℝ) - 6) / (3 * k)

/-- The nonnegative part of the outerplanar coefficient `γ'_k`. -/
noncomputable def gammaOuter (k : ℕ) : ℝ :=
  if k ≤ 4 then 0 else 2 * ((k : ℝ) - 4) / (3 * k)

lemma comparisonRoot_radicand_nonneg {n : ℕ} (hn : 3 ≤ n) :
    0 ≤ 8 * (n : ℝ) - 19 := by
  exact_mod_cast (show (0 : ℤ) ≤ 8 * (n : ℤ) - 19 by omega)

lemma comparisonRoot_sq_sqrt {n : ℕ} (hn : 3 ≤ n) :
    (√(8 * (n : ℝ) - 19)) ^ 2 = 8 * n - 19 := by
  rw [Real.sq_sqrt (comparisonRoot_radicand_nonneg hn)]

lemma comparisonRoot_quadratic {n : ℕ} (hn : 3 ≤ n) :
    comparisonRoot n ^ 2 - 3 * comparisonRoot n = 2 * n - 7 := by
  have hs := comparisonRoot_sq_sqrt hn
  rw [comparisonRoot]
  nlinarith

lemma comparisonRoot_pos {n : ℕ} :
    0 < comparisonRoot n := by
  rw [comparisonRoot]
  have := Real.sqrt_nonneg (8 * (n : ℝ) - 19)
  positivity

lemma comparisonRoot_gt_thirteen_halves {n : ℕ} (hn : 15 ≤ n) :
    (13 : ℝ) / 2 < comparisonRoot n := by
  have hn3 : 3 ≤ n := by omega
  have hs := comparisonRoot_sq_sqrt hn3
  have hsnonneg := Real.sqrt_nonneg (8 * (n : ℝ) - 19)
  have hnreal : (15 : ℝ) ≤ n := by exact_mod_cast hn
  rw [comparisonRoot]
  nlinarith

lemma comparisonRoot_gt_five {n : ℕ} (hn : 10 ≤ n) :
    5 < comparisonRoot n := by
  have hn3 : 3 ≤ n := by omega
  have hs := comparisonRoot_sq_sqrt hn3
  have hsnonneg := Real.sqrt_nonneg (8 * (n : ℝ) - 19)
  have hnreal : (10 : ℝ) ≤ n := by exact_mod_cast hn
  rw [comparisonRoot]
  nlinarith

lemma comparisonRoot_lt_n_sub_two {n : ℕ} (hn : 10 ≤ n) :
    comparisonRoot n < n - 2 := by
  have hquad := comparisonRoot_quadratic (show 3 ≤ n by omega)
  have ht := comparisonRoot_gt_five hn
  have hnreal : (10 : ℝ) ≤ n := by exact_mod_cast hn
  nlinarith [sq_nonneg (comparisonRoot n - (n - 2))]

lemma alpha_eq_zero {k : ℕ} (hk : k ≤ 2) : alpha k = 0 := by
  simp [alpha, hk]

lemma alpha_eq {k : ℕ} (hk : 3 ≤ k) :
    alpha k = (2 * (k : ℝ) - 5) / (2 * k + 1) := by
  simp [alpha, show ¬k ≤ 2 by omega]

lemma gamma_eq_zero {k : ℕ} (hk : k ≤ 6) : gamma k = 0 := by
  simp [gamma, hk]

lemma gamma_eq {k : ℕ} (hk : 7 ≤ k) :
    gamma k = 2 * ((k : ℝ) - 6) / (3 * k) := by
  simp [gamma, show ¬k ≤ 6 by omega]

lemma gammaOuter_eq_zero {k : ℕ} (hk : k ≤ 4) : gammaOuter k = 0 := by
  simp [gammaOuter, hk]

lemma gammaOuter_eq {k : ℕ} (hk : 5 ≤ k) :
    gammaOuter k = 2 * ((k : ℝ) - 4) / (3 * k) := by
  simp [gammaOuter, show ¬k ≤ 4 by omega]

lemma cubicWeightLowerBound_bounds {n k : ℕ} {t : ℝ}
    (hk : 0 < k) (hkmax : 3 * k ≤ 2 * n - 4) (ht : 3 < t) :
    (k : ℝ) / (2 * n - 4) < cubicWeightLowerBound n k t ∧
      cubicWeightLowerBound n k t < 1 / 2 := by
  have hkR : (0 : ℝ) < k := by exact_mod_cast hk
  have hn4 : 4 ≤ 2 * n := by omega
  have hkmax' : (3 : ℝ) * k ≤ 2 * n - 4 := by
    have hcast : ((3 * k : ℕ) : ℝ) ≤ ((2 * n - 4 : ℕ) : ℝ) :=
      Nat.cast_le.mpr hkmax
    simpa [Nat.cast_sub hn4] using hcast
  have ht0 : 0 < t := lt_trans (by norm_num) ht
  let D : ℝ := 2 * n - k - 4 + 3 * k / t
  have hfracpos : 0 < (3 : ℝ) * k / t := div_pos (mul_pos (by norm_num) hkR) ht0
  have hfraclt : (3 : ℝ) * k / t < k := by
    rw [div_lt_iff₀ ht0]
    nlinarith
  have hDpos : 0 < D := by
    dsimp [D]
    nlinarith
  have htotalpos : 0 < (2 : ℝ) * n - 4 := by
    nlinarith
  have hDlt : D < 2 * n - 4 := by
    dsimp [D]
    nlinarith
  constructor
  · rw [cubicWeightLowerBound]
    exact (div_lt_div_iff_of_pos_left hkR htotalpos hDpos).mpr hDlt
  · rw [cubicWeightLowerBound, div_lt_iff₀ hDpos]
    dsimp [D]
    nlinarith

/-- The first branch of the two-variable linear optimization used in
Lemma 4.1.  It is stated independently of the graph parameters so the
algebraic certificate is transparent. -/
lemma linearObjective_upper_of_nonnegative_slope
    {a k t A B s z : ℝ}
    (ht : 2 < t) (hk : 0 ≤ k)
    (hs : (t + 1) * s ≤ A)
    (hsz : t * s + (t - 2) * z ≤ B)
    (hslope : 0 ≤ a - k * t / (t - 2)) :
    a * s + k * z ≤
      (a - k * t / (t - 2)) * (A / (t + 1)) + k * B / (t - 2) := by
  have ht2 : 0 < t - 2 := by linarith
  have ht1 : 0 < t + 1 := by linarith
  have hz : z ≤ (B - t * s) / (t - 2) := by
    rw [le_div_iff₀ ht2]
    linarith
  have hs' : s ≤ A / (t + 1) := by
    rw [le_div_iff₀ ht1]
    simpa [mul_comm] using hs
  calc
    a * s + k * z ≤ a * s + k * ((B - t * s) / (t - 2)) := by
      gcongr
    _ = (a - k * t / (t - 2)) * s + k * B / (t - 2) := by
      field_simp
      ring
    _ ≤ (a - k * t / (t - 2)) * (A / (t + 1)) + k * B / (t - 2) := by
      gcongr

/-- The intersection of `z = s/2` with
`t s + (t-2)z = B`, used in the negative-slope branch. -/
lemma halfLine_intersection {t B : ℝ} (ht : 2 < t) :
    t * (2 * B / (3 * t - 2)) +
        (t - 2) * (B / (3 * t - 2)) = B := by
  have hden : 3 * t - 2 ≠ 0 := by linarith
  have hden' : -2 + t * 3 ≠ 0 := by linarith
  have hinv : (-2 + t * 3)⁻¹ * (-2 + t * 3) = 1 :=
    inv_mul_cancel₀ hden'
  rw [show 3 * t - 2 = -2 + t * 3 by ring]
  calc
    t * (2 * B / (-2 + t * 3)) +
        (t - 2) * (B / (-2 + t * 3)) =
        B * ((-2 + t * 3)⁻¹ * (-2 + t * 3)) := by ring
    _ = B := by rw [hinv, mul_one]

/-- The averaging calculation in Lemma 3.6.  `F` is the number of
faces of the core, `K` the number of occupied faces, `lam * L` their
total weight, and `lam - (lam + 3)L` the total weight of all faces. -/
lemma selectedFace_averaging
    {lam L K F : ℝ}
    (hlam : 0 < lam) (hK : 0 < K) (hF : 0 < F)
    (haverage : lam * L / K ≥ (lam - (lam + 3) * L) / F) :
    K / (F + K + 3 * K / lam) ≤ L := by
  let D := F + K + 3 * K / lam
  have hD : 0 < D := by
    dsimp [D]
    positivity
  have havg' :
      K * (lam - (lam + 3) * L) ≤ F * (lam * L) := by
    have h := (div_le_div_iff₀ hF hK).mp haverage
    simpa [mul_comm] using h
  rw [div_le_iff₀ hD]
  dsimp [D]
  have hlam_ne : lam ≠ 0 := ne_of_gt hlam
  field_simp
  nlinarith

end BootsRoyle