11.3. Case I: the Mirimanoff route
For a putative case-I solution a^p + b^p = c^p with p \nmid abc, set
t = -a / b \pmod p. Classical Mirimanoff theory (Ribenboim, 13 Lectures on
Fermat's Last Theorem, Lecture VIII) gives a chain of congruences in \mathbb{F}_p
relating t to the values of the Mirimanoff polynomials
\varphi_n(t) := \sum_{j=1}^{p-1} j^{n-1}\, t^j \in \mathbb{F}_p[t], \qquad n = 1, 2, \ldots, p-2.
These polynomials arise from the cyclotomic-unit factorisation of a^p + b^p
combined with Stickelberger's annihilator and the p-adic logarithm. The Lean
development captures the chain through three predicates of increasing strength.
\mathrm{MirimanoffPolynomialVanishing} asserts: for every n with
2 \le n \le p - 3, \varphi_n(t) \equiv 0 \pmod p.
Lean code for Definition11.3.1●1 definition
Associated Lean declarations
-
defdefined in BernoulliRegular/FLT37/CaseI/Part3.leancomplete
def BernoulliRegular.FLT37.MirimanoffPolynomialVanishing (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : Prop
def BernoulliRegular.FLT37.MirimanoffPolynomialVanishing (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : Prop
**Mirimanoff polynomial vanishing predicate.** The classical conclusion of Mirimanoff's theorem: under FLT case I + regularity, the Mirimanoff polynomial `φ_n` vanishes at `t = -a · b⁻¹ (mod p)` for all `n` in the range `2 ≤ n ≤ p - 3`. The Mirimanoff polynomial here is from `Mirimanoff.lean`.
\mathrm{MirimanoffBernoulliIdentity} asserts the product congruence
\varphi_n(t) \cdot B_{p-n} \equiv 0 \pmod p for every odd n with
2 \le n \le p - 3.
Lean code for Definition11.3.2●1 definition
Associated Lean declarations
-
defdefined in BernoulliRegular/FLT37/CaseI/Part3.leancomplete
def BernoulliRegular.FLT37.MirimanoffBernoulliIdentity (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : Prop
def BernoulliRegular.FLT37.MirimanoffBernoulliIdentity (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : Prop
**Mirimanoff-Bernoulli identity predicate** (classical Mirimanoff theorem, Ribenboim, *13 Lectures on Fermat's Last Theorem*, Lecture VIII Theorem 1B). For an FLT case I solution `(a, b, c)` at `p` and `t = -a · b⁻¹ ∈ ZMod p`, the classical Mirimanoff theorem gives the **product congruence** `φ_n(t) · B_{p-n} ≡ 0 (mod p)` for every odd `n` with `2 ≤ n ≤ p - 3`. (Equivalently, with `2s = p - n` ranging over even values in `[2, p-3]`, the congruence reads `φ_{p-2s}(t) · B_{2s} ≡ 0 (mod p)` for `s ∈ [1, (p-3)/2]`.) Combined with the parity hypothesis (every irregular Bernoulli index of `p` has even `k`) and `p ≡ 1 (mod 4)`, the congruence at indices `n ≡ 3 (mod 4)` forces `B_{p-n} ≢ 0 (mod p)` (parity rules out the odd `k = (p-n)/2`), so the product factors give the polynomial vanishing `φ_n(t) ≡ 0 (mod p)` — see `mirimanoffPolynomial_eval_eq_zero_of_mbi_and_parity` for the bridge. The previous formulation `(p-1)·φ_n(t) ≡ -n·B_{p-n}·(1-t^n) (mod p)` was incorrect (numerical refutation at `p = 5, n = 3, t = 2`: LHS = 4, RHS = 1) and has been replaced by the classical product form.
\mathrm{MirimanoffBernoulliConclusion} asserts: for every n with
2 \le n \le p - 3 such that t^n \not\equiv 1 \pmod p,
p \mid \mathrm{num}(B_{p-n}).
Lean code for Definition11.3.3●1 definition
Associated Lean declarations
-
defdefined in BernoulliRegular/FLT37/CaseI/Part3.leancomplete
def BernoulliRegular.FLT37.MirimanoffBernoulliConclusion (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : Prop
def BernoulliRegular.FLT37.MirimanoffBernoulliConclusion (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : Prop
**Direct Bernoulli divisibility predicate.** A higher-level alternative to the conjunction `MirimanoffPolynomialVanishing ∧ MirimanoffBernoulliIdentity`: directly state the conclusion that under FLT case I, for every `n` in the range `2 ≤ n ≤ p - 3` such that `t^n ≠ 1` in `ZMod p`, the prime `p` divides the numerator of the Bernoulli number `B_{p - n}`. This predicate is implied by the conjunction (via `bernoulli_dvd_of_mirimanoff_polynomial_vanishing`), and is easier to consume downstream.
The Mirimanoff–Bernoulli identity (\mathrm{MBI}) is the classical Mirimanoff
theorem. Combined with the Vandiver III parity hypothesis it forces
\varphi_n(t) \equiv 0 \pmod p for every n \equiv 3 \pmod 4 in range, because the
parity hypothesis rules out p \mid \mathrm{num}(B_{p-n}) when (p-n)/2 is odd, so
the other factor of the product congruence must vanish. That in turn yields the
Bernoulli-divisibility conclusion (\mathrm{MBC}).
At \ell = 37, \mathrm{MirimanoffBernoulliConclusion}\ 37\ a\ b for a case-I
solution (a,b,c) produces a contradiction (i.e. no such solution exists).
Lean code for Theorem11.3.4●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/FLT37/Final.leancomplete
theorem BernoulliRegular.FLT37.caseI_thirtyseven_of_bernoulli_conclusion {a b c : ℤ} (heq : a ^ 37 + b ^ 37 = c ^ 37) (hc : ¬37 ∣ c) (hb : ¬37 ∣ b) (hMC : BernoulliRegular.FLT37.MirimanoffBernoulliConclusion 37 a b) : False
theorem BernoulliRegular.FLT37.caseI_thirtyseven_of_bernoulli_conclusion {a b c : ℤ} (heq : a ^ 37 + b ^ 37 = c ^ 37) (hc : ¬37 ∣ c) (hb : ¬37 ∣ b) (hMC : BernoulliRegular.FLT37.MirimanoffBernoulliConclusion 37 a b) : False
**ℓ = 37 conditional case I via `MirimanoffBernoulliConclusion`.** Takes the higher-level Bernoulli-divisibility predicate directly.
This is the case-I closure: once \mathrm{MBC} is discharged from \mathrm{MBI}
(which is the genuine open analytic content of case I), case I at \ell = 37 is
proved.