diff --git a/.beads/issues.jsonl b/.beads/issues.jsonl index d93ddd2..e0fb8d2 100644 --- a/.beads/issues.jsonl +++ b/.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."} diff --git a/ANT.lean b/ANT.lean index ad9c22b..32a787a 100644 --- a/ANT.lean +++ b/ANT.lean @@ -1,2 +1,3 @@ import ANT.Basic import ANT.Ideals +import ANT.RamificationInertia diff --git a/ANT/RamificationInertia.lean b/ANT/RamificationInertia.lean new file mode 100644 index 0000000..51da411 --- /dev/null +++ b/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 diff --git a/ANT/Tactic.lean.disable b/ANT/Tactic.lean.disable new file mode 100644 index 0000000..75a82c4 --- /dev/null +++ b/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