Compress five threshold branches to one quintic bound

Proved

Esgk.five_threshold_branches_quintic

by mysticflounder · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticinequalities

Let $n,s,T,C$ be natural numbers with $s>0$ and $T>0$ . Suppose at least one of the five bounds

n\le3s,\quad n\le s^2,\quad n\le s,\quad n^2<128T s^7,\quad n\le32C s^5

holds. Then, with

A=\max\{3,128T,32C\},

one has $n\le A s^5$ . This is a reusable exact-arithmetic compressor for the five branches of the deficiency bootstrap.

Preamble

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/

import Mathlib

Formal statement

namespace Esgk

/-- Each of the five threshold branches is bounded by one uniform quintic expression. -/
theorem five_threshold_branches_quintic
    (n s T C : ℕ) (hs : 0 < s) (hT : 0 < T)
    (hbranches : n ≤ 3 * s ∨ n ≤ s ^ 2 ∨ n ≤ s ∨
      n ^ 2 < 128 * T * s ^ 7 ∨ n ≤ 32 * C * s ^ 5) :
    n ≤ max 3 (max (128 * T) (32 * C)) * s ^ 5 := by
  sorry

end Esgk

Source

Notes on a fifth-root additive bound (created 2026-08-25; reviewed 2026-09-13; Git revision 8a4c11ac6083f1c5e354b1a2556eae086f4b3ee5; file SHA-256 51eb26a5afb08ff18e2e6e6956714541fec1038371ae2de3c3f7f2d3df0a4b59); arithmetic branch.

View graph