From 9921de2a1fcf3255d7eb34f55cfcb3a6d8917dfc Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 03:07:00 +0000
Subject: [PATCH] refactor(Nat,Ladner): move foldr_bit_one lemmas to
 Foundations/Data/Nat/Bits (#949)

Move `foldr_bit_one_ne_zero`, `bits_foldr_bit_one`, and `foldr_bit_one_lt` from
`Complexity.Computability.Complexity.Classes.Ladner.Basic` to
`Complexity.Foundations.Data.Nat.Bits` under the `Nat` namespace.

Delete local copies in `Ladner/Basic.lean` and route call sites to `Nat.*`.
Closes item D.7 on #949.
---
 .../Complexity/Classes/Ladner/Basic.lean      | 28 ++++---------------
 Complexity/Foundations/Data/Nat/Bits.lean     | 25 +++++++++++++++++
 2 files changed, 30 insertions(+), 23 deletions(-)

diff --git a/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean b/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
index 6a50113a4c..ca78cd78ad 100644
--- a/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
+++ b/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Machi
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Compose
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Decode
 public import Complexity.Foundations.Data.List.Append
+import Complexity.Foundations.Data.Nat.Bits
 import Mathlib.Data.Nat.Size
 
 /-!
@@ -84,35 +85,16 @@ def word (j : ℕ) : List Bool := (j + 1).bits.dropLast
 `true`. -/
 def index (w : List Bool) : ℕ := w.foldr Nat.bit 1 - 1
 
-theorem foldr_bit_one_ne_zero (w : List Bool) : w.foldr Nat.bit 1 ≠ 0 := by
-  induction w with
-  | nil => simp
-  | cons b w ih => exact Nat.bit_ne_zero b ih
-
-theorem bits_foldr_bit_one (w : List Bool) : (w.foldr Nat.bit 1).bits = w ++ [true] := by
-  induction w with
-  | nil => simp
-  | cons b w ih =>
-    rw [List.foldr_cons, Nat.bits_append_bit _ _ fun h => absurd h (foldr_bit_one_ne_zero w), ih,
-      List.cons_append]
-
-theorem foldr_bit_one_lt (w : List Bool) : w.foldr Nat.bit 1 < 2 ^ (w.length + 1) := by
-  induction w with
-  | nil => simp
-  | cons b w ih =>
-    rw [List.foldr_cons, Nat.bit_val, List.length_cons, pow_succ]
-    cases b <;> simp only [Bool.toNat_false, Bool.toNat_true] <;> omega
-
 /-- **Every word has an index.** -/
 @[simp]
 theorem word_index (w : List Bool) : word (index w) = w := by
-  rw [word, index, Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr (foldr_bit_one_ne_zero w)),
-    bits_foldr_bit_one, List.dropLast_concat]
+  rw [word, index, Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr (Nat.foldr_bit_one_ne_zero w)),
+    Nat.bits_foldr_bit_one, List.dropLast_concat]
 
 /-- The index of a word of length `l` is less than `2 ^ (l + 1) - 1`. -/
 theorem index_add_two_le (w : List Bool) : index w + 2 ≤ 2 ^ (w.length + 1) := by
-  have h₁ := foldr_bit_one_lt w
-  have h₂ := foldr_bit_one_ne_zero w
+  have h₁ := Nat.foldr_bit_one_lt w
+  have h₂ := Nat.foldr_bit_one_ne_zero w
   rw [index]
   omega
 
diff --git a/Complexity/Foundations/Data/Nat/Bits.lean b/Complexity/Foundations/Data/Nat/Bits.lean
index 14dc3c4f04..ca5a106bbf 100644
--- a/Complexity/Foundations/Data/Nat/Bits.lean
+++ b/Complexity/Foundations/Data/Nat/Bits.lean
@@ -23,6 +23,8 @@ with initial value zero reconstructs the original number.
 
 * `Nat.foldr_bit_bits`: folding `Nat.bit` over the binary representation of `n` gives `n`.
 * `Nat.foldr_bit_lt`, `Nat.foldr_bit_testBit`: fixed-width little-endian reconstruction.
+* `Nat.foldr_bit_one_ne_zero`, `Nat.bits_foldr_bit_one`, `Nat.foldr_bit_one_lt`: reconstruction
+  with base value `1`, producing a positive number whose binary digits end in `true`.
 * `Nat.foldr_bit_ofFn`: reconstruction is the sum of the digits' binary place values.
 * `Nat.size_div_two_add_one`: halving a positive number removes one binary digit.
 -/
@@ -57,6 +59,29 @@ theorem Nat.foldr_bit_lt (l : List Bool) : l.foldr Nat.bit 0 < 2 ^ l.length := b
     simp only [List.foldr_cons, Nat.bit_val, List.length_cons, Nat.pow_succ]
     cases b <;> simp only [Bool.toNat_true, Bool.toNat_false] <;> lia
 
+/-- Folding `Nat.bit` with base `1` over any word gives a positive number. -/
+theorem Nat.foldr_bit_one_ne_zero (w : List Bool) : w.foldr Nat.bit 1 ≠ 0 := by
+  induction w with
+  | nil => simp
+  | cons b w ih => exact Nat.bit_ne_zero b ih
+
+/-- Folding `Nat.bit` with base `1` appends `true` to the binary representation. -/
+theorem Nat.bits_foldr_bit_one (w : List Bool) : (w.foldr Nat.bit 1).bits = w ++ [true] := by
+  induction w with
+  | nil => simp
+  | cons b w ih =>
+    rw [List.foldr_cons,
+      Nat.bits_append_bit _ _ fun h => absurd h (Nat.foldr_bit_one_ne_zero w), ih,
+      List.cons_append]
+
+/-- Folding `Nat.bit` with base `1` produces a number strictly below `2 ^ (|w| + 1)`. -/
+theorem Nat.foldr_bit_one_lt (w : List Bool) : w.foldr Nat.bit 1 < 2 ^ (w.length + 1) := by
+  induction w with
+  | nil => simp
+  | cons b w ih =>
+    rw [List.foldr_cons, Nat.bit_val, List.length_cons, pow_succ]
+    cases b <;> simp only [Bool.toNat_false, Bool.toNat_true] <;> omega
+
 /-- Reading enough low-order digits recovers the natural, including its leading zero digits. -/
 theorem Nat.foldr_bit_testBit {n K : ℕ} (h : n.size ≤ K) :
     ((List.range K).map n.testBit).foldr Nat.bit 0 = n := by