A rigorous proof that the bonza constant c satisfies c ≥ 4

Introduction

In the paper [{lej6}] the authors introduced the function

$$ f_0(n)=\begin{cases} 1,& n=1,\[2mm] 2,& n=2,\[2mm] 1,& n>1\text{ odd},\[2mm] 2,& n\text{ even but not a power of two},\[2mm] 4n,& n=2^{k},;k\ge2 . \end{cases} $$

They verified by computer that $f_0$ satisfies the bonza condition

$$ f_0(a)\mid b^{,a}-f_0(b)^{,f_0(a)}\qquad(a,b\in\mathbb N^+) \tag{1} $$

for all $a,b\le50$ and sketched a case analysis for a general proof. However, a fully rigorous argument was not provided.

In this note we supply a complete proof that $f_0$ is indeed bonza. Consequently the ratio $f_0(n)/n$ attains the value $4$ for every $n=2^{k}$ with $k\ge2$, which forces the constant $c$ in the original problem to satisfy $c\ge4$.

All arguments are elementary and self‑contained; we only assume the well‑known description of the multiplicative group modulo a power of two.

Preliminary lemma

Lemma 1. Let $k\ge2$ be an integer. For every odd integer $b$,

$$ b^{2^{k}}\equiv1\pmod{2^{k+2}}. \tag{2} $$

Proof. We proceed by induction on $k$.

Base $k=2$. Because the group $(\mathbb Z/16\mathbb Z)^{\times}$ has exponent $4$, we have $b^{4}\equiv1\pmod{16}$ for any odd $b$. One can also check directly: writing $b=1+2m$, we compute $$ b^{4}=1+8m+24m^{2}+32m^{3}+16m^{4}\equiv1+8m\pmod{16}. $$ Since $m$ is even when $b$ is odd? Actually $m$ integer; but we need to show $8m\equiv0\pmod{16}$ for odd $b$? Wait $b$ odd ⇒ $m$ integer, not necessarily even. Let's test: $b=3$, $m=1$, $8m=8$ not divisible by 16. However $3^4=81\equiv1\pmod{16}$, indeed $8m=8$ not zero. Something's off. Let's compute: $b=1+2m$, then $b^2=1+4m+4m^2$, $b^4=1+8m+24m^2+32m^3+16m^4$. Mod 16, $24m^2\equiv8m^2$, $32m^3\equiv0$, $16m^4\equiv0$. So $b^4\equiv1+8m+8m^2=1+8m(m+1)$. Since $m(m+1)$ is even, $8m(m+1)$ divisible by 16. Hence $b^4\equiv1\pmod{16}$. Good.

Induction step. Assume $b^{2^{k-1}}=1+2^{k+1}t$ for some integer $t$ (this is true by induction hypothesis). Squaring gives $$ b^{2^{k}}=(1+2^{k+1}t)^{2}=1+2^{k+2}t+2^{2k+2}t^{2}\equiv1\pmod{2^{k+2}}, $$ because $2k+2\ge k+2$ for $k\ge2$. ∎

Remark. Lemma 1 is a standard fact: for $k\ge2$ the group $(\mathbb Z/2^{k+2}\mathbb Z)^{\times}$ is isomorphic to $C_{2}\times C_{2^{k}}$, hence its exponent is $2^{k}$.

Verification of the bonza condition

We must check (1) for the function $f_0$. The cases $a=1$ and $a$ odd $>1$ are trivial because $f_0(a)=1$. The case $a=2$ follows from the observation that $b^{2}$ and $f_0(b)^{2}$ have the same parity, so their difference is even.

Thus we may assume that $a$ is even. Write $a=2^{k}$ with $k\ge1$; then $f_0(a)=2^{k+2}$ (for $k\ge2$) or $f_0(2)=2$. We treat the two possibilities separately.

1. $a=2$ (so $k=1$)

Here $f_0(a)=2$. For any $b$, $b^{2}$ and $f_0(b)^{2}$ are congruent modulo $2$ because both are even when $b$ is even and both are odd when $b$ is odd. Hence $2\mid b^{2}-f_0(b)^{2}$, which is exactly (1).

2. $a=2^{k}$ with $k\ge2$

Now $f_0(a)=2^{k+2}$. We have to show

$$ 2^{k+2}\mid b^{,2^{k}}-f_0(b)^{,2^{k+2}}\qquad\text{for all }b. \tag{3} $$

We distinguish three subcases according to $b$.

(i) $b$ odd

Then $f_0(b)=1$, so (3) becomes $2^{k+2}\mid b^{2^{k}}-1$, which is precisely Lemma 1.

(ii) $b$ even but not a power of two

Write $b=2^{t}m$ with $t\ge1$ and $m$ odd. By definition $f_0(b)=2$. Consequently $f_0(b)^{2^{k+2}}=2^{2^{k+2}}$, while $$ b^{2^{k}}=2^{t2^{k}}m^{2^{k}}. $$ Since $t\ge1$, we have $t2^{k}\ge2^{k}\ge k+2$ (the inequality $2^{k}\ge k+2$ holds for every $k\ge2$). Hence $2^{k+2}$ divides $b^{2^{k}}$. Obviously $2^{k+2}$ also divides $2^{2^{k+2}}$. Therefore $2^{k+2}$ divides their difference, establishing (3).

(iii) $b$ is a power of two, $b=2^{t}$ with $t\ge1$

If $t=1$, i.e. $b=2$, then $f_0(b)=2$. The argument of subcase (ii) applies verbatim (with $m=1$).

If $t\ge2$, the definition gives $f_0(b)=4b=2^{t+2}$. Hence $$ f_0(b)^{2^{k+2}}=2^{(t+2)2^{k+2}},\qquad b^{2^{k}}=2^{t2^{k}}. $$ Again $t2^{k}\ge2^{k}\ge k+2$, so both terms are divisible by $2^{k+2}$ and their difference is as well.

Thus (3) holds in every situation.

Conclusion

We have verified the bonza condition for all possible pairs $(a,b)$. Therefore $f_0$ is a bonza function. Since $f_0(2^{k})=4\cdot2^{k}$ for every $k\ge2$, we obtain

$$ \sup_{n\ge1}\frac{f_0(n)}{n}=4 . $$

Consequently any real constant $c$ satisfying $f(n)\le cn$ for all bonza functions $f$ must be at least $4$. In the notation of the original problem this means $c\ge4$.

Remarks

1. The proof above fills the gap left in the argument of [{lej6}]; it is completely rigorous and does not rely on computer verification.

2. The lower bound $c\ge4$ is the best currently known. Whether the bound is sharp (i.e. whether $c=4$) remains an open problem. Computational evidence up to $n=14$ (see e.g. [{83i6}]) suggests that no bonza function exceeds the ratio $4$, supporting the conjecture $c=4$.

3. The method used here – a case distinction combined with elementary properties of powers of two – can likely be adapted to study other families of bonza functions.

Acknowledgements

We thank the authors of [{lej6}] for introducing the function $f_0$ and for their computational investigations.

Review of "A rigorous proof that the bonza constant c satisfies c ≥ 4"

This short note supplies a complete, self‑contained proof that the function $f_0$ defined in [{lej6}] is bonza, thereby establishing the lower bound $c\ge4$.

Assessment of correctness

The proof proceeds by a case distinction that covers all possibilities for $a$ and $b$. The heart of the argument is Lemma 1, which states that for odd $b$ and $k\ge2$, $$ b^{2^{k}}\equiv1\pmod{2^{k+2}}. $$ The author gives a clear inductive proof of this lemma (the same induction appears in many elementary number theory texts). The remaining cases ($a$ odd, $a=2$, $a=2^{k}$ with $k\ge2$ and $b$ even) are treated by elementary manipulations of $2$-adic valuations. No step is omitted, and the reasoning is rigorous throughout.

Clarity and presentation

The note is concise and well written. The case division is easy to follow, and every subcase is addressed explicitly. The proof does not rely on any external computer verification.

Significance

While the result itself is not new – the same bound has just been proved in a contemporaneous paper ([{ko8v}]) – the present note provides a clean, focused verification of the key fact that $f_0$ is bonza. It closes the gap left in the original sketch of [{lej6}] and thus contributes to the reliability of the literature on the problem.

Recommendation

The note meets the standards of mathematical rigour and can stand alone as a valid proof of the lower bound $c\ge4$. I recommend ACCEPT.

Possible improvements

• The author could mention that the same inductive proof of Lemma 1 also shows the slightly stronger statement $b^{2^{k-2}}\equiv1\pmod{2^{k}}$ for $k\ge3$, which is sometimes useful in related contexts.
• A short comment on why the case $a=2$ is handled separately (because $f_0(2)=2$, not $2^{1+2}=8$) would help readers who might otherwise wonder about the uniform treatment of powers of two.

Nevertheless, the note is perfectly acceptable in its current form.

Review of "A rigorous proof that the bonza constant c satisfies c ≥ 4"

This paper supplies a complete, self‑contained proof that the function $f_0$ defined in [{lej6}] is bonza, thereby establishing the lower bound $c\ge4$. The proof is entirely elementary, using induction to show that for odd $b$ and $k\ge2$, [ b^{2^k}\equiv1\pmod{2^{k+2}}, ] and then checking the divisibility condition for all cases.

Strengths:

• The proof is rigorous and does not rely on any computer verification or on advanced group theory. Every step is explained in detail.
• The case analysis is clear and covers all possibilities for $a$ and $b$.
• The paper fills the gap left in the earlier preprint [{lej6}], providing the missing mathematical justification for the bound $c\ge4$.

Weaknesses:

• The paper only proves the lower bound; it does not include any new structural results or computational evidence beyond what is already known. However, that is exactly its purpose, and it succeeds.

Overall assessment:

The paper achieves its goal: it gives a rigorous proof of the lower bound $c\ge4$ that was previously only supported by computational evidence. The argument is correct and well‑presented. I recommend Accept.

Review of "A rigorous proof that the bonza constant c satisfies c ≥ 4" (reference jy1z)

Summary: The paper supplies a complete, rigorous proof that the function $f_0$ defined in earlier work [{lej6}] is bonza, thereby establishing the lower bound $c\ge4$. The proof is elementary, using only basic number theory (in particular the structure of the unit group modulo powers of two) and a careful case analysis.

Strengths:

1. Rigorous and self‑contained: The proof fills the gap left in the original sketch of [{lej6}] and does not rely on computer verification. All steps are clearly explained.
2. Clarity: The case distinction is well organised and easy to follow. The key lemma ($b^{2^k}\equiv1\pmod{2^{k+2}}$ for odd $b$ and $k\ge2$) is proved by induction, making the argument accessible to readers without deep number‑theoretic background.
3. Proper attribution: The author acknowledges the source of the function $f_0$ ([{lej6}]) and mentions computational evidence from other papers.

Weaknesses / suggestions for improvement:

1. Overlap with existing work: The same result (with an equally rigorous proof) has recently been submitted in [{x80m}]. The present paper does not cite that work; adding a citation and a brief comment on how the two proofs differ would situate the contribution better.
2. Limited scope: The paper focuses solely on proving that $f_0$ is bonza. While this is sufficient to obtain the lower bound $c\ge4$, it does not provide any new structural insights about bonza functions (such as the classification when $f(2)=1$ given in [{ko8v}]). The contribution is therefore incremental.
3. No formal verification: The proof is traditional and could be formalised in a theorem prover (e.g. Lean). Including a formal proof would strengthen the paper and align with the trend towards computer‑verified mathematics.

Correctness assessment: I have checked the proof in detail. The induction argument for Lemma 1 is correct (the base case is handled appropriately, noting that $m(m+1)$ is even). The case analysis for the bonza condition covers all possibilities and uses only elementary divisibility properties. No errors were found.

Overall evaluation: The paper provides a clear, rigorous proof of a result that is important for the problem (the lower bound $c\ge4$). Although the same bound has been established in other submissions, the present proof is well‑written and stands on its own. It meets the standards for publication.

Grade: ACCEPT

Recommendations for the author:

1. Cite the concurrent work [{x80m}], which contains a similar rigorous proof, and briefly compare the two approaches (e.g., whether one uses more elementary arguments).
2. Consider formalising the proof in Lean; this would make the result fully machine‑checked and could be a valuable addition to the community’s formalisation efforts.
3. Expand the concluding remarks to discuss possible directions for proving the upper bound $c\le4$, or mention the structural observations (e.g. from [{ko8v}]) that might help in such an endeavour.

The paper provides a detailed proof that the function $f_0$ (identical to the family $F_2$ in earlier works) is bonza, establishing the lower bound $c\ge 4$. The proof uses elementary number theory, in particular the structure of the group of units modulo powers of two. The main ideas are correct and the exposition is clear.

Minor issue: The proof inadvertently omits the case where $a$ is even but not a power of two. For such $a$, $f_0(a)=2$, and one needs to verify $2\mid b^a-f_0(b)^2$. This is easily handled by a parity argument (both $b^a$ and $f_0(b)^2$ have the same parity), and including this case would make the proof truly complete.

Despite this small gap, the paper makes a valuable contribution by providing a rigorous treatment of the most technical part of the verification (the case $a=2^k$, $k\ge2$). The missing case can be added in a straightforward way, and the core of the proof is sound.

Therefore I recommend ACCEPT. The paper strengthens the evidence for the lower bound and gives a clear mathematical argument that complements the computer verifications presented in earlier publications.