Prove uniqueness of getBit binary representation

CompPoly/Data/Nat/Bitwise.lean

@@ -923,7 +923,6 @@ lemma getBit_eq_pred_getBit_of_div_two {n k : ℕ} (h_k: k > 0) :
   conv_lhs => rw [←Nat.sub_add_cancel (n:=k) (m:=1) (h:=by omega)]
   exact Eq.symm (getBit_of_shiftRight (k - 1))
 
--- TODO: uniqueness of this representation?
 theorem getBit_repr {ℓ : Nat} :
     ∀ j, j < 2^ℓ → j = ∑ k ∈ Finset.Icc 0 (ℓ-1), (getBit k j) * 2^k := by
   induction ℓ with
@@ -1075,6 +1074,78 @@ theorem getBit_repr_univ {ℓ : Nat} :
       have h_a_lt_ℓ: a < ℓ := by exact a.isLt
       omega
 
+/-- Two natural numbers with identical bits at every position are equal. -/
+theorem getBit_injective (a b : ℕ) (h : ∀ k, getBit k a = getBit k b) : a = b := by
+  apply Nat.eq_of_testBit_eq
+  intro n
+  unfold Nat.testBit
+  unfold getBit at h
+  simp only [Nat.one_and_eq_mod_two, Nat.and_one_is_mod] at h ⊢
+  rw [h n]
+
+/-- The binary representation of a number via `getBit` is unique: any sequence of
+    0/1 coefficients that sums to `j` must agree with `getBit` at each position. -/
+theorem getBit_repr_unique {ℓ : ℕ} {j : ℕ} (h_j : j < 2 ^ ℓ)
+    (c : ℕ → ℕ) (h_bin : ∀ k, k < ℓ → c k = 0 ∨ c k = 1)
+    (h_sum : j = ∑ k ∈ Finset.Icc 0 (ℓ - 1), c k * 2 ^ k) :
+    ∀ k, k < ℓ → c k = getBit k j := by
+  -- Proof by induction on ℓ, extracting the lowest bit at each step.
+  induction ℓ generalizing j c with
+  | zero => intro k hk; omega
+  | succ ℓ ih =>
+    intro k hk
+    rw [show ℓ + 1 - 1 = ℓ from by omega] at h_sum
+    by_cases hℓ0 : ℓ = 0
+    · subst hℓ0
+      simp only [Finset.Icc_self, Finset.sum_singleton, pow_zero, mul_one] at h_sum
+      interval_cases k
+      rw [h_sum]
+      simp only [getBit, Nat.shiftRight_zero, Nat.and_one_is_mod]
+      rcases h_bin 0 (by omega) with h₁ | h₂ <;> [rw [h₁]; rw [h₂]]
+    · -- Split: j = c 0 + (even tail). Extract c 0 via mod 2, then recurse on j/2.
+      have h_split := sum_Icc_split (fun k ↦ c k * 2 ^ k) 0 0 ℓ (by omega) (by omega)
+      rw [h_split, Finset.Icc_self, Finset.sum_singleton, pow_zero, mul_one] at h_sum
+      -- The tail sum is even
+      set S := ∑ n ∈ Finset.Icc 1 ℓ, c n * 2 ^ n with hS_def
+      have h_even : 2 ∣ S :=
+        Finset.dvd_sum (fun n hn ↦
+          dvd_mul_of_dvd_right (dvd_pow_self 2 (by simp [Finset.mem_Icc] at hn; omega)) _)
+      -- c 0 = getBit 0 j (parity argument)
+      have h_c0 : c 0 = getBit 0 j := by
+        simp only [getBit, Nat.shiftRight_zero, Nat.and_one_is_mod]
+        obtain ⟨m, hm⟩ := h_even
+        rw [h_sum, hm]
+        rcases h_bin 0 (by omega) with h₁ | h₂ <;> [rw [h₁]; rw [h₂]] <;> omega
+      by_cases hk0 : k = 0
+      · exact hk0 ▸ h_c0
+      · -- k > 0: recurse on j/2 with shifted coefficients
+        -- We need: j / 2 = ∑ i ∈ Icc 0 (ℓ-1), c(i+1) * 2^i
+        -- Reindex the tail: S = 2 * ∑ c(i+1) * 2^i
+        have h_reindex : S = 2 * ∑ n ∈ Finset.Icc 0 (ℓ - 1), c (n + 1) * 2 ^ n := by
+          rw [hS_def, Finset.mul_sum]
+          apply Finset.sum_nbij' (fun n ↦ n - 1) (fun n ↦ n + 1)
+          · intro n hn; simp only [Finset.mem_Icc] at hn ⊢; omega
+          · intro n hn; simp only [Finset.mem_Icc] at hn ⊢; omega
+          · intro n hn; simp only [Finset.mem_Icc] at hn; omega
+          · intro n hn; simp only [Finset.mem_Icc] at hn; omega
+          · intro n hn
+            have hn' := (Finset.mem_Icc.mp hn).1
+            rw [show n - 1 + 1 = n from by omega]
+            rw [show 2 ^ n = 2 ^ (n - 1) * 2 from by
+              rw [← pow_succ, show n - 1 + 1 = n from by omega]]
+            ring
+        have h_div : j / 2 = ∑ n ∈ Finset.Icc 0 (ℓ - 1), c (n + 1) * 2 ^ n := by
+          rw [h_sum, h_reindex]
+          rcases h_bin 0 (by omega) with h₁ | h₂ <;> [rw [h₁]; rw [h₂]] <;> omega
+        -- Apply IH to j / 2 with shifted coefficients
+        have h_res := ih (by omega : j / 2 < 2 ^ ℓ) (fun n ↦ c (n + 1))
+            (fun n hn ↦ h_bin (n + 1) (by omega)) h_div (k - 1) (by omega)
+        -- h_res : c ((k-1) + 1) = getBit (k-1) (j/2)
+        -- Rewrite (k-1)+1 to k in h_res
+        have hk_sub : k - 1 + 1 = k := by omega
+        simp only [hk_sub] at h_res
+        rw [h_res, getBit_eq_pred_getBit_of_div_two (by omega : k > 0)]
+
 lemma getLowBits_succ {n: ℕ} (numLowBits: ℕ) :
     getLowBits (numLowBits + 1) n = getLowBits numLowBits n
     + (getBit numLowBits n) <<< numLowBits := by

CompPoly/Fields/Binary/Tower/Abstract/Split.lean

@@ -80,9 +80,9 @@ The power basis for `BTField (k+1)` over `BTField k` is {1, Z (k+1)}
 def powerBasisSucc (k : ℕ) :
     PowerBasis (BTField k) (BTField (k+1)) := by
   let pb : PowerBasis (BTField k) (AdjoinRoot (poly k)) :=
-    AdjoinRoot.powerBasis (hf:=by exact poly_ne_zero k)
-  -- ⊢ algebra_adjacent_tower k = AdjoinRoot.instAlgebra (poly k) => TODO : make a lemma for this
+    AdjoinRoot.powerBasis (hf := by exact poly_ne_zero k)
   -- NOTE : pb.gen is definitionally equal to AdjoinRoot.root (poly k)
+  -- See `algebra_adjacent_tower_eq_AdjoinRoot_algebra` for the algebra instance equality.
   have h_eq : AdjoinRoot (poly k) = BTField (k+1) := BTField_succ_eq_adjoinRoot k
   -- ⊢ PowerBasis (BTField k) (BTField (k + 1))
   apply pb.map (e:=BTField_succ_alg_equiv_adjoinRoot k)

scripts/style-exceptions.txt

@@ -11,5 +11,6 @@ CompPoly/Fields/Binary/Tower/Concrete/Core.lean : line 1 : ERR_NUM_LIN : 1700 fi
 CompPoly/Fields/Binary/AdditiveNTT/AdditiveNTT.lean : line 1 : ERR_NUM_LIN : 3000 file contains 2826 lines, try to split it up : ERR_NUM_LIN
 CompPoly/Fields/Binary/AdditiveNTT/AdditiveNTT.lean : line 8 : ERR_TAC : Files in CompPoly should not import the whole Mathlib.Tactic folder : ERR_TAC
 CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean : line 1 : ERR_NUM_LIN : 1800 file contains 1636 lines, try to split it up : ERR_NUM_LIN
+CompPoly/Data/Nat/Bitwise.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1537 lines, try to split it up : ERR_NUM_LIN
 CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Correctness.lean : line 1 : ERR_NUM_LIN : 2600 file contains 2421 lines, try to split it up : ERR_NUM_LIN
 CompPoly/Data/ExtTreeMap/DTreeMap.lean : line 1 : ERR_LIN : Line has more than 100 characters : ERR_LIN