CubicPathwidth.CutSweep.Deterministic

Source file CubicPathwidth/CutSweep/Deterministic.lean of the Lean project (how it is built).

import CubicPathwidth.CutSweep.Defs
import CubicPathwidth.T2.LayoutS

/-!
# Deterministic children of the cut sweep (N1, L1, L2)

Mirrors Section 3 (`sec:warmup`) of the manuscript:
* `constantClaim`: the constant paragraph of Section 3 (`sec:warmup`) (triple-angle formula);
* `layoutClaim`: Lemma 3.2 (`lem:warmup-layout`), pathwidth at most cutwidth;
* `orderingClaim`: ordering by distinct labels, prefix cuts are threshold counts.
-/

noncomputable section

namespace CubicPathwidth
namespace CutSweep

/-! ## N1: the constant -/

/-- `arccos(2√2/3) = arcsin(1/3)`. -/
theorem arccos_eq_arcsin_third :
    Real.arccos ((2 * Real.sqrt 2) / 3) = Real.arcsin (1 / 3) := by
  have h2 : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num)
  rw [Real.arccos_eq_arcsin (by positivity)]
  congr 1
  have : 1 - ((2 * Real.sqrt 2) / 3) ^ 2 = (1 / 3) ^ 2 := by
    rw [div_pow, mul_pow, h2]; norm_num
  rw [this, Real.sqrt_sq (by norm_num)]

/-- `1/3 < sin(π/9)`, by the triple-angle formula. -/
theorem one_third_lt_sin_pi_div_nine : (1 : ℝ) / 3 < Real.sin (Real.pi / 9) := by
  set s := Real.sin (Real.pi / 9) with hs
  have hpi := Real.pi_pos
  -- `3s - 4s³ = sin(π/3) = √3/2`
  have htriple : 3 * s - 4 * s ^ 3 = Real.sqrt 3 / 2 := by
    rw [hs, ← Real.sin_three_mul, ← Real.sin_pi_div_three]
    congr 1; ring
  -- `0 < s < sin(π/6) = 1/2`
  have hs0 : 0 < s := Real.sin_pos_of_pos_of_lt_pi (by positivity) (by linarith)
  have hs1 : s < 1 / 2 := by
    rw [← Real.sin_pi_div_six]
    exact Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith) (by linarith) (by linarith)
  have h3 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num)
  have h3n : 0 ≤ Real.sqrt 3 := Real.sqrt_nonneg 3
  by_contra hle
  rw [not_lt] at hle
  -- `h(x) = 3x - 4x³` is increasing on `[0, 1/2]`, so `h(s) ≤ h(1/3) = 23/27`
  have hmono : 3 * s - 4 * s ^ 3 ≤ 23 / 27 := by
    nlinarith [mul_nonneg hs0.le hs0.le, mul_nonneg (sub_nonneg.mpr hle) hs0.le,
      mul_nonneg (sub_nonneg.mpr hle) (mul_nonneg hs0.le hs0.le)]
  -- but `23/27 < √3/2` since `46² = 2116 < 2187 = 3 · 27²`
  rw [htriple] at hmono
  nlinarith

theorem constantClaim : ConstantClaim := by
  refine ⟨by rw [bisectionCoefficient, arccos_eq_arcsin_third], ?_⟩
  rw [bisectionCoefficient, arccos_eq_arcsin_third]
  have hpi := Real.pi_pos
  -- `c_* < 1/6 ⟺ arcsin(1/3) < π/9 ⟺ 1/3 < sin(π/9)`
  have harc : Real.arcsin (1 / 3) < Real.pi / 9 :=
    (Real.arcsin_lt_iff_lt_sin' ⟨by linarith, by linarith⟩).mpr one_third_lt_sin_pi_div_nine
  rw [div_mul_eq_mul_div, div_lt_iff₀ (by positivity)]
  linarith

/-! ## L1: pathwidth at most cutwidth (Lemma 3.2, `lem:warmup-layout`) -/

variable {n : ℕ}

/-- `|N(T) \ T| ≤ e(T)` for the level set `T = S_t`: every frontier vertex has
a neighbour in `T`, hence is the outer end of a crossing edge. -/
theorem outerFrontier_card_le_crossCount (G : SimpleGraph (Fin n)) (y : Fin n → ℝ) (t : ℝ) :
    (C3.outerFrontier G y t).card ≤ crossCount G y t := by
  classical
  unfold crossCount cutSize
  refine le_trans (Finset.card_le_card ?_) Finset.card_biUnion_le
  intro w hw
  simp only [C3.outerFrontier, Finset.mem_filter, Finset.mem_univ, true_and] at hw
  obtain ⟨htw, u, hu, hut⟩ := hw
  simp only [Finset.mem_biUnion, Finset.mem_sdiff, SimpleGraph.mem_neighborFinset, levelSet,
    Finset.mem_filter, Finset.mem_univ, true_and]
  exact ⟨u, hut, hu, not_le.mpr htw⟩

/-- Level sets of the position labels are prefixes. -/
theorem levelSet_position (σ : Fin n ≃ Fin n) (t : ℝ) :
    ∃ i : ℕ, levelSet (fun v => ((σ v : ℕ) : ℝ)) t = prefixSet σ i := by
  rcases lt_or_ge t 0 with ht | ht
  · refine ⟨0, ?_⟩
    ext v
    simp only [levelSet, prefixSet, Finset.mem_filter, Finset.mem_univ, true_and,
      Nat.not_lt_zero, iff_false, not_le]
    exact lt_of_lt_of_le ht (Nat.cast_nonneg _)
  · refine ⟨⌊t⌋₊ + 1, ?_⟩
    ext v
    simp only [levelSet, prefixSet, Finset.mem_filter, Finset.mem_univ, true_and]
    rw [Nat.lt_succ_iff, Nat.le_floor_iff ht]

theorem layoutClaim : LayoutClaim := by
  intro n G w ⟨σ, hσ⟩
  have hy : Function.Injective (fun v => ((σ v : ℕ) : ℝ)) := by
    intro u v h
    simp only [Nat.cast_inj] at h
    exact σ.injective (Fin.ext h)
  refine T2.plainLayout_s n G _ hy w (fun t => ?_)
  obtain ⟨i, hi⟩ := levelSet_position σ t
  have h1 := outerFrontier_card_le_crossCount G (fun v => ((σ v : ℕ) : ℝ)) t
  unfold crossCount at h1
  rw [hi] at h1
  exact le_trans (by exact_mod_cast h1) (hσ i)

/-! ## L2: ordering by distinct labels -/

theorem cutSize_empty (G : SimpleGraph (Fin n)) : cutSize G ∅ = 0 := by
  classical
  unfold cutSize
  simp

theorem cutSize_univ (G : SimpleGraph (Fin n)) : cutSize G Finset.univ = 0 := by
  classical
  unfold cutSize
  simp

theorem orderingClaim : OrderingClaim := by
  intro n G y hy w hw
  let f : Fin n → Fin n := fun v => ⟨C3.rank y v, C3.rank_lt_n y v⟩
  have hf : Function.Injective f := fun u v h => C3.rank_injective hy (congrArg Fin.val h)
  let σ : Fin n ≃ Fin n := Equiv.ofBijective f (Finite.injective_iff_bijective.mp hf)
  have hσ : ∀ v, ((σ v : Fin n) : ℕ) = C3.rank y v := fun v => rfl
  have hw0 : (0 : ℝ) ≤ w := le_trans (Nat.cast_nonneg _) (hw 0)
  refine ⟨σ, fun i => ?_⟩
  rcases Nat.eq_zero_or_pos i with rfl | hi0
  · have : prefixSet σ 0 = ∅ := by
      ext v; simp [prefixSet]
    rw [this, cutSize_empty]; simpa using hw0
  rcases lt_or_ge n i with hni | hin
  · have : prefixSet σ i = Finset.univ := by
      ext v
      simp only [prefixSet, Finset.mem_filter, Finset.mem_univ, true_and, iff_true]
      exact lt_trans (σ v).isLt hni
    rw [this, cutSize_univ]; simpa using hw0
  · obtain ⟨v, hv⟩ := C3.exists_rank_eq hy (show i - 1 < n by omega)
    have : prefixSet σ i = levelSet y (y v) := by
      ext u
      simp only [prefixSet, levelSet, Finset.mem_filter, Finset.mem_univ, true_and, hσ]
      rw [← C3.rank_le_iff hy, hv]
      omega
    rw [this]
    exact hw (y v)

end CutSweep
end CubicPathwidth

#print axioms CubicPathwidth.CutSweep.constantClaim
#print axioms CubicPathwidth.CutSweep.layoutClaim
#print axioms CubicPathwidth.CutSweep.orderingClaim
Back to top