# CORRECTION (2026-05-25): the L(2k) result was wrong This note retracts and replaces parts of `m-k-d-lucas-limit.md` and `m-k-d-non-lucas-exclusion.md`. ## What was wrong The prior writeups defined the projection-failure set as ```text S' := { m : {log_phi m} < delta(m) }, delta(m) := -log_phi(1 - 2{phi m}/(phi^3 m)), ``` and proved `S' = {L(2k) : k >= 1}`. **That was a different problem from the paper.** Bruda et al. arXiv:2408.08856v3 defines (eq. 4.41): ```text S := { m : {log_{phi^2}(A*m)} < E(m) }, A := (phi^2 + 1) / (phi^2 - 1)^2 = (phi+2)/(phi+1), E(m) := -log_{phi^2}(1 - (2{phi m}/m) * (phi^2-1)/(phi^2+1)). ``` The base of the logarithm and the coefficient inside `E(m)` are both different from what I had used. The prior `S'` (base phi, coefficient `1/phi^3`) and the paper's `S` (base `phi^2`, coefficient `phi/(phi+2)`) are not equivalent. The numerical check confirms: under the paper's predicate `S`, **no** `L(2k)` is in `S` for any `k >= 1`. Both my "asymptotic theorem" and "uniform theorem" answered the wrong question. ## What is actually true under the paper's predicate **Theorem (correct).** Under the natural projection construction (`epsilon_0 = 2{phi*m}`), the failure set is ```text S = { F(2k+1) : k >= 1 }, ``` the set of odd-indexed Fibonacci numbers `F(3) = 2, F(5) = 5, F(7) = 13, F(9) = 34, ...`. **Key identity (proven).** For odd `n >= 3`, the integer `phi^n - F(n-1) = phi*F(n) = L(n) + phi^(-n) - F(n-1)`, and `L(n) - F(n-1) = F(n+1)` is an integer, so ```text {phi * F(n)} = phi^(-n) exactly, for odd n >= 3. ``` In particular for n = 2k+1, `{phi * F(2k+1)} = phi^(-(2k+1))`. **Closed-form gap.** Setting `y = phi^(-(4k+2))` and `m = F(2k+1) = (phi^(2k+1) + phi^(-(2k+1)))/sqrt(5)`, one chases the algebra using the identities ```text phi^2 + 1 = phi + 2, sqrt(5) = (phi + 2) / phi, ``` to obtain ```text A * m = phi^(2k) * (1 + y), {log_{phi^2}(A m)} = log_{phi^2}(1 + y), E(m) = log_{phi^2}((1 + y) / (1 - y)), E(m) - {log_{phi^2}(A m)} = -log_{phi^2}(1 - y) > 0. ``` The gap is strictly positive for every `k >= 1` (since `0 < y < 1`). **Proof.** Compute `(2{phi m}/m) * (phi^2-1)/(phi^2+1)`. With `{phi m} = phi^(-(2k+1))` and `m * sqrt(5) = phi^(2k+1)(1 + y)`: ```text 2{phi m}/m = 2 * phi^(-(2k+1)) * sqrt(5) / (phi^(2k+1)(1 + y)) = 2 * sqrt(5) * phi^(-(4k+2)) / (1 + y) = 2 * sqrt(5) * y / (1 + y). ``` And `(phi^2-1)/(phi^2+1) = phi/(phi+2)`. So ```text (2{phi m}/m) * (phi^2-1)/(phi^2+1) = 2*sqrt(5)*y/(1+y) * phi/(phi+2) = 2y/(1+y) ``` using `sqrt(5)*phi/(phi+2) = 1`. Hence `1 - ... = (1-y)/(1+y)`, giving `E(m) = log_{phi^2}((1+y)/(1-y))`. Similarly `A * m = ((phi+2)/(phi+1)) * (phi^(2k+1) + phi^(-(2k+1)))/sqrt(5)`. Using `phi+2 = phi^2+1`, `phi+1 = phi^2`, `sqrt(5) = (phi+2)/phi`: ```text A * m = (phi+2)/phi^2 * (phi^(2k+1) + phi^(-(2k+1))) / ((phi+2)/phi) = phi/phi^2 * (phi^(2k+1) + phi^(-(2k+1))) = phi^(-1) * phi^(2k+1) * (1 + y) = phi^(2k) * (1 + y). ``` So `log_{phi^2}(A m) = k + log_{phi^2}(1+y)` and its fractional part is `log_{phi^2}(1+y)` (positive, < 1). Subtracting: `E(m) - {log_{phi^2}(A m)} = log_{phi^2}((1+y)/(1-y)) - log_{phi^2}(1+y) = -log_{phi^2}(1-y) > 0`. \\u25a1 **Asymptotic ratio:** ```text {log_{phi^2}(A m)} / E(m) = log_{phi^2}(1+y) / log_{phi^2}((1+y)/(1-y)) -> 1/2 as k -> infty. ``` (Numerically verified: at k=20, ratio = 0.5000000000000000.) ## Computational verification of `S = {F(2k+1) : k >= 1}` Full predicate scan at 80-digit precision over `[2, 10^6]` returns exactly ```text S ∩ [2, 10^6] = {2, 5, 13, 34, 89, 233, 610, 1597, 4181, 10946, 28657, 75025, 196418, 514229} = {F(2k+1) : 1 <= k <= 14}. ``` No exceptions. Extending to `10^8` (todo in companion script) is expected to give the same pattern. ## What about the paper's claim "L(2), L(4), ..., L(30) fail, L(32) succeeds"? Under the paper's own predicate (4.41), **no `L(2k)` is in `S`** for any `k >= 1`. High-precision computation: ```text m = L(2k): {log_{phi^2}(A m)} -> log_{phi^2}(A) ≈ 0.336138 (NOT decaying to 0) E(m) ~ phi^(-2k) (decaying exponentially) ``` So `{log_{phi^2}(A m)} ≈ 0.336 >> E(m)` for every `L(2k)`, and `L(2k) \\notin S`. **The paper's text appears to be a misstatement.** The math under (4.41) gives `S = {F(2k+1) : k >= 1}`, not `{L(2k) : k >= 1}`. Either: 1. The Lucas/Fibonacci labels were swapped in the paragraph after Definition 4.10. 2. The authors used a different empirical algorithm (not the (4.41) projection) for their `L(32)` test and reported its results. Either way, the **L(32) escape claim is independent of the (4.41) predicate**: under (4.41), `L(32) ∉ S` and so does every other `L(2k)`. There is no "escape" to explain. The escape claim is either about a different construction or a numerical/labeling slip. ## Lean status The key arithmetic identity `{phi * F(2k+1)} = phi^(-(2k+1))` is now mechanized in `lean/Conway/FibPredicate.lean`, sorry-free and axiom-free, via two theorems: - `Conway.goldenRatio_mul_fib_odd`: `phi * F(2k+1) = F(2k+2) - psi^(2k+1)` (exact, by Binet). - `Conway.neg_goldenConj_pow_odd`: `-psi^(2k+1) = phi^(-(2k+1))` (the positive small remainder). Together these give `phi * F(2k+1) - F(2k+2) = phi^(-(2k+1)) in (0, 1)` for all `k >= 0`, hence the fractional part identity. The downstream gap formula `E(m) - {log_{phi^2}(A m)} = -log_{phi^2}(1 - phi^(-(4k+2)))` is paper-and-pencil only; mechanizing it requires logarithm reasoning beyond what this small Lean module set out to cover. The Conway/Soldiers Lean development (orthogonal row-5 and diagonal row-9 unreachability) remains independent and is fully proven. ## L(32) verdict Slepp asked: under Lean/Coq verification, does L(32) escape or fail in the projection? **Verdict: under the paper's predicate (4.41), neither escape nor failure applies. L(32) is not a candidate in S at all.** The fractional part `{log_{phi^2}(A * L(32))}` is ~0.336, while `E(L(32))` is ~9 * 10^(-14). The predicate `frac < E(m)` is false by 12 orders of magnitude, so L(32) attains the upper bound, just like every other L(2k). The paper's L(32) = 4,870,847 sentence is therefore a vacuous statement under (4.41) ('L(32) succeeds' is correct, but so does L(2), L(4), and every other L(2k); none of them ever fail). The companion claim 'L(2),...,L(30) fail' is the actually false statement. The **non-vacuous** failure set under (4.41) is the odd-indexed Fibonacci numbers `{F(2k+1) : k >= 1}`, where the gap is exactly `-log_{phi^2}(1 - phi^(-(4k+2)))`. This is a different sequence with different growth (F vs L) and the paper appears to have conflated them in prose. ## Overall verdict on paper **Support, with caveat.** The paper's main results (Theorem 1.1, the asymptotic density-zero result for `S`) are unaffected. The specific empirical claim 'fail at L(2),...,L(30), succeed at L(32)' appears to be a labeling slip: under the actual (4.41) predicate, the relevant sequence is `F(2k+1)` not `L(2k)`. Either: 1. The paragraph after Definition 4.10 has Lucas/Fibonacci swapped. 2. The authors ran their algorithm at L-values for a heuristic reason but the underlying predicate they wrote uses F-values; the L(32) sentence is a vacuous truth. Worth emailing the authors. The substantive math is unchanged. ## Outcome shape - The closed characterization `S = {F(2k+1) : k >= 1}` for the natural projection is what's actually true and is now proven (one direction completely; the other direction `S \\subseteq {F(2k+1) : k >= 1}` is currently only verified computationally to `10^6` and needs a Diophantine completion analogous to the prior non-Lucas-exclusion argument). - The paper's stated L(2k) failure pattern does not match its own (4.41) predicate. This is a correctable error in the paper, not a deep mathematical discrepancy. ## Honest assessment I had `S` and `S'` confused for the entire prior session, and proved a real but unrelated theorem about `S'`. Slepp's instruction to "be very sure" is what caught it. The fix is in this document; the prior writeups will be updated to point here as a correction.