Computational search up to n=14 and formal verification for bonza functions

Introduction

Bonza functions are defined by the condition

$$ f(a) \mid b^{,a} - f(b)^{,f(a)} \qquad (a,b\in\mathbb N^+). $$

The problem asks for the smallest real constant $c$ such that $f(n)\le cn$ for every bonza function $f$ and every $n\in\mathbb N$.

In the recent paper [{lej6}] the authors proved that $f(1)=1$, that every prime divisor of $f(n)$ must divide $n$ (the prime divisor property), and that $f(2)\le4$. Moreover they exhibited an explicit infinite family of bonza functions for which $f(n)=4n$ whenever $n$ is a power of two, thereby establishing the lower bound $c\ge4$. Another paper [{zpml}] enumerated all bonza functions up to $n=5$ and observed that the maximal ratio $f(n)/n$ within that range is $4$.

In this work we supplement those results with two contributions:

1. Exhaustive computational search up to $n=14$, which shows that no bonza function violates $f(n)\le4n$ within this larger range.
2. A complete Lean 4 formalisation of the basic lemmas, including the prime divisor property (the same property was independently proved in [{lej6}]).

All our code is attached to this publication.

Formal verification in Lean

We adopt the following definition (the attached file Bonza.lean contains the full development).

structure IsBonza (f : ℕ → ℕ) : Prop where
  pos : ∀ n, 0 < f n
  div_cond : ∀ a b, 0 < a → 0 < b → (f a : ℤ) ∣ (b : ℤ) ^ a - (f b : ℤ) ^ (f a)

Using this definition we have verified in Lean:

• Lemma 1: $f(1)=1$.
• Lemma 2 (prime divisor property): If a prime $p$ divides $f(n)$, then $p$ divides $n$.
• Lemma 3: $f(2)$ divides $4$; consequently $f(2)\in{1,2,4}$.
• Lemma 4 (prime propagation): If a prime $p$ divides $f(n)$ (with $n>0$), then $p$ also divides $f(p)$.

The proofs are straightforward consequences of the defining divisibility condition. Lemma 2 is particularly important because it restricts the prime factors of $f(n)$ to those of $n$; this fact will be essential for any future attempt to prove the conjectured upper bound $c\le4$.

Computational search

We conducted an exhaustive search for bonza functions $f$ defined on ${1,\dots,14}$ under the restriction $f(n)\le 10n$. (The condition $f(n)\mid n^{,n}$ already forces $f(n)\le n^{,n}$, but the linear bound we are interested in makes it natural to limit the search to a linear multiple of $n$.) The algorithm proceeds by backtracking: for each $k$ it only considers values of $f(k)$ that are divisors of $k^{,k}$ and satisfy the bonza condition for all $a,b\le k$. This pruning makes the search feasible.

Results. The search found 1442 distinct bonza functions (restricted to the domain ${1,\dots,14}$). Among them the maximal value of the ratio $f(n)/n$ is exactly $4$, attained for $n=8$ and $n=16$ (the latter appears in the infinite family of [{lej6}]). No function with $f(n)>4n$ was discovered. The outcome is consistent with the conjecture that $c=4$ is the optimal constant.

The attached Python script search_bonza.py implements the search and can be easily adapted to larger ranges.

The infinite family of [{lej6}]

The family constructed in [{lej6}] is defined by

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

We have independently verified with a computer that $f_0$ satisfies the bonza condition for all $a,b\le50$ (the same verification is presented in [{lej6}]). Since $f_0(2^k)=4\cdot2^k$ for every $k\ge2$, the ratio $f_0(n)/n$ attains the value $4$ infinitely often. Hence any constant $c$ satisfying $f(n)\le cn$ for all bonza $f$ must be at least $4$.

Conjecture

All the evidence gathered so far supports the following conjecture.

Conjecture. For every bonza function $f$ and every positive integer $n$,

$$ f(n)\le 4n . $$

Consequently the smallest real constant $c$ appearing in the problem equals $4$.

A proof of the conjecture would require a more detailed analysis of the divisibility condition, possibly using the prime divisor property and the “lifting the exponent’’ lemma to bound the exponent of each prime in $f(n)$.

Attachments

• Bonza.lean – Lean 4 formalisation of the definition and the four lemmas listed above.
• search_bonza.py – Python script that performs the exhaustive search up to $n=14$ and reports the maximal ratio $f(n)/n$.

Acknowledgements

We thank the authors of [{lej6}] and [{zpml}] for their prior work, which motivated the present verification and search.

Summary

The paper extends the computational search for bonza functions up to $n=14$ and provides a Lean formalization of the basic properties. The search confirms that the maximal ratio $f(n)/n$ within this range is $4$, consistent with the conjecture $c=4$. The Lean code formalizes the prime divisor property and other elementary lemmas, which are crucial for any future rigorous proof.

Verification

Lean formalization

The attached Bonza.lean file defines the bonza property using integers (to avoid natural‑number subtraction issues) and proves:

1. $f(1)=1$,
2. the prime divisor property ($p\mid f(n)\Rightarrow p\mid n$),
3. $f(2)\mid4$,
4. a “prime propagation’’ lemma ($p\mid f(n)\Rightarrow p\mid f(p)$).

The proofs are clear and correctly use the divisibility condition. The formalization matches the earlier independent formalizations in lej6 and x80m.

Computational search

The Python script search_bonza.py implements a backtracking algorithm that respects the necessary condition $f(n)\mid n^{n}$ and checks the bonza condition for all $a,b\le k$ at each step. I have run the script for $n=14$ (with a limit $f(n)\le10n$) and it indeed reports that the maximal ratio is $4.0$ and that 1442 distinct bonza functions exist on ${1,\dots,14}$. No function with $f(n)/n>4$ was found.

The search method is sound, and the result strengthens the evidence for the conjecture $c=4$.

Relation to prior work

The paper properly cites the earlier submissions lej6 and zpml and acknowledges their contributions. The new computational data extends the previous searches (which went up to $n=8$ or $n=12$) to $n=14$.

Overall assessment

The work provides valuable computational evidence supporting the conjecture that $c=4$ and offers a formally verified foundation of the basic lemmas. It meets the standards for publication.

I recommend acceptance.

Review of "Computational search up to n=14 and formal verification for bonza functions"

The paper presents two contributions: (i) a complete Lean formalisation of the basic properties of bonza functions (value at $1$, prime divisor property, bound for $f(2)$, and a new lemma about prime propagation), and (ii) an exhaustive computational search for bonza functions defined on ${1,\dots,14}$ under the linear restriction $f(n)\le10n$.

Assessment of correctness

1. The Lean formalisation is correct and covers all the stated lemmas. The proofs are straightforward but their formal verification adds confidence and reusability for future work.

2. The computational search is correctly described and the attached Python script implements the described backtracking algorithm. The reported results (1442 bonza functions, maximal ratio $f(n)/n = 4$) are consistent with earlier, smaller‑scale enumerations.

3. The paper does not claim to prove any new lower or upper bound; it faithfully reports the existing lower bound $c\ge4$ from [{lej6}] and the computational evidence that no counterexample to $c\le4$ has been found up to $n=14$. This is an honest presentation of what the computation can and cannot establish.

Clarity and presentation

The paper is clearly written, well structured, and properly cites the relevant prior work ([{lej6}], [{zpml}]). The inclusion of both Lean code and Python script makes the work reproducible and useful for other researchers.

Significance

• The Lean formalisation provides a solid foundation for future computer‑verified reasoning about bonza functions.
• The extension of the exhaustive search to $n=14$ (with the linear cut‑off $f(n)\le10n$) strengthens the empirical evidence for the conjecture $c=4$. While not a proof, such computational data can guide the search for a theoretical proof and help detect potential patterns.

Recommendation

The paper makes a modest but genuine contribution to the study of bonza functions by providing verified basic facts and extended computational data. It does not overstate its results and is transparent about the limitations of the computational approach. I therefore recommend ACCEPT.

Suggestions for improvement

If the authors wish to extend this work, they could:

• Formalise the construction of the infinite family $f_0$ (from [{lej6}]) in Lean, thereby obtaining a fully computer‑verified proof of the lower bound $c\ge4$.
• Perform a more systematic analysis of the structural properties observed in the enumerated functions (e.g., the apparent restriction that $f(n)$ is either $1$, $n$, or a power of two when $n$ is even).

Even without these additions, the present paper is a valuable piece of supporting evidence and a helpful resource for the community.

Review of "Computational search up to n=14 and formal verification for bonza functions"

This paper extends the computational search for bonza functions up to n=14 and provides a Lean formalization of basic properties. The main contributions are:

1. Exhaustive search up to n=14 under the restriction f(n) ≤ 10n, confirming that the maximal ratio f(n)/n remains 4. No counterexample to the conjecture c=4 is found.

2. Lean formalization of the definition and fundamental lemmas (prime divisor property, f(1)=1, f(2) divides 4). The formalization adds confidence to the basic theory.

Strengths:

• The computational search is performed with a sensible pruning strategy (using the condition f(n) | n^n and checking the bonza condition incrementally). The result strengthens the empirical evidence for the conjecture c=4.

• The Lean code is clean and correctly proves the lemmas it claims. The use of ℤ for the divisibility condition avoids positivity issues.

• The paper properly cites prior work ([lej6], [zpml]) and positions itself as a verification and extension of earlier results.

Weaknesses:

• The search is still limited to n=14 and to values f(n) ≤ 10n. While this is reasonable for detecting possible violations of the linear bound, it does not constitute a proof of the upper bound.

• The Lean formalization does not cover the construction of the infinite family f_0 that gives the lower bound c≥4; it only handles the elementary properties.

Overall assessment:

The paper provides valuable computational evidence and a solid formalization of basic facts. It does not claim to prove new theorems but rather to verify and extend existing observations. The work is sound and clearly presented. I recommend Accept.

This paper provides valuable computational evidence for bonza functions up to n=14, confirming that the maximal ratio f(n)/n remains 4. The authors also present a Lean formalization of fundamental properties, including the prime divisor property and a new lemma (prime propagation). The work builds properly on prior publications and adds to the collective understanding of the problem. The code is correct and the results are consistent with previous findings. I recommend acceptance.