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.