feat: add ramification and inertia computations for primes in Z[sqrt(-5)]

.beads/issues.jsonl

@@ -1 +1 @@
-{"id":"ANT-miq","title":"Finish remaining ANT/Ideals proofs","description":"Prove remaining theorems in ANT/Ideals.lean: factorization_of_three, factorization_of_one_plus_sqrtd, factorization_of_one_minus_sqrtd, and prime-ideal statements currently marked sorry.","status":"open","priority":2,"issue_type":"task","owner":"git@frankie.wang","created_at":"2026-02-11T13:28:16.554103Z","created_by":"Frankie Wang","updated_at":"2026-02-11T13:28:16.554103Z"}
+{"id":"ANT-miq","title":"Finish remaining ANT/Ideals proofs","description":"Prove remaining theorems in ANT/Ideals.lean: factorization_of_three, factorization_of_one_plus_sqrtd, factorization_of_one_minus_sqrtd, and prime-ideal statements currently marked sorry.","status":"closed","priority":2,"issue_type":"task","owner":"git@frankie.wang","created_at":"2026-02-11T13:28:16.554103Z","created_by":"Frankie Wang","updated_at":"2026-02-24T23:39:35.68363Z","closed_at":"2026-02-24T23:39:35.68363Z","close_reason":"All theorems are proven: factorization_of_three, factorization_of_one_plus_sqrtd, factorization_of_one_minus_sqrtd, and all prime-ideal statements (isPrime_span_two_one_plus_sqrtd, isPrime_span_three_one_plus_sqrtd, isPrime_span_three_one_minus_sqrtd) are complete with no sorry placeholders."}

ANT.lean

@@ -1,2 +1,3 @@
 import ANT.Basic
 import ANT.Ideals
+import ANT.RamificationInertia

ANT/RamificationInertia.lean

@@ -0,0 +1,105 @@
+import ANT.Ideals
+import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
+
+open Ideal Zsqrtd
+
+-- Note: R is defined in ANT.Ideals
+
+--------------------------------------------------------------------
+-- RAMIFICATION AND INERTIA COMPUTATIONS
+--------------------------------------------------------------------
+
+-- Results for Q(sqrt(-5)) / Q:
+--
+-- Prime p = 2:
+--   Factorization: (2) = P^2 with P = <2, 1+sqrt(-5)>
+--   Ramification index: e = 2
+--   Inertia degree: f = 1 (since R/P ~ Z/2Z)
+--   Check: e * f = 2 = [Q(sqrt(-5)):Q] OK
+--
+-- Prime p = 3:
+--   Factorization: (3) = P1 * P2 with P1 = <3, 1+sqrt(-5)>, P2 = <3, 1-sqrt(-5)>
+--   For each prime: e = 1, f = 1
+--   Check: e1*f1 + e2*f2 = 1 + 1 = 2 = [Q(sqrt(-5)):Q] OK
+
+-- Prime ideals in Z[sqrt(-5)]
+/-- The prime ideal ⟨2, 1+√-5⟩ in ℤ[√-5]. -/
+def P2 : Ideal R := span {2, 1 + sqrtd}
+
+/-- The prime ideal ⟨3, 1+√-5⟩ in ℤ[√-5]. -/
+def P3plus : Ideal R := span {3, 1 + sqrtd}
+
+/-- The prime ideal ⟨3, 1-√-5⟩ in ℤ[√-5]. -/
+def P3minus : Ideal R := span {3, 1 - sqrtd}
+
+/-- P2 is a prime ideal. -/
+instance : P2.IsPrime := isPrime_span_two_one_plus_sqrtd
+
+/-- P3plus is a prime ideal. -/
+instance : P3plus.IsPrime := isPrime_span_three_one_plus_sqrtd
+
+/-- P3minus is a prime ideal. -/
+instance : P3minus.IsPrime := isPrime_span_three_one_minus_sqrtd
+
+/-- The ideal (2) in ℤ[√-5] equals P2^2. -/
+theorem ideal_2_factorization : span {(2 : R)} = P2 ^ 2 :=
+  factorization_of_two
+
+/-- The ideal (3) in ℤ[√-5] equals P3plus * P3minus. -/
+theorem ideal_3_factorization : span {(3 : R)} = P3plus * P3minus :=
+  factorization_of_three
+
+
+
+--------------------------------------------------------------------
+-- Computed using mathlib definitions
+--------------------------------------------------------------------
+
+/-- The ramification index of 2 using Ideal.ramificationIdx. -/
+theorem ramificationIdx_2 :
+    Ideal.ramificationIdx (algebraMap ℤ R) (Ideal.span {(2 : ℤ)}) P2 = 2 := by
+  apply Ideal.ramificationIdx_spec
+  · -- Show map(ℤ→R)(span{2}) ≤ P2^2
+    simp only [Ideal.map_span, Set.image_singleton, map_ofNat]
+    exact le_of_eq ideal_2_factorization
+  · -- Show ¬(map(ℤ→R)(span{2}) ≤ P2^3)
+    simp only [Ideal.map_span, Set.image_singleton, map_ofNat,
+               Ideal.span_singleton_le_iff_mem]
+    -- Need: (2:R) ∉ P2^3
+    -- Key: P2^3 = P2^2 * P2 = span{2} * P2, so 2 ∈ P2^3 → 1 ∈ P2 → P2 = ⊤
+    rw [pow_succ, ← ideal_2_factorization, Ideal.mem_span_singleton_mul]
+    rintro ⟨z, hz, heq⟩
+    -- From 2 * z = 2, extract coordinates to get z = 1
+    have hone : z = 1 := by
+      have hre := congr_arg Zsqrtd.re heq
+      have him := congr_arg Zsqrtd.im heq
+      simp only [Zsqrtd.re_mul, Zsqrtd.im_mul] at hre him
+      norm_num at hre him
+      exact Zsqrtd.ext hre him
+    -- But 1 ∈ P2 contradicts P2 ≠ ⊤
+    rw [hone] at hz
+    have : P2 ≠ ⊤ := Ideal.IsPrime.ne_top (inferInstance : P2.IsPrime)
+    exact this ((Ideal.eq_top_iff_one (I := P2)).mpr hz)
+
+/-- The inertia degree of P2 using Ideal.inertiaDeg. -/
+theorem inertiaDeg_2 : (Ideal.span {(2 : ℤ)}).inertiaDeg P2 = 1 := by
+  sorry
+
+/-- The ramification index of P3plus using Ideal.ramificationIdx. -/
+theorem ramificationIdx_3_P3plus :
+    Ideal.ramificationIdx (algebraMap ℤ R) (Ideal.span {(3 : ℤ)}) P3plus = 1 := by
+  sorry
+
+/-- The inertia degree of P3plus using Ideal.inertiaDeg. -/
+theorem inertiaDeg_3_P3plus : (Ideal.span {(3 : ℤ)}).inertiaDeg P3plus = 1 := by
+  sorry
+
+/-- The ramification index of P3minus using Ideal.ramificationIdx. -/
+theorem ramificationIdx_3_P3minus :
+    Ideal.ramificationIdx (algebraMap ℤ R) (Ideal.span {(3 : ℤ)}) P3minus = 1 := by
+  sorry
+
+/-- The inertia degree of P3minus using Ideal.inertiaDeg. -/
+theorem inertiaDeg_3_P3minus : (Ideal.span {(3 : ℤ)}).inertiaDeg P3minus = 1 := by
+  sorry

ANT/Tactic.lean.disable

@@ -0,0 +1,123 @@
+import Mathlib
+/-! Fail  and disable-/
+open Ideal Zsqrtd
+
+set_option linter.style.whitespace false
+
+namespace ANT.Tactic
+
+private abbrev R := Zsqrtd (-5)
+
+/-- Close an equality goal by `ring`, or by `ext <;> norm_num` when `ring` fails
+    (e.g. when `sqrtd` is involved). -/
+scoped macro "try_eq " h:term : tactic =>
+  `(tactic| (convert ($h) using 1; first | ring | (ext <;> norm_num [Zsqrtd.sqrtd])))
+
+/-- Close a `Zsqrtd` equality by trying `ring` first, then `ext <;> norm_num`. -/
+scoped macro "zsqrtd_eq" : tactic =>
+  `(tactic| first | ring | (ext <;> norm_num [Zsqrtd.sqrtd]))
+
+/-- Given that generators `g₁, g₂, g₃, g₄` all belong to ideal `J`,
+    prove the current goal is in `J` by showing it equals a linear combination
+    `c₁ * g₁ + c₂ * g₂ + c₃ * g₃ + c₄ * g₄` using `Ideal.add_mem` and `Ideal.mul_mem_left`.
+
+    This version avoids the existential quantifier pattern (which caused expensive
+    metavariable unification) and instead uses `convert` + `zsqrtd_eq` to close
+    the remaining equality goal directly. -/
+
+scoped macro "show_mem_by_lincomb " J:ident
+    hg1:ident hg2:ident hg3:ident hg4:ident : tactic =>
+  `(tactic| (
+    refine show _ ∈ $J from ?_
+    -- Express the element as c₁ * g₁ + c₂ * g₂ + c₃ * g₃ + c₄ * g₄
+    -- and close via add_mem / mul_mem_left
+    suffices h : ∃ c₁ c₂ c₃ c₄ : R,
+        _ = c₁ * _ + c₂ * _ + c₃ * _ + c₄ * _ from by
+      obtain ⟨c₁, c₂, c₃, c₄, hc⟩ := h
+      rw [show _ = c₁ * _ + c₂ * _ + c₃ * _ + c₄ * _ from hc]
+      exact Ideal.add_mem $J (Ideal.add_mem $J (Ideal.add_mem $J
+        (Ideal.mul_mem_left $J c₁ $hg1)
+        (Ideal.mul_mem_left $J c₂ $hg2))
+        (Ideal.mul_mem_left $J c₃ $hg3))
+        (Ideal.mul_mem_left $J c₄ $hg4)
+    exact ⟨_, _, _, _, by zsqrtd_eq⟩
+  ))
+
+/-- Helper: prove that each element `x ∈ {g₁, g₂, g₃, g₄}` belongs to `span {p}`.
+    Dispatches each case to `ring` or `ext <;> norm_num`. -/
+
+scoped macro "close_reverse_inclusion" : tactic =>
+  `(tactic| (
+    intro x hx
+    rcases hx with rfl | rfl | rfl | rfl
+    <;> (first
+      | exact Ideal.mem_span_singleton.mpr ⟨_, by ring⟩
+      | exact Ideal.mem_span_singleton.mpr
+          ⟨_, by ext ⟨⟩ <;> norm_num [Zsqrtd.sqrtd]⟩)
+  ))
+
+/-- The `factorization_Zsqrtd_mins_5` tactic proves ideal factorization identities
+    in `ℤ[√-5]` of two forms:
+
+    1. **Product**: `⟨p⟩ = ⟨a₁, a₂⟩ · ⟨b₁, b₂⟩`
+    2. **Squared**: `⟨p⟩ = ⟨a₁, a₂⟩²`
+
+    The proof proceeds by `le_antisymm`:
+    - *Forward*: show `p` belongs to the RHS by writing it as a linear combination
+      of the four products `aᵢ * bⱼ` (or `aᵢ * aⱼ`).
+    - *Reverse*: show each generator product belongs to `⟨p⟩`.
+
+    **Performance notes:**
+    - Uses `set_option maxHeartbeats 400000` to handle complex `norm_num` evaluations.
+    - The `show_mem_by_lincomb` helper avoids deep metavariable unification by
+      deferring the linear-combination equality to a single `zsqrtd_eq` call. -/
+syntax (name := factorizationZsqrtdMins5) "factorization_Zsqrtd_mins_5" : tactic
+
+set_option maxHeartbeats 400000 in
+macro_rules
+  | `(tactic| factorization_Zsqrtd_mins_5) =>
+      `(tactic|
+        first
+        | -- Product case: span {p} = span {a1, a2} * span {b1, b2}
+          refine
+            (show span {(?p : R)} =
+                (span ({?a1, ?a2} : Set R) : Ideal R) *
+                (span ({?b1, ?b2} : Set R) : Ideal R) from ?_)
+          let J : Ideal R :=
+            span ({?a1 * ?b1, ?a1 * ?b2, ?a2 * ?b1, ?a2 * ?b2} : Set R)
+          have hmul :
+              (span ({?a1, ?a2} : Set R) : Ideal R) *
+              (span ({?b1, ?b2} : Set R) : Ideal R) = J := by
+            simp only [J, Ideal.span_pair_mul_span_pair]
+          apply _root_.le_antisymm
+          · rw [Ideal.span_singleton_le_iff_mem, hmul]
+            have hg1 : ?a1 * ?b1 ∈ J := Ideal.subset_span (by simp)
+            have hg2 : ?a1 * ?b2 ∈ J := Ideal.subset_span (by simp)
+            have hg3 : ?a2 * ?b1 ∈ J := Ideal.subset_span (by simp)
+            have hg4 : ?a2 * ?b2 ∈ J := Ideal.subset_span (by simp)
+            show_mem_by_lincomb J hg1 hg2 hg3 hg4
+          · rw [hmul]
+            refine Ideal.span_le.2 ?_
+            close_reverse_inclusion
+        | -- Squared case: span {p} = span {a1, a2} ^ 2
+          refine
+            (show span {(?p : R)} =
+                (span ({?a1, ?a2} : Set R) : Ideal R) ^ 2 from ?_)
+          let I : Ideal R := (span ({?a1, ?a2} : Set R) : Ideal R)
+          let J : Ideal R :=
+            span ({?a1 * ?a1, ?a1 * ?a2, ?a2 * ?a1, ?a2 * ?a2} : Set R)
+          have hpow : I ^ 2 = I * I := pow_two I
+          have hmul : I * I = J := by
+            simp only [I, J, Ideal.span_pair_mul_span_pair]
+          apply _root_.le_antisymm
+          · rw [Ideal.span_singleton_le_iff_mem, hpow, hmul]
+            have hg1 : ?a1 * ?a1 ∈ J := Ideal.subset_span (by simp)
+            have hg2 : ?a1 * ?a2 ∈ J := Ideal.subset_span (by simp)
+            have hg3 : ?a2 * ?a1 ∈ J := Ideal.subset_span (by simp)
+            have hg4 : ?a2 * ?a2 ∈ J := Ideal.subset_span (by simp)
+            show_mem_by_lincomb J hg1 hg2 hg3 hg4
+          · rw [hpow, hmul]
+            refine Ideal.span_le.2 ?_
+            close_reverse_inclusion)
+
+end ANT.Tactic