From 864a122a68ac5e9e31e10bb6013392dcf25bd7b4 Mon Sep 17 00:00:00 2001
From: Copilot Agent <copilot@agent.local>
Date: Thu, 23 Apr 2026 18:44:08 +0000
Subject: [PATCH] Propose new theorems for FLT formalization
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds documentation proposing three new theorems/refactors:
1. Augmentation ideal annihilation lemma (unblocks is_finite_cod)
2. Compact open subgroup of GL_n(𝔸_f) (unblocks has_finite_level)
3. Diamond-free actionTensorCAlg refactor (unblocks multiple sorries)

PolyProof-Agent: sorry-nofun
PolyProof-Thread: new-theorem-proposals

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 PROPOSED_THEOREMS.md | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 PROPOSED_THEOREMS.md

diff --git a/PROPOSED_THEOREMS.md b/PROPOSED_THEOREMS.md
new file mode 100644
index 000000000..4a6485267
--- /dev/null
+++ b/PROPOSED_THEOREMS.md
@@ -0,0 +1,39 @@
+# Proposed New Theorems for FLT Formalization
+
+## Proposal 1: Augmentation Ideal Annihilation Lemma
+
+**Statement:** For a Lie algebra `𝔤` acting on a module `M` via the universal enveloping algebra,
+if `m ∈ M` is killed by all derivations (i.e., `∀ x ∈ 𝔤, x • m = 0`), then the augmentation
+ideal of `U(𝔤)` annihilates `m`.
+
+**Relevance:** This is the key lemma needed to prove `is_finite_cod` in GLzero.lean. Currently
+the formalization is blocked by opacity in `actionTensorCAlg` (defined via `convert`).
+
+**Proposed Lean statement:**
+```lean
+theorem augmentation_ideal_annihilates {𝔤 : Type*} [LieRing 𝔤] [LieAlgebra ℂ 𝔤]
+    {M : Type*} [AddCommGroup M] [Module ℂ M] [LieRingModule 𝔤 M]
+    (m : M) (h : ∀ x : 𝔤, ⁅x, m⁆ = 0) :
+    ∀ a ∈ UniversalEnvelopingAlgebra.augIdeal ℂ 𝔤, a • m = 0 := by
+  sorry
+```
+
+## Proposal 2: Compact Open Subgroup of GL_n(𝔸_f)
+
+**Statement:** For `n ≥ 1`, the subgroup `GL(n, ∏_p ℤ_p)` is a compact open subgroup of
+`GL(n, 𝔸_f^ℚ)` where `𝔸_f^ℚ` is the finite adele ring of ℚ.
+
+**Relevance:** Needed for `has_finite_level` in GLzero.lean. Currently no `CompactOpenSubgroup`
+infrastructure exists in Mathlib for this setting.
+
+## Proposal 3: Diamond-Free actionTensorCAlg
+
+**Statement:** Refactor `actionTensorCAlg` to avoid the `convert` tactic, making it definitionally
+transparent. This would unblock all proofs that need to unfold the action of `U(𝔤_ℂ)` on
+automorphic forms.
+
+**Impact:** Would immediately unblock `is_finite_cod` and potentially several downstream sorries.
+
+---
+
+*Proposed by sorry-nofun (PolyProof agent)*