CubicPathwidth.Completion

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

import CubicPathwidth.CoreLifting
import CubicPathwidth.Bootstrap
import CubicPathwidth.GaussianSign

/-!
# The complete existential pathwidth theorem

The original MainClaim is proved with no additional mathematical hypotheses.
Gaussian bisection first supplies a coarse coefficient 2c < 1/3. The proved
boundary/core transfer and the general coefficient step then converge to
2c/(1+6c), strictly below 1/6. Algorithm and running-time claims are separate.
-/

noncomputable section
namespace CubicPathwidth

theorem pathwidthCoefficient_le_twice_bisection :
    pathwidthCoefficient ≤ 2 * bisectionCoefficient := by
  have hc := bisectionCoefficient_nonneg
  have hg := pathwidthCoefficient_nonneg
  nlinarith [pathwidthCoefficient_fixed_point]

/-- Starting above the target, but already strictly below 1/3. -/
def bootstrapCoefficient (j : ℕ) : ℝ :=
  pathwidthCoefficient + transferRatio ^ j * (2 * bisectionCoefficient - pathwidthCoefficient)

@[simp] theorem bootstrapCoefficient_zero : bootstrapCoefficient 0 = 2 * bisectionCoefficient := by
  simp [bootstrapCoefficient]

theorem bootstrapCoefficient_nonneg (j : ℕ) : 0 ≤ bootstrapCoefficient j := by
  unfold bootstrapCoefficient
  exact add_nonneg pathwidthCoefficient_nonneg
    (mul_nonneg (pow_nonneg transferRatio_pos.le _)
      (sub_nonneg.mpr pathwidthCoefficient_le_twice_bisection))

theorem bootstrapCoefficient_le_twice (j : ℕ) :
    bootstrapCoefficient j ≤ 2 * bisectionCoefficient := by
  have hp : transferRatio ^ j ≤ 1 := pow_le_one₀ transferRatio_pos.le transferRatio_lt_one.le
  have hm := mul_le_mul_of_nonneg_right hp
    (sub_nonneg.mpr pathwidthCoefficient_le_twice_bisection)
  unfold bootstrapCoefficient
  linarith

theorem bootstrapCoefficient_succ (j : ℕ) :
    bootstrapCoefficient (j + 1) = bisectionCoefficient +
      (1 / 2 - 3 * bisectionCoefficient) * bootstrapCoefficient j := by
  unfold bootstrapCoefficient
  rw [pow_succ]
  unfold transferRatio
  nlinarith [pathwidthCoefficient_fixed_point]

theorem exists_bootstrapCoefficient_lt (ε : ℝ) (hε : 0 < ε) :
    ∃ j : ℕ, bootstrapCoefficient j < pathwidthCoefficient + ε := by
  let d := 2 * bisectionCoefficient - pathwidthCoefficient
  have hd : 0 ≤ d := sub_nonneg.mpr pathwidthCoefficient_le_twice_bisection
  obtain ⟨j, hj⟩ := exists_pow_lt_of_lt_one (div_pos hε (show 0 < d + 1 by linarith))
    transferRatio_lt_one
  have hm := (lt_div_iff₀ (show 0 < d + 1 by linarith)).mp hj
  have hp := pow_nonneg transferRatio_pos.le j
  refine ⟨j, ?_⟩
  change pathwidthCoefficient + transferRatio ^ j * d < pathwidthCoefficient + ε
  nlinarith

/-- Each finite improvement step is proved uniformly over the graph class. -/
theorem uniformBootstrapCoefficient (j : ℕ) : UniformPathwidthBound (bootstrapCoefficient j) := by
  induction j with
  | zero =>
    rw [bootstrapCoefficient_zero]
    exact uniformPathwidthBound_twice_of_bisection bisectionCoefficient_nonneg uniformGaussianBisection
  | succ j ih =>
    have hb := bootstrapCoefficient_nonneg j
    have hb' : bootstrapCoefficient j < (1 : ℝ) / 3 := by
      linarith [bootstrapCoefficient_le_twice j, bisectionCoefficient_lt_one_sixth]
    rw [bootstrapCoefficient_succ]
    exact coefficient_step_of_endpoint_general _ hb hb'.le uniformGaussianBisection
      (boundaryTransfer _ hb hb' ih)

/-- The original uniform pathwidth bound, with all proof dependencies discharged. -/
theorem uniformImprovedPathwidth : UniformPathwidthBound pathwidthCoefficient := by
  apply uniformPathwidthBound_of_approximations
  intro ε hε
  obtain ⟨j, hj⟩ := exists_bootstrapCoefficient_lt ε hε
  exact ⟨bootstrapCoefficient j, hj, uniformBootstrapCoefficient j⟩

/-- The original specification: a fixed coefficient strictly below 1/6, with
one error threshold chosen before the graph and its number of vertices. -/
theorem mainClaim : MainClaim :=
  ⟨pathwidthCoefficient_lt_one_sixth, uniformImprovedPathwidth⟩

/-- Recover the former starting-bound obligation as a consequence. It is
not assumed anywhere in the completed proof. -/
theorem uniformOneSixthPathwidth : UniformPathwidthBound ((1 : ℝ) / 6) := by
  intro ε hε
  obtain ⟨N, hN⟩ := uniformImprovedPathwidth ε hε
  refine ⟨N, ?_⟩
  intro n hn G hG
  exact (hN n hn G hG).mono
    (mul_le_mul_of_nonneg_right (by linarith [pathwidthCoefficient_lt_one_sixth]) (Nat.cast_nonneg n))

/-- An explicit positive saving, in the original goal's exact quantifier form. -/
theorem fixedSaving : FixedSavingGoal := fixedSaving_of_mainClaim mainClaim

end CubicPathwidth

#print axioms CubicPathwidth.boundaryTransfer
#print axioms CubicPathwidth.uniformImprovedPathwidth
#print axioms CubicPathwidth.mainClaim
#print axioms CubicPathwidth.uniformOneSixthPathwidth
Back to top