Erdős Problem 788 — exact finite model and final propositions

I

For each natural number $n$, $I(n)$ is the finite set $\{m\in\mathbb N:n<m<2n\}$, with both endpoints excluded. Thus $I(0)=I(1)=\varnothing$, while for $n\ge1$ it consists of $n+1,n+2,\ldots,2n-1$ and has cardinality $n-1$.

J

For each natural number $n$, $J(n)$ is the finite set $\{m\in\mathbb N:2n<m<4n\}$, with both endpoints excluded. Thus $J(0)=\varnothing$, while for $n\ge1$ it consists of $2n+1,2n+2,\ldots,4n-1$ and has cardinality $2n-1$; in particular, $J(1)=\{3\}$.

Admissible

For every natural number $n$ and arbitrary finite sets $B,C\subseteq\mathbb N$, Admissible n B C holds exactly when every $c\in C$ satisfies $n<c<2n$, and for every two universally quantified natural numbers $c,c'\in C$, if $c\ne c'$, then $c+c'\notin B$. There is no requirement here that $B\subseteq\{b\in\mathbb N:2n<b<4n\}$. The sum of an element with itself is unrestricted because only distinct members are tested. The pair-avoidance condition is vacuous when $C$ is empty or a singleton; the empty set is admissible for every $n$ and every $B$, and when $n=0$ or $n=1$, admissibility forces $C=\varnothing$.

Guarantees

For every pair of natural numbers $n,t$, Guarantees n t asserts that for every finite set $B\subseteq\mathbb N$ whose members all satisfy $2n<b<4n$, there exists a finite set $C\subseteq\mathbb N$, allowed to depend on $B$, such that every $c\in C$ satisfies $n<c<2n$, no sum $c+c'$ of two distinct members $c,c'\in C$ belongs to $B$, and $t\le|B|+|C|$. The universal quantifier includes $B=\varnothing$, and the existential choice may be $C=\varnothing$. Consequently, the assertion always holds for $t=0$. For $n=0$ it holds exactly when $t=0$, since both intervals are empty; for $n=1$ it also holds exactly when $t=0$, since the universally included choice $B=\varnothing$ and the forced choice $C=\varnothing$ give score $0$.

scoreBound

For every natural number $n$, scoreBound n is the natural number $\left|\{b\in\mathbb N:2n<b<4n\}\right|+\left|\{c\in\mathbb N:n<c<2n\}\right|$. It is $0$ when $n=0$, and for $n\ge1$ it equals $(2n-1)+(n-1)=3n-2$; in particular, its values at $n=1$ and $n=2$ are $1$ and $4$. This declaration defines that number but does not itself quantify over $B$ or $C$ or assert a proposition about them.

fNat

For every natural number $n$, fNat n is obtained by searching only among natural numbers $t\le\left|\{b\in\mathbb N:2n<b<4n\}\right|+\left|\{c\in\mathbb N:n<c<2n\}\right|$ and taking the greatest $t$ such that, for every finite $B\subseteq\{b\in\mathbb N:2n<b<4n\}$, there exists a finite $C\subseteq\{c\in\mathbb N:n<c<2n\}$ for which every two distinct $c,c'\in C$ satisfy $c+c'\notin B$ and $t\le|B|+|C|$. The bounded greatest-search operation is total and would return $0$ if no searched value satisfied the predicate; here $t=0$ always satisfies it, by choosing $C=\varnothing$, so the returned value is an actual satisfying maximum. The search bound is $0$ at $n=0$ and $3n-2$ for $n\ge1$. In particular, fNat 0 and fNat 1 are $0$, while fNat 2 is $1$: at $n=2$ the inner interval is $\{3\}$, so a singleton $C$ always gives score at least $1$, whereas $B=\varnothing$ prevents any score greater than $1$.

f

For every natural number $n$, f n is the integer obtained by coercing the following natural number to $\mathbb Z$: the greatest natural $t\le\left|\{b\in\mathbb N:2n<b<4n\}\right|+\left|\{c\in\mathbb N:n<c<2n\}\right|$ such that every finite $B\subseteq\{b\in\mathbb N:2n<b<4n\}$ admits a finite $C\subseteq\{c\in\mathbb N:n<c<2n\}$ with no sum of two distinct members of $C$ in $B$ and with $t\le|B|+|C|$. The bounded search is total with fallback value $0$, and $0$ is in fact always a valid candidate. Hence f n is always a nonnegative integer, with $f(0)=0$, $f(1)=0$, and $f(2)=1$.

IntegerGuarantees

For every natural number $n$ and every integer $t$, IntegerGuarantees n t asserts that for every finite set $B\subseteq\{b\in\mathbb N:2n<b<4n\}$, there exists a finite set $C\subseteq\{c\in\mathbb N:n<c<2n\}$ such that no sum of two distinct members of $C$ belongs to $B$ and $t\le\iota_{\mathbb N\to\mathbb Z}(|B|+|C|)$, where the entire natural-number sum of cardinalities is then cast to an integer. Every integer $t\le0$ satisfies this assertion for every $n$, by taking $C=\varnothing$, because the cast score is nonnegative. For $n=0$ and for $n=1$, the assertion holds exactly for $t\le0$, since the universally included choice $B=\varnothing$ and the forced choice $C=\varnothing$ produce score $0$.

exponentCorrection

For every natural number $n$, exponentCorrection n is the real-power value $\left(\dfrac{\log(\log n)}{\log n}\right)^{1/3}$, with $n$ first cast to $\mathbb R$ and the division and exponent interpreted in $\mathbb R$. The operations are totalized: $\log0=0$, while for a negative nonzero real $x$, $\log x=\log|x|$; real division satisfies $x/0=0$; for $x>0$, Mathlib’s real power is $x^y=\exp(\log x\cdot y)$; for $x<0$, it is $x^y=\exp(\log|x|\cdot y)\cos(\pi y)$; and $0^0=1$ while $0^y=0$ for every $y\ne0$, including negative $y$. Consequently, at $n=0$ and $n=1$ the quotient is $0/0=0$ and the correction is $0^{1/3}=0$. At $n=2$, $\log2\in(0,1)$, so $q_2:=\log(\log2)/\log2<0$, and therefore $q_2^{1/3}=\exp\!\left(\frac13\log|q_2|\right)\cos(\pi/3)=\frac12\exp\!\left(\frac13\log|q_2|\right)$: it is one half of the ordinary positive cube root of $|q_2|$, not the signed real cube root and not the full positive cube root. For every natural $n\ge3$, the quotient is positive, so the expression is the ordinary positive cube root of that quotient.

finalLowerBoundConstant

finalLowerBoundConstant is the real number $\dfrac1{2000}$. Although real division is totalized at zero denominators, the denominator here is nonzero, so this is the ordinary positive rational number $1/2000$.

QuantitativeMainTheorem

For this declaration, for each $n\in\mathbb N$ let $\mathcal I_n=\{i\in\mathbb N:n<i<2n\}$ and $\mathcal J_n=\{j\in\mathbb N:2n<j<4n\}$, and let $M_n$ be the greatest natural number $t\le|\mathcal J_n|+|\mathcal I_n|$ such that every finite $B\subseteq\mathcal J_n$ admits a finite $D\subseteq\mathcal I_n$ satisfying $\forall d,d'\in D,\ d\ne d'\Rightarrow d+d'\notin B$ and $t\le|B|+|D|$; $t=0$ is always a candidate, and $M_n$ is used below after coercion first to $\mathbb Z$ and then to $\mathbb R$. The proposition asserts that there exist real numbers $c,C$ with $c>0$ and $C>0$, and then a natural number $n_0\ge1$, such that every natural number $n\ge n_0$ simultaneously satisfies $c\sqrt{n\log n}\le M_n$ and $M_n\le n^{\,1/2+Cq_n^{1/3}}$, where $q_n=\log(\log n)/\log n$ and both superscripted operations use Mathlib’s real power. The constants $c,C$ are uniform in $n$, while $n_0$ is chosen after them. Here $\log0=0$, division by zero is $0$, and $\sqrt{x}$ is the usual nonnegative square root for $x\ge0$ and is $0$ for $x<0$. For real power, a positive base satisfies $x^y=\exp(\log x\cdot y)$, a negative base satisfies $x^y=\exp(\log|x|\cdot y)\cos(\pi y)$, and $0^0=1$ while $0^y=0$ for $y\ne0$. The condition $n\ge n_0\ge1$ excludes $n=0$ and makes the outer power base positive and $n\log n$ nonnegative. If $n=1$ is included, then $\log1=0$, the square-root term and $q_1^{1/3}$ are $0$, $M_1=0$, and the outer power is $1^{1/2}=1$. If $n=2$ is included, then $q_2<0$ and $q_2^{1/3}$ is one half of the ordinary positive cube root of $|q_2|$ because $\cos(\pi/3)=1/2$.

HasExponentOneHalf

For this declaration, for each $n\in\mathbb N$ let $\mathcal I_n=\{i\in\mathbb N:n<i<2n\}$ and $\mathcal J_n=\{j\in\mathbb N:2n<j<4n\}$, and let $M_n$ be the greatest natural number $t\le|\mathcal J_n|+|\mathcal I_n|$ such that every finite $B\subseteq\mathcal J_n$ admits a finite $D\subseteq\mathcal I_n$ with no sum of two distinct members in $B$ and with $t\le|B|+|D|$; this maximum exists because $t=0$ is a candidate, and it is used as a real number after coercion through $\mathbb Z$. The proposition asserts that for every real $\varepsilon>0$, there exists a natural number $n_0\ge1$, allowed to depend on $\varepsilon$, such that every natural $n\ge n_0$ satisfies both $n^{\,1/2-\varepsilon}\le M_n$ and $M_n\le n^{\,1/2+\varepsilon}$. These are Mathlib real powers: a positive base satisfies $x^y=\exp(\log x\cdot y)$, a negative base satisfies $x^y=\exp(\log|x|\cdot y)\cos(\pi y)$, and $0^0=1$ while $0^y=0$ for every nonzero $y$, including negative $y$. Every quantified base is in fact positive because $n\ge n_0\ge1$, so neither the negative-base nor zero-base branch occurs, although the lower exponent may be zero or negative. Since $M_1=0$ but $1^y=1$ for every real $y$, $n_0=1$ cannot satisfy the displayed lower bound; any actual witness must therefore be at least $2$. The excluded value $n=0$ would exhibit the zero-base totalization: its lower power would be $1$ when $\varepsilon=1/2$ and $0$ otherwise, including when $1/2-\varepsilon<0$.

AnswersOriginalUpperQuestion

For this declaration, for each $n\in\mathbb N$ let $\mathcal I_n=\{i\in\mathbb N:n<i<2n\}$ and $\mathcal J_n=\{j\in\mathbb N:2n<j<4n\}$, and let $M_n$ be the greatest natural number $t\le|\mathcal J_n|+|\mathcal I_n|$ such that every finite $B\subseteq\mathcal J_n$ admits a finite $D\subseteq\mathcal I_n$ whose distinct-pair sums avoid $B$ and for which $t\le|B|+|D|$; $t=0$ is always a candidate, and $M_n$ is read as a real number after coercion through $\mathbb Z$. The proposition asserts that for every real $\varepsilon>0$, there exists a natural number $n_0\ge1$, allowed to depend on $\varepsilon$, such that every natural number $n\ge n_0$ satisfies $M_n\le n^{\,1/2+\varepsilon}$. The right side is Mathlib’s real power: it is $\exp(\log x\cdot y)$ for a positive base, $\exp(\log|x|\cdot y)\cos(\pi y)$ for a negative base, $1$ when $x=y=0$, and $0$ when $x=0$ and $y\ne0$. In the quantified range the base is positive and the exponent is strictly positive, so neither the zero-base nor negative-base branch is used. If $n=1$ is included, the inequality at that value is $M_1=0\le1^{1/2+\varepsilon}=1$; $n=0$ is excluded by $n_0\ge1$, and if evaluated there its positive-exponent power would be $0$.

PaperMainTheorem

For this declaration, for each $n\in\mathbb N$ let $\mathcal I_n=\{i\in\mathbb N:n<i<2n\}$ and $\mathcal J_n=\{j\in\mathbb N:2n<j<4n\}$, and let $M_n$ be the greatest natural number $t\le|\mathcal J_n|+|\mathcal I_n|$ such that every finite $B\subseteq\mathcal J_n$ admits a finite $D\subseteq\mathcal I_n$ satisfying $\forall d,d'\in D,\ d\ne d'\Rightarrow d+d'\notin B$ and $t\le|B|+|D|$; $0$ is always a candidate, and $M_n$ is used in the inequalities after coercion through $\mathbb Z$ to $\mathbb R$. The proposition is the conjunction of three requirements: first, every natural $n\ge3$ satisfies $\frac1{2000}\sqrt{n\log n}\le M_n$; second, there exist a real $C>0$ and a natural $n_0\ge1$ such that every natural $n\ge n_0$ satisfies both $\frac1{2000}\sqrt{n\log n}\le M_n$ and $M_n\le n^{\,1/2+Cq_n^{1/3}}$, where $q_n=\log(\log n)/\log n$; third, for every real $\varepsilon>0$ there exists a natural number $m_0\ge1$, allowed to depend on $\varepsilon$, such that every natural $n\ge m_0$ satisfies both $n^{\,1/2-\varepsilon}\le M_n$ and $M_n\le n^{\,1/2+\varepsilon}$. The $C,n_0$ in the second requirement are independent of the per-$\varepsilon$ thresholds in the third. The operations are totalized: $\log0=0$ and $\log x=\log|x|$ for negative nonzero $x$; $x/0=0$; $\sqrt{x}=0$ for $x<0$ and is the usual nonnegative square root for $x\ge0$; positive-base real power is $\exp(\log x\cdot y)$; negative-base real power is $\exp(\log|x|\cdot y)\cos(\pi y)$; and $0^0=1$ while $0^y=0$ for $y\ne0$. The first requirement encounters only $n\ge3$, where its logarithm and radicand are positive. In the second requirement, $n=0$ is excluded; at $n=1$, if included, the square-root term and correction are $0$, $M_1=0$, and the outer power is $1$; at $n=2$, $q_2<0$ and $q_2^{1/3}=\frac12\exp\!\left(\frac13\log|q_2|\right)$, one half of the ordinary positive cube root of $|q_2|$. In the third requirement, an actual $m_0$ cannot equal $1$, because its lower inequality at $n=1$ would be $1\le M_1=0$.

MainTheorem

For this declaration, for each $n\in\mathbb N$ let $\mathcal I_n=\{i\in\mathbb N:n<i<2n\}$ and $\mathcal J_n=\{j\in\mathbb N:2n<j<4n\}$, and let $M_n$ be the greatest natural number $t\le|\mathcal J_n|+|\mathcal I_n|$ such that every finite $B\subseteq\mathcal J_n$ admits a finite $D\subseteq\mathcal I_n$ with every distinct-pair sum outside $B$ and with $t\le|B|+|D|$; $0$ is always a candidate, and $M_n$ is used as a real number after coercion first to $\mathbb Z$ and then to $\mathbb R$. The proposition is the conjunction of four fully quantified requirements: (i) every natural $n\ge3$ satisfies $\frac1{2000}\sqrt{n\log n}\le M_n$; (ii) there exist a real $C>0$ and a natural $n_0\ge1$ such that every natural $n\ge n_0$ satisfies both $\frac1{2000}\sqrt{n\log n}\le M_n$ and $M_n\le n^{\,1/2+Cq_n^{1/3}}$, where $q_n=\log(\log n)/\log n$; (iii) for every real $\varepsilon>0$ there exists a natural $m_0\ge1$ such that every natural $n\ge m_0$ satisfies both $n^{\,1/2-\varepsilon}\le M_n$ and $M_n\le n^{\,1/2+\varepsilon}$; and (iv) separately, for every real $\varepsilon>0$ there exists a natural $k_0\ge1$ such that every natural $n\ge k_0$ satisfies $M_n\le n^{\,1/2+\varepsilon}$. The thresholds $m_0$ and $k_0$ may depend on $\varepsilon$ and are separately existentially quantified, while $C,n_0$ belong only to requirement (ii). Here $\log0=0$, negative nonzero inputs to the real logarithm are handled through absolute value, division by zero is $0$, and the real square root is $0$ on negative inputs and the usual nonnegative root otherwise. Mathlib’s real power is $\exp(\log x\cdot y)$ for $x>0$, $\exp(\log|x|\cdot y)\cos(\pi y)$ for $x<0$, $1$ for $0^0$, and $0$ for $0^y$ when $y\ne0$. Thus $q_0=q_1=0$ because $0/0=0$; $q_2<0$ and $q_2^{1/3}=\frac12\exp\!\left(\frac13\log|q_2|\right)$ because $\cos(\pi/3)=1/2$; and $q_n>0$ for natural $n\ge3$. Requirement (i) starts at $3$; requirement (ii) excludes $0$ but may include $1$ or $2$; requirement (iii) cannot have $m_0=1$ because $1^{1/2-\varepsilon}=1>M_1=0$; and requirement (iv) has no such lower-bound obstruction at $1$, where its inequality is $0\le1$.