iwasawa_main_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result iwasawa_main_conjecture is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Iwasawa's main conjecture (1969): The characteristic ideal of the Iwasawa module over the cyclotomic ℤₚ-extension is generated by the p-adic L-function. Proved for abelian fields over ℚ (Mazur–Wiles 1984, Rubin 1991), and for many other cases. General version for non-abelian extensions is open.

Why this node was retired

The posted statement is

import Mathlib

theorem iwasawa_main_conjecture (p : ℕ) (hp : Nat.Prime p) (hp_odd : p ≠ 2)
    (K : Type*) [Field K] [NumberField K] :
    ∃ (char_ideal : Ideal (ZMod p)),
      char_ideal ≠ ⊤ ∧
      ∀ s : ℂ, s.re > 1 →
        True := by
  sorry

The goal is ∃ char_ideal : Ideal (ZMod p), char_ideal ≠ ⊤ ∧ ∀ s : ℂ, s.re > 1 → True. The second conjunct is True, and ⊥ witnesses the first, so the goal holds for trivial reasons. The characteristic ideal of an Iwasawa module and the p-adic L-function occur nowhere; Ideal (ZMod p) is not the object the conjecture is about.

What a faithful statement would require

The Iwasawa module over the Iwasawa algebra and its characteristic ideal must be formalized alongside the p-adic L-function, and the conclusion must be the equality of the two.

No corrected replacement node exists yet.