One-fifth excess from a natural deficiency quintic

Proved

Esgk.eventual_one_fifth_excess_of_nat_deficiency_quintic

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

analysisasymptotics

For each natural number $n$ , let $X_n$ be a type of objects, let $P_n(x)$ be a qualifying predicate, and let $K_n(x)$ be a natural-valued quantity. Suppose there are a positive integer $A$ and a threshold after which every qualifying object admits $\sigma\in\mathbb N$ with

(n-1)+\sigma=3K_n(x),\qquad n\le A(\sigma+1)^5.

Then there are $c>0$ and a threshold after which every qualifying object satisfies

K_n(x)\ge\frac n3+c n^{1/5}.

Both constants are uniform over the family. This is a reusable analytic interface for fifth-root extraction and absorption of the fixed deficiency offset.

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

open Filter

Formal statement

namespace Esgk

/-- An eventual natural deficiency quintic bound yields an additive one-fifth excess. -/
theorem eventual_one_fifth_excess_of_nat_deficiency_quintic
    (X : ℕ → Type)
    (P : (n : ℕ) → X n → Prop)
    (K : (n : ℕ) → X n → ℕ)
    (hquintic :
      ∃ A : ℕ, 0 < A ∧
        ∀ᶠ n : ℕ in Filter.atTop,
          ∀ x : X n,
            P n x →
            ∃ σ : ℕ, (n - 1) + σ = 3 * K n x ∧ n ≤ A * (σ + 1) ^ 5) :
    ∃ c : ℝ, 0 < c ∧
      ∀ᶠ n : ℕ in Filter.atTop,
        ∀ x : X n,
          P n x →
          (n : ℝ) / 3 + c * Real.rpow (n : ℝ) (1 / 5 : ℝ) ≤ (K n x : ℝ) := by
  sorry

end Esgk

Source

Consolidated argument for a fifth-root additive bound (dated 2026-08-25; revision 2026-09-13; Git revision 8a4c11ac6083f1c5e354b1a2556eae086f4b3ee5; file SHA-256 af6ee6023fe1ff3730b492ea3756d240818df46a877abe3b7ac1153fc7c0245c); Sections 2 and 16.3.

View graph