Skip to content

[Help Wanted] Problem #257: Lean Formalization of a Solution #217

@danuaemx

Description

@danuaemx

Description

Hello, I would like to contribute regarding the formalization status and mathematical context of this problem.

I have worked on an article about, the manuscript is available at 10.5281/zenodo.18321596.

Below is a summary of the definitions and the proof strategy employed, specifically regarding the growth of the multiplicative order, the Diophantine constraints on carries, and the filtration method for arbitrary sets. Notably, due to the recursive and deterministic nature of this construction, the proof strategy admits a direct and simplified implementation in Lean.

Early Formalization

An early formalization draft in the file Erdos\Basic.lean available at the Repository . This code was developed with AI assistance (using GPT-5.2 in VSCode with Copilot). It currently formalizes the core concepts of the recursive period and smoothness shells, but relies on a single axiom density regarding the bounds of the Diophantine Region to close the stability proof.

Context: Definitions and Proof Strategy

1. Definitions

  • The Set and Exponents: Let $A = \{ a_1, a_2, \dots \} \subset \mathbb{N}$ be an infinite strictly ordered subset. For each generator $a \in A$, we define a finite set of ordered exponents $E_a = {e_{a,1}, \dots, e_{a, \max}}$.
  • The Target Sum: We analyze the irrationality of the sum formed by the effective exponents $x = a^e$:
    $$S = \sum_{a \in A} \sum_{e \in E_a} \frac{1}{b^{a^e} - 1}$$

2. The Ordinal Growth ($\text{ord}_b$)
We define the fundamental period $L_N$ of the partial sum as the multiplicative order of the base $b$ modulo the denominator $Q_N$. The proof relies on the behavior of this ordinal:
$$L_N := \text{ord}_b(Q_N) = \min \{k \ge 1 : b^k \equiv 1 \pmod{Q_N}\}$$

The growth of this period depends strictly on the arithmetic structure of $A$:

  • Case A (Pairwise Coprime): If elements of $A$ are pairwise coprime (see the manuscript for the proof), the period grows strictly multiplicatively. Using the dominant term $a^m_{N+1} = a_{N+1}^{\max(E_{N+1})}$, we have:
    $$L_{N+1} = L_N a^m_{N+1}$$

  • Case B (Arbitrary Sets - Non-Coprime): When $A$ is arbitrary, we define the Cumulative Active Set $\mathcal{A}^{(k)} = \{ a \in A \mid P(a) \le p_k \}$, where $P(a)$ is the largest prime factor.
    The period grows via the Least Common Multiple (LCM):
    $$L_k = \text{lcm}(\mathcal{A}^{(k)}) $$
    In the infinite limit, this converges to a Steinitz number (supernatural number).

Empirical Analysis of Denominator and Period Correlation

We examine the arithmetic growth of the partial sum's denominator $Q_N$ relative to the fundamental period $L_N$. The tables below present the data for bases $b \in {2, 3, 11}$ iterating through the first 8 prime exponents.

Key Observation

Although the arithmetic value of the denominator $Q_N$ varies wildly depending on the base (ranging from $10^{22}$ to $10^{79}$ for $i=8$), the multiplicative order (and thus the period $L_N$) remains structurally invariant:
$$L_N(b=2) = L_N(b=3) = L_N(b=11)$$
This empirically confirms that the period is determined exclusively by the LCM of the exponents $$L_N = \text{lcm} (p_1, \dots, p_i)$$ not by the base.

Table 1: Base $b=2$

For the classical Erdős sum $\sum \frac{1}{2^p-1}$.

  • $Q_N$: Cumulative denominator $\text{lcm}(2^{p_1}-1, \dots, 2^{p_i}-1)$.
  • $\text{ord}_2(Q_N)$: The fundamental period in base 2.
Iteration ($i$) Denominator $Q_N$ $\text{ord}_2(Q_N)$
1 ($p=2$) $3$ 2
2 ($p=3$) $21$ 6
3 ($p=5$) $651$ 30
4 ($p=7$) $82,677$ 210
5 ($p=11$) $1.69 \times 10^8$ 2,310
6 ($p=13$) $1.39 \times 10^{12}$ 30,030
7 ($p=17$) $1.82 \times 10^{17}$ 510,510
8 ($p=19$) $9.56 \times 10^{22}$ 9,699,690

Table 2: Base $b=3$

For the variant sum $\sum \frac{1}{3^p-1}$.

Iteration ($i$) Denominator $Q_N$ $\text{ord}_3(Q_N)$
1 ($p=2$) $8$ 2
2 ($p=3$) $104$ 6
3 ($p=5$) $12,584$ 30
4 ($p=7$) $1.37 \times 10^7$ 210
5 ($p=11$) $1.21 \times 10^{12}$ 2,310
6 ($p=13$) $9.68 \times 10^{17}$ 30,030
7 ($p=17$) $6.27 \times 10^{25}$ 510,510
8 ($p=19$) $\approx 3.6 \times 10^{34}$ 9,699,690

Table 3: Base $b=11$

For the variant sum $\sum \frac{1}{11^p-1}$.

Iteration ($i$) Denominator $Q_N$ $\text{ord}_{11}(Q_N)$
1 ($p=2$) $120$ 2
2 ($p=3$) $15,960$ 6
3 ($p=5$) $2.56 \times 10^{10}$ 30
4 ($p=7$) $4.99 \times 10^{17}$ 210
5 ($p=11$) $\approx 1.4 \times 10^{28}$ 2,310
6 ($p=13$) $\approx 4.2 \times 10^{41}$ 30,030
7 ($p=17$) $\approx 2.1 \times 10^{59}$ 510,510
8 ($p=19$) $\approx 1.3 \times 10^{79}$ 9,699,690

3. Smoothness Filtration (General Case)
To resolve the general case where coprimality is not guaranteed, we introduce a Smoothness Shell Filtration. We partition the arbitrary set $A$ into differential shells based on the largest prime factor $P(n)$:
$$\Delta \Psi_k = \{ n \in A \mid P(n) = p_k \}$$
This reorders the summation so that the period $L_k$ at step $k$ absorbs all arithmetic complexity from primes $p \le p_k$.

3. Diophantine Stability and Carry Control
To ensure that the digital blocks defined by $L_N$ are not corrupted by arithmetic overflows, we define a Diophantine Region $\mathcal{R}$ (proven in the article). The key is to control the carries in the augmented blocks $C'(N,q)$ Formed by the background period $C_N$ and the perturbation $B(N+1,q)$:
$$C'(N,q) = C_N + B(N+1,q)$$
We demonstrate that the "carry propagation" is confined to a logarithmic neighborhood using the density bounds of $\mathcal{R}$. This guarantees that the period boundaries remain stable.

The condition for structural interference (carry propagation), The structural analysis iterates over the sub-block indices $q \in \{1, \dots, L_k/L_{k-1}\}$ for any active generator $n \in \Delta \Psi_k$. In the general case is governed by the modular constraints of the region:
$$q \cdot L_{k-1} \equiv z \pmod n, \quad \text{subject to} \quad 1 \le z \le \lfloor \log_b(n) \rfloor + 1$$
We demonstrate that the density of indices $q$ satisfying this condition vanishes asymptotically, guaranteeing that the period boundaries remain stable.

5. Result Proven
We establish the unconditional irrationality of $S$ in the current maunscript. The proof demonstrates that the introduction of the new prime factor $p_k$ in the $k$-th smoothness shell creates a "Witness Term" with maximal $p$-adic valuation. This induces a topological obstruction in the profinite limit $\hat{\mathbb{Z}}$, preventing the sequence of digits from stabilizing into a rational period.

This obstruction relies on the CRT decomposition (Inversion Equation) of the Witness Term $n^{*}$:
$$n^{*} = M \cdot p_k^e$$.The phase shift introduced by the Witness Term is governed by the modular congruence:
$$q \cdot L_{k-1} \equiv z_q \pmod{n^*}$$

Metadata

Metadata

Assignees

No one assigned

    Labels

    help wantedExtra attention is needed

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions