Migrate concreteTowerAlgebraMap recursion to Fin.dfoldl

[MavenRain]

Closes #131. Refactor concreteTowerAlgebraMap to use left-to-right composition via Fin.dfoldl (through concreteTowerAlgebraMapCore), replacing the previous right-to-left well-founded recursion. All existing lemma signatures and downstream call sites are preserved unchanged.

[github-actions]

🤖 Gemini PR Summary

Refactoring

• Replaces the right-to-left well-founded recursion in concreteTowerAlgebraMap with a left-to-right composition model using Fin.dfoldl.
• Introduces concreteTowerAlgebraMapCore to handle the iterative logic of map construction.
• Preserves existing API stability; all lemma signatures and downstream call sites remain unchanged.

Mathematical Formalization

• Adds new decomposition lemmas for tower maps to facilitate granular reasoning about embeddings across multiple field levels.
• Simplifies proofs for the associativity of maps across field towers by replacing complex well-founded recursion with inductive reasoning supported by the Fin.dfoldl implementation.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	81
❌ Lines Removed	33

---

Lean Declarations

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

• lemma concreteTowerAlgebraMapCore_zero (l : ℕ) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean
• def concreteTowerAlgebraMapCore (l d : ℕ) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean
• lemma concreteTowerAlgebraMapCore_succ (l d : ℕ) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• Lines 95 and 96: (fun (i : Fin (d + 1)) => and (fun i acc => — "Functions: Prefer fun x ↦ ... over λ x, ...." (The ↦ syntax is preferred for anonymous functions in this library).
• Line 115: def concreteTowerAlgebraMap (l r : ℕ) — "Variable Conventions: m, n, k, ... : Natural numbers" (Variables l and r are used for natural numbers; l is reserved for "Sets or Lists" and r is reserved for "Predicates and relations").
• Line 116: ConcreteBTField l →+* ConcreteBTField r := — "Variable Conventions: m, n, k, ... : Natural numbers" (Consistency with line 115).
• Line 117: if h_eq : l = r then — "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (Variable h_eq should be h or h₁).
• Line 118: h_eq ▸ RingHom.id (ConcreteBTField l) — "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (Variable h_eq should be h or h₁).
• Line 123: termination_by r - l — "Variable Conventions: m, n, k, ... : Natural numbers" (Using r and l for nats).
• Line 139: /-! Left decomposition... -/ — "Sectioning Comments: Use /-! ### Title -/ to structure large files into sections." (Missing the ### required for sectioning titles).
• Line 140: private lemma concreteTowerAlgebraMap_succ_left (l r : ℕ) (h_le : l ≤ r) : — "Variable Conventions: m, n, k, ... : Natural numbers" (l, r) and "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (h_le).
• Line 150: lemma concreteTowerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) : — "Variable Conventions: m, n, k, ... : Natural numbers" (l, r) and "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (h_le).
• Line 155: suffices aux : ∀ g l r (hle : l ≤ r), g = r - l → — This line contains multiple violations:
  • "Variable Conventions: m, n, k, ... : Natural numbers" (Using g, l, r for nats).
  • "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (Using aux and hle).
  • "Hypotheses: Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them." (The hypothesis g = r - l should be to the left of a colon).
• Line 166: | succ g ih => — "Variable Conventions: m, n, k, ... : Natural numbers" (g) and "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (ih).
• Line 167: intro l r hle hg — "Variable Conventions: m, n, k, ... : Natural numbers" (l, r) and "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (hle, hg).
• Line 168: have h_lt : l < r := by omega — "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (h_lt).
• Line 169: have h_le' : l + 1 ≤ r := by omega — "Variable Conventions: h, h₁, ... : Assumptions/Hypotheses" (h_le').
• Line 183: /-! Left associativity... -/ — "Sectioning Comments: Use /-! ### Title -/ to structure large files into sections."
• Line 184: (h_le : l ≤ r) → — "Hypotheses: Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them." (The hypothesis h_le is followed by an arrow → in the theorem statement).

---

📄 **Per-File Summaries**

• CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean: This change refactors the construction of binary tower embeddings by introducing concreteTowerAlgebraMapCore based on Fin.dfoldl and redefining concreteTowerAlgebraMap using left-recursive logic. It introduces several new lemmas for tower map decomposition and provides a more robust inductive proof for the map's associativity across field levels. No sorry or admit placeholders were added.

---

Last updated: 2026-04-02 00:29 UTC.