refactor(binary-tower): rewrite towerAlgebraMap using Fin.dfoldl

[erdkocak]

I moved the main logic to towerAlgebraMapCore, towerAlgebraMap is now just a wrapper around it. Existing callers of towerAlgebraMap require no API changes. I kept the current if else branching logic in towerAlgebraMap because it helps with proofs. But if preferred I can also do something like:

def towerAlgebraMap (l r : ℕ) (h_le : l ≤ r) : BTField l →+* BTField r := cast (BTField.RingHom_eq_of_dest_eq (k:=l) (m:=l + (r - l)) (n:=r) (Nat.add_sub_of_le h_le)) (towerAlgebraMapCore l (r - l))

Also, I changed the name of the hypothesis in the towerAlgebraMap branch to h_eq because it made more sense.

Fixes #130

Co-authored-by: GPT-5.3-Codex

[github-actions]

🤖 Gemini PR Summary

Refactors the binary tower's towerAlgebraMap by migrating from manual recursion to a fold-based implementation using Fin.dfoldl.

Key Changes

• Logic Decoupling: Extracted the main transformation logic into towerAlgebraMapCore, utilizing Fin.dfoldl to iteratively apply lifting operations.
• Wrapper Pattern: Updated towerAlgebraMap to serve as a thin wrapper around the core function, maintaining a stable public API and requiring no changes to existing callers.
• Proof Stability: Retained the original if-else branching logic within the wrapper to ensure compatibility with existing proofs that rely on specific case analysis.
• Naming Clarity: Renamed the hypothesis in the branching logic to h_eq to better reflect its role in the proof state.

Technical Impact

• Fixes: Migrate towerAlgebraMap recursion to Fin.dfoldl #130.
• Implementation: Transitions to idiomatic Lean functional patterns for index-based transformations, improving maintainability of the binary tower's field arithmetic.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	82
❌ Lines Removed	20

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

Based on the style guide provided, here are the violations found in the diff:

• Documentation Standards

  • Line 646: The definition towerAlgebraMap is missing a docstring. "Every definition and major theorem should have a docstring."
  • Line 655: The theorem towerAlgebraMap_id is missing a docstring. "Every definition and major theorem should have a docstring."
  • Line 661: The theorem towerAlgebraMap_succ_1 is missing a docstring. "Every definition and major theorem should have a docstring."
  • Line 671: The theorem towerAlgebraMap_succ is missing a docstring. "Every definition and major theorem should have a docstring."
  • Line 700: The theorem towerAlgebraMap_succ_last is missing a docstring. "Every definition and major theorem should have a docstring."

• Syntax and Formatting (Spaces around Operators)

  • Line 614: (k:=l) violates "Put spaces on both sides of :, :=, and infix operators."
  • Line 615: (m:=l + ...) and (n:=l + d) violate "Put spaces on both sides of :, :=, and infix operators."
  • Line 652: (k:=l), (m:=l + (r - l)), and (n:=r) violate "Put spaces on both sides of :, :=, and infix operators."
  • Line 655: (h_le:=by omega) violates "Put spaces on both sides of :, :=, and infix operators."
  • Line 662: (l:=k), (r:=k+1), and (h_le:=by omega) violate "Put spaces on both sides of :, :=, and infix operators." Additionally, k+1 violates "Put spaces on both sides of... infix operators."
  • Line 672: (l:=l), (r:=r+1), and (h_le:=by omega) violate "Put spaces on both sides of :, :=, and infix operators." Additionally, r+1 violates spacing for infix operators.
  • Line 674: (l:=r), (r:=r+1), and (h_le:=by omega) violate "Put spaces on both sides of :, :=, and infix operators." Additionally, r+1 violates spacing for infix operators.
  • Line 675: (l:=l), (r:=r), and (h_le:=by omega) violate "Put spaces on both sides of :, :=, and infix operators."

• Syntax and Formatting (Function Arrow Preference)

  • Line 606: fun i => violates "Prefer fun x ↦ ... over λ x, ...." (The symbol ↦ is preferred over =>).
  • Line 631: fun i : Fin (d + 2) => violates "Prefer fun x ↦ ... over λ x, ...."
  • Line 632: fun i f => violates "Prefer fun x ↦ ... over λ x, ...."
  • Line 635: fun i : Fin (d + 1) => violates "Prefer fun x ↦ ... over λ x, ...."
  • Line 636: fun i f => violates "Prefer fun x ↦ ... over λ x, ...."
  • Line 644: fun f => violates "Prefer fun x ↦ ... over λ x, ...."

• Variable Conventions

  • Lines 605, 606, 618, 624, 646, 671, 689, 700: Use of l, d, and r for natural numbers violates the convention "m, n, k, ... : Natural numbers".
  • Lines 606, 629: Use of α for a function (Fin (d + 1) → Type) violates the convention "α, β, γ, ... : Generic types".
  • Lines 610, 632, 636, 644: Use of f for terms/functions violates the convention "x, y, z, ... : Elements of a generic type".
  • Lines 613, 615, 646, 647, 653, 655, 662, 666, 671, 680, 683, 689, 690, 694, 700: Use of descriptive hypothesis names like h_last, h_le, h_eq, h_sub, h_lr, h_diff, h_idx, and hd violates the convention "h, h₁, ... : Assumptions/Hypotheses".

---

📄 **Per-File Summaries**

• CompPoly/Fields/Binary/Tower/Basic.lean: This Lean file refactors the towerAlgebraMap definition to use Fin.dfoldl instead of structural recursion, introducing the towerAlgebraMapCore helper definition and updating associated lemmas and proofs.

---

Last updated: 2026-03-05 10:35 UTC.

[erdkocak]

Linter seems to be failing because of the line count. I guess we can add an exception to linter, but I did not wanted to do that without discussing first.