target: longest run of zeros in binary √2 (weak bound Lₙ ≤ n+1)

[thedavidyoungblood]

The theorem

Statement (plain English):

A run of L zero-bits immediately following position n in the binary
expansion of √2 has length at most n + 1. (Equivalently: if the fractional
part of 2ⁿ·√2 is below 2⁻ᴸ, then L ≤ n + 1.) This is the weak bound
Granville proves; it is far from his open log₂ n conjecture, which is NOT
proposed here (unsorry does not attack open conjectures).

Proposed Lean 4 statement:

theorem sqrt_two_zero_run_le (n L : ℕ)
    (h : Int.fract ((2 : ℝ) ^ n * Real.sqrt 2) < 1 / (2 : ℝ) ^ L) :
    L ≤ n + 1 := by sorry

Statement-fidelity note (for the maintainer lowering this): "a run of L
zeros after position n" is encoded as Int.fract (2ⁿ√2) < 2⁻ᴸ, the standard
"next L binary digits are zero" condition. If you prefer a digit-indexed
encoding, the proof rebinds easily — the core lemma is
Int.fract (2ⁿ√2) ≥ 2⁻⁽ⁿ⁺²⁾.

It is already proven

Reference: Vincent Granville, Number Theory: Longest Runs of Zeros in
Binary Digits of Square Root of 2, MLTechniques.com, 2023-10-27; paper
RunLengths.pdf §4.3.1, Formula (4.1): for x₀ = √(p/q),
Lₙ ≤ n + 2 + ½·log₂(pq); specialized to √2 this gives Lₙ ≤ n + 1. The proof
is elementary (a positive-integer gap argument from the irrationality of √2).

A self-contained, kernel-verified Lean proof is available (axioms
{propext, Classical.choice, Quot.sound}, no sorryAx) and can accompany the
target — happy to open it as the proving PR once the target is admitted.

It is (probably) not in mathlib

Why absent: mathlib has no formalization of binary-digit run lengths of √2
(or of Int.fract (2ⁿ √2) bounds).

Absence check I ran (repo tool, against the pinned mathlib):

$ python3 -m tools.sourcing.check_absence \
    --pattern "sqrt_two_zero_run|zero_run_le" \
    --mathlib .lake/packages/mathlib/Mathlib
mathlib rev: c5ea00351c28e24afc9f0f84379aa41082b1188f
no local match — absent as far as grep can tell

It is not trivial

Triviality check I ran (repo tool):

$ python3 -m tools.sourcing.check_triviality goals/sqrt-two-zero-run-le.lean
NON-TRIVIAL  sqrt-two-zero-run-le

(The one-shot battery — rfl/trivial/decide/norm_num/omega/simp/simp_all/aesop/ ring/linarith/tauto — does not close it; it needs the irrationality argument.)

Difficulty (my guess)

2 — elementary, but genuinely requires the irrational_sqrt_two /
not-a-perfect-square step; not a one-liner.