Erdős Problem 788 — exact finite model and final propositions
Definitionerdos788_problemFor , define the integer intervals
Given a finite set , call admissible when no sum of two distinct elements of lies in . Define to be the greatest integer threshold such that every finite admits an admissible finite with
The bundle also defines the exponent correction
and the explicit lower-bound constant . All occurrences of below are its integer value viewed as a real number.
The quantitative proposition says that there are and such that every satisfies
The exponent-one-half proposition says that for every there is such that every satisfies
The original upper-question proposition separately asserts the upper half of this conclusion, with its own threshold for each . The strengthened paper proposition is the conjunction of:
- for every natural ;
- the eventual two-sided quantitative estimate with lower constant exactly and some ; and
- the exponent-one-half proposition.
The complete final proposition conjoins that strengthened paper proposition with the separately quantified original upper-question proposition.
Formalization Note The finite maximum is first formed over natural
thresholds with an explicit finite score bound and then embedded into
. A separate mission milestone proves that this construction is
exactly the greatest integer with the stated universal property. Lean's
natural numbers include ; at both intervals are empty and .
Lean's real logarithm, division, and real power are total operations: in
particular . At the quotient inside the power is
negative, and Real.rpow uses Mathlib's total negative-base convention rather
than the signed real cube root. The proved asymptotic statements may choose
thresholds above these small values.
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Finset.Interval
/-!
# Erdős Problem 788: exact problem data and final statements
This file contains the public mathematical interface used by the Prove2Me
mission. It preserves the exact finite maximum from the original problem and
the strengthened final statement proved by the accompanying Lean repository.
The proof implementation is submitted separately.
-/
namespace Erdos788
/-- The integer interval `I_n = (n, 2n) ∩ ℕ`. -/
def I (n : ℕ) : Finset ℕ :=
Finset.Ioo n (2 * n)
/-- The integer interval `J_n = (2n, 4n) ∩ ℕ`. -/
def J (n : ℕ) : Finset ℕ :=
Finset.Ioo (2 * n) (4 * n)
/-- `C` is `B`-admissible: it lies in `I n`, and no sum of two distinct
members of `C` belongs to `B`. -/
def Admissible (n : ℕ) (B C : Finset ℕ) : Prop :=
C ⊆ I n ∧
∀ ⦃c⦄, c ∈ C → ∀ ⦃c'⦄, c' ∈ C → c ≠ c' → c + c' ∉ B
/-- The natural-number form of the universal guarantee at threshold `t`. -/
def Guarantees (n t : ℕ) : Prop :=
∀ B : Finset ℕ, B ⊆ J n →
∃ C : Finset ℕ, Admissible n B C ∧ t ≤ B.card + C.card
/-- A uniform finite upper bound for every score `|B| + |C|`. -/
def scoreBound (n : ℕ) : ℕ :=
(J n).card + (I n).card
/-- The largest natural-number threshold with the universal property. -/
noncomputable def fNat (n : ℕ) : ℕ := by
classical
exact Nat.findGreatest (Guarantees n) (scoreBound n)
/-- The integer-valued function `f(n)` in the original problem. -/
noncomputable def f (n : ℕ) : ℤ :=
(fNat n : ℤ)
/-- The paper's universal guarantee predicate for an arbitrary integer `t`. -/
def IntegerGuarantees (n : ℕ) (t : ℤ) : Prop :=
∀ B : Finset ℕ, B ⊆ J n →
∃ C : Finset ℕ, Admissible n B C ∧
t ≤ ((B.card + C.card : ℕ) : ℤ)
/-- The exponent correction in the quantitatively strong paper. -/
noncomputable def exponentCorrection (n : ℕ) : ℝ :=
(Real.log (Real.log (n : ℝ)) / Real.log (n : ℝ)) ^ (1 / 3 : ℝ)
/-- The explicit lower-bound constant in the strengthened formal statement. -/
noncomputable def finalLowerBoundConstant : ℝ :=
1 / 2000
/-- The fully quantified two-sided conclusion of the main theorem. -/
def QuantitativeMainTheorem : Prop :=
∃ c C : ℝ, 0 < c ∧ 0 < C ∧
∃ n₀ : ℕ, 1 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n →
c * Real.sqrt ((n : ℝ) * Real.log (n : ℝ)) ≤ (f n : ℝ) ∧
(f n : ℝ) ≤
(n : ℝ) ^ ((1 / 2 : ℝ) + C * exponentCorrection n)
/-- Explicit epsilon quantifiers for `f(n) = n^(1/2+o(1))`. -/
def HasExponentOneHalf : Prop :=
∀ ε : ℝ, 0 < ε → ∃ n₀ : ℕ, 1 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n →
(n : ℝ) ^ ((1 / 2 : ℝ) - ε) ≤ (f n : ℝ) ∧
(f n : ℝ) ≤ (n : ℝ) ^ ((1 / 2 : ℝ) + ε)
/-- The precise epsilon-quantified upper-bound question on the original
Erdős Problems page. -/
def AnswersOriginalUpperQuestion : Prop :=
∀ ε : ℝ, 0 < ε → ∃ n₀ : ℕ, 1 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n →
(f n : ℝ) ≤ (n : ℝ) ^ ((1 / 2 : ℝ) + ε)
/-- The strengthened paper statement: the explicit lower bound holds for
every `n ≥ 3`, the quantitative upper bound holds for all sufficiently large
positive integers, and the resulting exponent is one half. -/
def PaperMainTheorem : Prop :=
(∀ n : ℕ, 3 ≤ n →
finalLowerBoundConstant * Real.sqrt ((n : ℝ) * Real.log (n : ℝ)) ≤
(f n : ℝ)) ∧
(∃ C : ℝ, 0 < C ∧
∃ n₀ : ℕ, 1 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n →
finalLowerBoundConstant *
Real.sqrt ((n : ℝ) * Real.log (n : ℝ)) ≤ (f n : ℝ) ∧
(f n : ℝ) ≤
(n : ℝ) ^ ((1 / 2 : ℝ) + C * exponentCorrection n)) ∧
HasExponentOneHalf
/-- The complete final statement: the strengthened paper theorem together
with the original upper-bound question in its exact epsilon form. -/
def MainTheorem : Prop :=
PaperMainTheorem ∧ AnswersOriginalUpperQuestion
end Erdos788