Prove uniqueness of getBit binary representation

[MavenRain]

Add getBit_injective (pointwise bit equality implies number equality) and getBit_repr_unique (any binary coefficient sequence summing to j must agree with getBit at each position). Remove resolved TODO.

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Adds getBit_injective: Establishes that natural numbers are uniquely determined by the pointwise equality of their bits.
• Adds getBit_repr_unique: Formally proves that any sequence of coefficients $c_i \in {0, 1}$ such that $\sum c_i 2^i = j$ must satisfy $c_i = \text{getBit } j \ i$ for all $i$.
• These results bridge the gap between functional bit manipulation via getBit and the algebraic sum-of-powers representation of natural numbers.

Structural Refinement and Documentation

• Resolves a "TODO" in the binary tower implementation within Abstract/Split.lean.
• Refines the powerBasisSucc definition by incorporating an explicit reference to algebra_adjacent_tower_eq_AdjoinRoot_algebra, formalizing the justification for adjacent field extensions in the tower.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	74
❌ Lines Removed	2

---

Lean Declarations

✏️ **Added:** 2 declaration(s)

• theorem getBit_repr_unique {ℓ : ℕ} {j : ℕ} (h_j : j < 2 ^ ℓ) in CompPoly/Data/Nat/Bitwise.lean
• theorem getBit_injective (a b : ℕ) (h : ∀ k, getBit k a = getBit k b) : a = b in CompPoly/Data/Nat/Bitwise.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

There are more than 20 violations in the provided diff. They are grouped by rule below:

• Empty Lines: "Avoid empty lines inside definitions or proofs." (9 violations)

  • Line 1123: Empty line inside the proof of getBit_repr_unique.
  • Line 1139: Empty line inside the proof of getBit_repr_unique.
  • Line 1156: Empty line inside the proof of getBit_repr_unique.
  • (Also lines 1128, 1134, 1142, 1153, 1159, and 1161).

• Variable Conventions: "h, h₁, ... : Assumptions/Hypotheses", "m, n, k, ... : Natural numbers" (19 violations)

  • Line 1129: Use of S for a natural number (sum) instead of m, n, or k.
  • Lines 1113, 1114, 1115: Use of descriptive hypothesis names h_j, h_bin, and h_sum instead of the h, h₁ pattern.
  • Lines 1136, 1146, 1149: Use of hm, hn, and hn' for hypotheses instead of the h, h₁ pattern.
  • (Also descriptive hypothesis names on lines 1122, 1125, 1129, 1130, 1133, 1138, 1143, 1154, 1157, and 1162).

• Naming Conventions: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)","Theorems and Proofs: snake_case" (8 violations)

  • Lines 80, 81, 83, 85: Use of BTField (Binary Tower Field); as an acronym, it should be formatted as BtField.
  • Line 86: Use of BTField in the declaration name BTField_succ_alg_equiv_adjoinRoot.
  • Lines 1122, 1129, 1138: Use of hℓ0, hS_def, and hk0 for hypotheses; these are not in snake_case (e.g., h_ℓ0).

• Syntax and Formatting: "Use 2 spaces for indentation.", "Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting." (5 violations)

  • Lines 1114-1116: Use of 4-space indentation for theorem arguments and conclusion.
  • Line 1131: Use of parentheses (...) for the by block where a pipe <| could reduce nesting.
  • Line 1145: Use of parentheses for the fun arguments.

---

📄 **Per-File Summaries**

• CompPoly/Fields/Binary/Tower/Abstract/Split.lean: This update replaces a "TODO" comment with a reference to the lemma algebra_adjacent_tower_eq_AdjoinRoot_algebra within the powerBasisSucc definition. The changes are primarily documentation-focused and include minor formatting adjustments without introducing new theorems, definitions, or logic changes.
• CompPoly/Data/Nat/Bitwise.lean: This PR introduces theorems establishing the injectivity and uniqueness of bitwise representations for natural numbers. Specifically, it adds getBit_injective to prove that numbers with identical bits are equal and getBit_repr_unique to show that the coefficients in a sum of powers of two are uniquely determined by the getBit function.

---

Last updated: 2026-04-04 00:15 UTC.

[dhsorens]

thank you for this PR! looks good to me. if you can just fix the linting issue and update the branch we can merge this. I'm not too worried about the length of Bitwise.lean so feel free to add it to style-exceptions.txt