CubicPathwidth.PwSeq.Seeds

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

import CubicPathwidth.PwSeqSpec
import CubicPathwidth.C3.Constants
import CubicPathwidth.T2.Labels4
import CubicPathwidth.T3.Constants

/-!
# The five seeds satisfy the hypotheses of Lemma 2 (obligation A6)

Proves `CubicPathwidth.PwSeq.targetSeedHyps : TargetSeedHyps`, i.e. `SeedHyp` for
`C = (c₃)` (k = 3), `F = (F₄, F₄)` (k = 4), and `P`, `R`, `S` (k = 5).
Only the approved statement `PwSeqSpec.lean` is used; no new declarations are postulated.
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq

open T2 T3

/-! ## Unfolding lemmas for `runMin` -/

theorem runMin_three (b : ℕ → ℝ) : runMin b 3 = incr b 3 := rfl

theorem runMin_four_le (b : ℕ → ℝ) : runMin b 4 ≤ incr b 4 := by
  show min (runMin b 3) (incr b 4) ≤ incr b 4
  exact min_le_right _ _

theorem runMin_five_le (b : ℕ → ℝ) : runMin b 5 ≤ incr b 5 := by
  show min (runMin b 4) (incr b 5) ≤ incr b 5
  exact min_le_right _ _

/-! ## Bounds on the seed constants -/

/-- `0 ≤ c₃` and `c₃ + c₃ ≤ 1`. -/
theorem c3_bounds : 0 ≤ C3.c3 ∧ C3.c3 + C3.c3 ≤ 1 := by
  have hpi : 3 < Real.pi := Real.pi_gt_three
  have hA0 : 0 ≤ Real.arccos (5 / 6) := Real.arccos_nonneg _
  have hA1 : Real.arccos (5 / 6) < 3 / 5 := C3.arccos_five_sixths_lt
  have hq0 : 0 ≤ 3 / (4 * Real.pi) := by positivity
  have hq1 : 3 / (4 * Real.pi) ≤ 1 / 4 := by
    rw [div_le_iff₀ (by positivity)]
    linarith
  have hprod : 3 / (4 * Real.pi) * Real.arccos (5 / 6) ≤ 1 / 4 * (3 / 5) :=
    mul_le_mul hq1 hA1.le hA0 (by norm_num)
  have hc : C3.c3 = 3 / (4 * Real.pi) * Real.arccos (5 / 6) := rfl
  constructor
  · rw [hc]
    exact mul_nonneg hq0 hA0
  · rw [hc]
    linarith

/-- `0 ≤ F₄ ≤ 1`: `F₄` is a supremum of probabilities. -/
theorem F4_bounds : 0 ≤ F4 ∧ F4 ≤ 1 := by
  have hbdd : BddAbove (Set.range fun τ : ℝ => T2.idealStarFn 4 r44 τ) :=
    ⟨1, by rintro _ ⟨τ, rfl⟩; exact T2.L4.idealStarFn_le_one r44 τ⟩
  unfold F4
  constructor
  · exact (T2.L4.idealStarFn_nonneg r44 0).trans (le_csSup hbdd ⟨0, rfl⟩)
  · exact csSup_le (Set.range_nonempty _)
      (by rintro _ ⟨τ, rfl⟩; exact T2.L4.idealStarFn_le_one r44 τ)

/-! ## Seeds of length `k = 3, 4, 5` -/

/-- `SeedHyp` for `k = 3` with the constant sequence `c₃`. -/
theorem seedHyp_C : SeedHyp 3 seqC := by
  refine ⟨le_refl _, ?_, fun d h1 h2 => absurd h2 (by omega), ?_⟩
  · exact c3_bounds.1
  · have hinc : runMin (seedSeq seqC) 3 = seqC 3 := by
      rw [runMin_three]
      simp [incr, seedSeq]
    rw [hinc]
    exact c3_bounds.2

/-- `SeedHyp` for `k = 4` with the constant sequence `F₄`. -/
theorem seedHyp_F : SeedHyp 4 seqF := by
  refine ⟨by norm_num, ?_, fun d h1 h2 => ?_, ?_⟩
  · exact F4_bounds.1
  · interval_cases d
    exact le_refl _
  · have hle : runMin (seedSeq seqF) 4 ≤ incr (seedSeq seqF) 4 := runMin_four_le _
    have hinc : incr (seedSeq seqF) 4 = 0 := by
      simp [incr, seedSeq, seqF]
    have hF := F4_bounds.2
    have hF0 := F4_bounds.1
    have hseq : seqF 4 = F4 := rfl
    rw [hinc] at hle
    rw [hseq]
    linarith

/-- A general sufficient condition for `SeedHyp 5`. -/
theorem seedHyp_five_of (a : ℕ → ℝ) (h0 : 0 ≤ a 3) (h1 : a 3 ≤ a 4) (h2 : a 4 ≤ a 5)
    (h3 : 2 * a 5 - a 4 ≤ 1) : SeedHyp 5 a := by
  refine ⟨by norm_num, h0, fun d hd1 hd2 => ?_, ?_⟩
  · interval_cases d
    · exact h1
    · exact h2
  · have hle : runMin (seedSeq a) 5 ≤ incr (seedSeq a) 5 := runMin_five_le _
    have hinc : incr (seedSeq a) 5 = a 5 - a 4 := by
      simp [incr, seedSeq]
    rw [hinc] at hle
    linarith

theorem seqP_values : seqP 3 = T2.Fcubic ∧ seqP 4 = 103 / 400 ∧ seqP 5 = 3667 / 10000 := by
  refine ⟨?_, ?_, ?_⟩ <;> simp [seqP, T3.coeff]

theorem seqR_values : seqR 3 = 291 / 2000 ∧ seqR 4 = 253 / 1000 ∧ seqR 5 = 9 / 25 := by
  refine ⟨?_, ?_, ?_⟩ <;> simp [seqR, T3.coeff]

theorem seqS_values : seqS 3 = 5 / 32 ∧ seqS 4 = 1 / 4 ∧ seqS 5 = 11 / 32 := by
  refine ⟨?_, ?_, ?_⟩ <;> simp [seqS, T3.coeff]

/-- `SeedHyp` for `k = 5` with the cubic sequence `P`. -/
theorem seedHyp_P : SeedHyp 5 seqP := by
  obtain ⟨e3, e4, e5⟩ := seqP_values
  apply seedHyp_five_of seqP
  · rw [e3]; exact T3.Fcubic_nonneg
  · rw [e3, e4]; exact T2.Fcubic_le
  · rw [e4, e5]; norm_num
  · rw [e4, e5]; norm_num

/-- `SeedHyp` for `k = 5` with the sequence `R`. -/
theorem seedHyp_R : SeedHyp 5 seqR := by
  obtain ⟨e3, e4, e5⟩ := seqR_values
  apply seedHyp_five_of seqR
  · rw [e3]; norm_num
  · rw [e3, e4]; norm_num
  · rw [e4, e5]; norm_num
  · rw [e4, e5]; norm_num

/-- `SeedHyp` for `k = 5` with the sequence `S`. -/
theorem seedHyp_S : SeedHyp 5 seqS := by
  obtain ⟨e3, e4, e5⟩ := seqS_values
  apply seedHyp_five_of seqS
  · rw [e3]; norm_num
  · rw [e3, e4]; norm_num
  · rw [e4, e5]; norm_num
  · rw [e4, e5]; norm_num

/-! ## (A6) -/

/-- (A6) All five seeds satisfy the hypotheses of Lemma 2. -/
theorem targetSeedHyps : TargetSeedHyps := by
  unfold TargetSeedHyps
  exact ⟨seedHyp_C, seedHyp_F, seedHyp_P, seedHyp_R, seedHyp_S⟩

end PwSeq
end CubicPathwidth

#print axioms CubicPathwidth.PwSeq.targetSeedHyps
Back to top