The OEIS A175406 Greathouse Floor Formula

Abstract

The OEIS A175406 floor formula is refuted at a large explicit index.

Definition 1.1 (The sequence value).

$$\begin{array}{c}\forall n\in \mathbb{N},\\ a(n)=\mathrm{sSup}\left\{\begin{array}{c}k\in \mathbb{N}\mid (1+1/n{)}^k\le 2\end{array}\right\}\end{array}$$

Formalization. D5/S0/Certificates/GreathouseLogTwoFloorRefutation.a (✓ std3).

Citation. Charles R Greathouse IV; Zak Seidov (2012). OEIS A175406, The greatest integer k such that (1+1/n)^k <= 2. URL: https://oeis.org/A175406.

Commentary.

For each natural n, including zero, a(n) takes the natural sSup of exponents k satisfying the displayed bound. Powers and division are real, with Lean’s 1/0 = 0 convention. Natural sSup is 0 for unbounded sets, so a is total.

Definition 1.2 (Greathouse’s floor conjecture).

$$\begin{array}{c}\mathrm{claim}\iff \\ \forall n\in \mathbb{N},n\ge 1\Rightarrow \\ a(n)=\lfloor (n+1/2)\log 2{\rfloor }_{+}\end{array}$$

Formalization. D5/S0/Certificates/GreathouseLogTwoFloorRefutation.claim (✓ std3).

Citation. Charles R Greathouse IV; Zak Seidov (2012). OEIS A175406, The greatest integer k such that (1+1/n)^k <= 2. URL: https://oeis.org/A175406.

Commentary.

For every positive natural n, the conjecture identifies a(n) with the displayed natural floor. The subscript plus denotes Nat.floor, and log is the natural logarithm.

Theorem 1.3 (The floor conjecture is false).

$$\neg \mathrm{claim}$$

Proof. Machine-checked in Lean as D5/S0/Certificates/GreathouseLogTwoFloorRefutation.result (✓ std3). ∎

Resolves. Problems/oeis-a175406-log-two-floor-refutation (refuted) by D5/S0/Certificates/GreathouseLogTwoFloorRefutation.result.

Source. Repository-derived.

Acknowledgement. Charles R Greathouse IV; Zak Seidov (2012). OEIS A175406, The greatest integer k such that (1+1/n)^k <= 2. URL: https://oeis.org/A175406.

Commentary.

At n0 = 1121626023352383, let M = 777451915729368. The certified log-series estimates give the stated natural floor as M, while the defining supremum is M - 1: the M-th power is greater than 2 and the (M - 1)-st power is at most 2. The proof uses 36 positive terms and a geometric tail for log 2, two positive terms for the witness logarithm, and log(1+x) <= x. No minimality claim is made.

References

• Truth anchor: D5/S0/Certificates/GreathouseLogTwoFloorRefutation.a
• Truth anchor: D5/S0/Certificates/GreathouseLogTwoFloorRefutation.claim
• Truth anchor: D5/S0/Certificates/GreathouseLogTwoFloorRefutation.result