slug: oeis-a175406-log-two-floor-refutation bibkey: greathouse2012a175406 doi: null url: https://oeis.org/A175406 triage: theorem motivation_gids:

• D5/S0/Certificates/GreathouseLogTwoFloorRefutation

Refutation of the A175406 floor formula conjecture

Problem

OEIS A175406 %N (verbatim):

The greatest integer k such that (1+1/n)^k <= 2

OEIS A175406 %C (verbatim):

The sequence of first differences consists of zeros and ones, with no two consecutive zeros and no more than three consecutive ones.

OEIS A175406 %F (verbatim):

a(n) = n log 2 + O(1). Conjecture: a(n) = floor((n + 1/2) log 2). - Charles R Greathouse IV, Apr 03 2012

OEIS A175406 %A (verbatim):

Zak Seidov, May 01 2010

The literal claim formalized here is ∀ n : ℕ, 1 ≤ n → a n = ⌊((n : ℝ) + 1 / 2) * Real.log 2⌋₊. The definition of a uses the literal natural supremum sSup {k : ℕ | (1 + 1 / (n : ℝ)) ^ k ≤ 2}; in the natural conditionally complete order, an unbounded set has sSup = 0. The result refutes this universal claim at one explicit positive index.

Motivation

The entry presents a universal floor formula for the greatest admissible exponent. A kernel-checked explicit counterexample resolves the literal conjecture while leaving the asymptotic statement and the difference-pattern observation as separate questions.

Gap

The search record on preregistration issue #7587 and the probe report is dated September 13, 2026. The OEIS history has 25 revisions: revision 3 introduced the conjecture, and revision 25 (2026-03-09) still marks it as a conjecture. The bounded search found 0 arXiv results, 0 results for OEIS Open arXiv:2608.11941 and LeanOpenProblems, 0 in formal-conjectures, 0 on MathOverflow, and 0 across DataCite / OpenAIRE. OpenAlex returned HTTP 429 and is ASSUMED-UNVERIFIED. Heuristically equidistribution suggests that the floor conjecture must fail somewhere, and no explicit counterexample was found in the surfaces listed above (bounded search; OpenAlex unverified) before this witness; no priority claim is made.

Route

The proof uses one certified estimate chain. (i) Real.hasSum_log_one_add_inv at a = 1 gives the 36-term lower sum S36 and the geometric upper tail S36 + 3⁻⁷² for log 2. (ii) At n₀ = 1121626023352383, the same series gives a lower bound from its first two positive terms for log(1 + 1/n₀), while Real.log_le_sub_one_of_pos gives the upper bound log(1 + x) ≤ x. (iii) Exact rational normalization yields ⌊(n₀ + 1/2) log 2⌋₊ = M with M = 777451915729368, and proves (1 + 1/n₀)^M > 2 while (1 + 1/n₀)^(M−1) ≤ 2. Hence the defining supremum is M − 1, not M.

The search seat found the witness through the continued fraction of log(2)/2; the convergent index was 36 and q = 2n₀ + 1. This is context only.

Falsifier

A proof of the literal universal claim would contradict the kernel theorem D5/S0/Certificates/GreathouseLogTwoFloorRefutation.result, because its specialized value at n₀ would identify a(n₀) with M even though the certified defining supremum is M − 1.

Evidence

• Lean module: D5/S0/Certificates/GreathouseLogTwoFloorRefutation.lean.
• Main theorem: result : ¬ claim, with std3 axioms propext, Classical.choice, and Quot.sound.
• Step 0 import deletion exits were: Mathlib.Algebra.Order.Floor.Semiring=0, Mathlib.Analysis.SpecialFunctions.Log.Deriv=1, Mathlib.Analysis.SpecialFunctions.Pow.Real=1, and Mathlib.Tactic.NormNum=0. The retained anchors are the two imports whose deletion breaks the build.
• The Step 0 profiler on the stamped hot tree reported 7.14 seconds wall time, 31.8 ms cumulative type checking, and 2,400,796,672 bytes maximum RSS.
• An independent 80-digit decimal recomputation found 0 mismatches for 1 ≤ n ≤ 20000, and recorded (n₀ + 1/2)·log 2 − M = +1.476015…×10⁻¹⁷ and M·log(1 + 1/n₀) − log 2 = +3.275470…×10⁻³².
• The probe’s Decimal(100) reading agrees and gives (M − 1)·log(1 + 1/n₀) − log 2 = −8.916×10⁻¹⁶.

Triage

theorem. The explicit kernel-checked witness refutes the literal universal floor formula and does not propose a corrected formula.

ASSUMED-UNVERIFIED

OpenAlex returned HTTP 429. The literature search is bounded, and no claim of exhaustive publication coverage is made. Minimality (not claimed): the search seat’s Legendre-reduction argument that n₀ is the least counterexample is unverified and is not formalized.