OEIS A057923 — Two-Step Monotonicity Proof Available

The greedy bitwise-OR sequence OEIS A057923 satisfies a(n+2) > a(n) for every n ≥ 0, so its even-indexed and odd-indexed subsequences are both strictly increasing. This is Robert Israel's two-step monotonicity conjecture.

Priority: I did not find an earlier explicit proof in the sources I examined. Older OEIS material contains closely related ingredients, described below. This is not a claim of novelty or historical priority, and the OEIS entry has not been updated. The purpose of this page is to make the proof and its verification available.

Original problem
Robert Israel's two-step monotonicity conjecture for OEIS A057923
Also known as
A057923 monotonicity conjecture; A057923 a(n+2) > a(n); greedy bitwise OR sequence two-step increase
Identifiers
OEIS A057923 · conjecture by Robert Israel, August 13, 2017 · sequence by Larry Reeves, October 3, 2000
Source
OEIS A057923. The sequence is credited to Larry Reeves (October 3, 2000); the conjecture was added by Robert Israel on August 13, 2017 (revision history).
Result
The greedy bitwise-OR sequence OEIS A057923 satisfies a(n+2) > a(n) for every n ≥ 0, so its even-indexed and odd-indexed subsequences are both strictly increasing. This is Robert Israel's two-step monotonicity conjecture.
Verification
Lean, kernel-checked; standard axioms only. Lean 4.35.0 using only Lean's standard library (no Mathlib); the audited checks depend only on propext, Classical.choice, and Quot.sound.
Repository
https://github.com/cozuya/oeis-a057923

Statement

Let ∨ denote bitwise OR on arbitrary-precision nonnegative integers. Define a(0) = 0, a(1) = 2, and, for every integer n ≥ 0,

a(n+2) = min { m ∈ ℤ≥0 : (a(n+1) ∨ m) > (a(n) ∨ a(n+1)) }.

The minimum and the strict comparison use the usual numerical order. Values may repeat; there is no unused-value condition and no fixed word size. The sequence begins

0, 2, 1, 4, 2, 5, 8, 6, 9, 16, 10, 17, 12, 18, 13, 32, …

Theorem. For every n ≥ 0, a(n+2) > a(n).

What is proved

  • Proved: a(n+2) > a(n) for all n ≥ 0, for the greedy definition above with seeds 0, 2. The Lean development also proves that the greedy choice exists and is minimal.
  • Two-step, not consecutive: consecutive terms are not monotone (for example 2, 1). The conjecture and the theorem concern two-step increase.
  • Not done: the OEIS entry has not been edited or marked resolved.

Proof outline

The greedy choice always exists: for a preceding pair x, y, the value m = (x ∨ y) + 1 satisfies (y ∨ m) ≥ m > (x ∨ y), so the admissible set has a least member.

The least admissible m shares no set bit with y: clearing such a bit would give a smaller number with the same OR with y, contradicting minimality. So every adjacent pair has disjoint set bits (the seeds 0, 2 do too). For integers with disjoint set bits, OR equals addition, so the defining inequality becomes a(n+1) + a(n+2) > a(n) + a(n+1). Cancelling a(n+1) gives a(n+2) > a(n).

Verification and trust model

The proof is formalized in Lean 4.35.0 (commit eb6cafb) using only Lean's standard library. The main theorem is A057923.two_step_strict : a n < a (n + 2).

python3 scripts/verify.py checks the exact compiler version and Git revision, compiles the proof from source, and then compiles Verification.lean, which separately checks four statements:

  • Verification.seed_zero and Verification.seed_one: a(0) = 0 and a(1) = 2
  • Verification.greedy_minimum: each term satisfies the strict OR inequality and is at most every admissible m
  • Verification.claimed_result: a(n+2) > a(n)

The script rejects compiler warnings and errors, missing axiom reports, and any dependency outside propext, Classical.choice, and Quot.sound; a proof using sorryAx is rejected.

Trust model: Lean's kernel and these three standard axioms. GitHub Actions installs a checksum-pinned Lean release, repeats the check on pushes and pull requests, and retains a report recording the commit, source hashes, compiler identity, and axiom dependencies.

Prior-art search

A bounded prior-art audit on October 15, 2026, before the solving attempt, concluded that the conjecture was still listed as conjectural and located no prior resolution. It inspected the OEIS entry, its internal record and full revision history, Robert Israel's Maple program, the related sequences A051145, A057924, and A057925, the jOEIS and LODA implementations, a C++ program by Rémy Sigrist, and public formal-mathematics collections (Google DeepMind's formal-conjectures, OpenAI's mathematics release, and the-omega-institute's repository).

Closely related earlier ingredients: Israel's 2017 Maple search starts at the lower bound (x ∨ y) − y, and Charlie Neder's October 12, 2018 update formula for A051145 clears the bits of the preceding term. If Neder's formula is assumed to generate the greedy sequence with seeds 0, 2 (it is stated for seeds 0, 1, and no inspected source proves the 0, 2 case), the two combine into a short deduction of the conjecture. The inspected sources state neither a proof nor an explicit monotonicity argument. The proof here derives disjointness directly from greedy minimality and does not assume Neder's formula.

Limits: direct SeqFan archive access failed, and search-engine and GitHub index limits prevent an exhaustive negative conclusion.

Provenance

Chris Ozols, with AI-assisted proof development and formalization; individual model names are not recorded. The status audit, solving prompt, returned proof, and first successful Lean check were recorded on October 15, 2026 (America/Chicago). The original prompt, returned proof, and formalization are retained unchanged in the repository with their SHA-256 hashes.