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

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Prove uniqueness of getBit binary representation

Mathematical Formalization

• getBit_injective: Proves that natural numbers are uniquely identified by their sequence of bits.
• getBit_repr_unique: Establishes that any binary coefficient sequence summing to a natural number matches its bitwise representation.

Refactoring and Proof Completion

• Resolves a TODO regarding algebra instance equality in binary tower splitting logic.
• Refines the proof of powerBasisSucc.
• No sorry or admit placeholders are present in this pull request.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	75
❌ 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.

---

📋 **Additional Analysis**

Style and Naming Guidelines

• Variable Naming Conventions:
  • In getBit_injective, the natural numbers are named a and b. The project convention (Mathlib-style) prefers m, n, or k for natural numbers.
  • In getBit_injective and getBit_repr_unique, the variable n is used as an index (for bit positions or summation). The convention specifies i, j, k for indexing roles.
  • The variable ℓ is used for a natural number (length/bound). While common in this module, it is not explicitly listed in the allowed algebraic carrier or natural number conventions (m, n, k).
• Theorem Naming:
  • getBit_injective: Adheres to the structural lemma convention for injectivity results.
  • getBit_repr_unique: Adheres to the convention for uniqueness results.

Documentation Standards

• LaTeX in Docstrings:
  • In the docstring for getBit_repr_unique, the variable j is enclosed in backticks (`j`). According to the documentation standards, mathematical variables should use LaTeX syntax (e.g., $j$).

Module Layout and Maintenance

• File Length:
  • The PR adds CompPoly/Data/Nat/Bitwise.lean to scripts/style-exceptions.txt for ERR_NUM_LIN. The file currently contains 1537 lines. The style guide (via the linter exception) suggests splitting large files (typically those exceeding 1500 lines) into smaller modules, such as moving theorems to a Lemmas leaf module.

Syntax and Formatting

• Operators and Spacing:
  • The change in CompPoly/Fields/Binary/Tower/Abstract/Split.lean correctly fixes spacing around the := operator in the hf hypothesis.
  • The new theorems in Bitwise.lean correctly place spaces around :, :=, and infix operators (e.g., ℓ - 1).
• Proof Construction:
  • Tactice blocks correctly follow the by placement at the end of the preceding line.
  • Function syntax correctly uses fun x ↦ ... (e.g., in h_reindex).
  • The proof of getBit_repr_unique uses rcases ... <;> [rw ...; rw ...]. This is acceptable as a short, single-line tactic sequence.

---

📄 **Per-File Summaries**

• CompPoly/Data/Nat/Bitwise.lean: This change introduces the theorems getBit_injective and getBit_repr_unique to establish that natural numbers are uniquely determined by their bitwise representations. These proofs demonstrate that numbers with identical bits are equal and that any valid binary sum expansion of a number must coincide with its getBit values, with no sorry or admit placeholders used.
• CompPoly/Fields/Binary/Tower/Abstract/Split.lean: This change refines the proof of powerBasisSucc by replacing a TODO comment with a reference to a lemma regarding algebra instance equality and applying minor formatting adjustments. No new definitions or theorems are introduced, and no sorry placeholders are added.

---

Last updated: 2026-06-23 23:35 UTC.

addressed