11.4. Case II: descent under 37 not dividing h-plus
Case II at irregular primes is substantially harder than case I. The classical
Washington 9.4 / Lehmer–Vandiver descent argument requires the hypothesis
p \nmid h^+ (Vandiver's conjecture for p), where
h^+ = h(\mathbb{Q}(\zeta_p)^+) is the class number of the maximal real subfield. At
p = 37 this hypothesis is not an assumption: it is proved unconditionally in the
cyclotomic-units chapter of this blueprint, via Sinnott's index formula combined with
a direct Bernoulli-table computation at the irregular index 32.
37 \nmid h^+(\mathbb{Q}(\zeta_{37})).
The Lean declaration BernoulliRegular.FLT37.Sinnott.flt37_not_dvd_hPlus lives in a
module outside the import closure of the BernoulliRegular root, so this node is left
unwired here.
Combines two ingredients. First, Sinnott's index formula
[\mathcal{O}_{\mathbb{Q}(\zeta_p)^+}^\times : C^+] = 2^{(p-3)/2} \cdot h^+ reduces
p \nmid h^+ to the p-coprimality of the cyclotomic-unit index
[E^+ : C^+]. Second, the p-coprimality of that index follows from the
non-divisibility p \nmid B_{2k} at all relevant k except possibly the irregular
ones; at p = 37 the unique irregular index k = 16 is discharged by a direct
congruence check on B_{32}\bmod 37^2 (the Bernoulli-table computation).
Under 37 \nmid h^+, the case-II descent is captured by the predicate
\mathrm{VandiverLemma1Thirtyseven}, which encodes the regularity-free structural
input needed for the Washington 9.4 descent.
\mathrm{VandiverLemma1Thirtyseven} asserts: for any coprime integers a,b,c with
37 \mid abc, a^{37} + b^{37} \neq c^{37}.
Lean code for Definition11.4.2●1 definition
Associated Lean declarations
-
defdefined in BernoulliRegular/FLT37/CaseII.leancomplete
def BernoulliRegular.FLT37.VandiverLemma1Thirtyseven : Prop
def BernoulliRegular.FLT37.VandiverLemma1Thirtyseven : Prop
**Vandiver Lemma 1 predicate, ℓ = 37 specialization.** Captures the regularity-free structural input needed for case II at ℓ = 37: under the parity hypothesis plus `37 ∤ h⁺`, the ideals arising in the case II decomposition are principal even without the regular-prime hypothesis. The reflection theorem T044 (already established in `Reflection/Final.lean`) is one of the inputs to discharging this predicate.
\mathrm{VandiverLemma1Thirtyseven} implies \mathrm{VandiverIIICaseII} at
\ell = 37.
Lean code for Theorem11.4.3●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/FLT37/CaseII.leancomplete
theorem BernoulliRegular.FLT37.caseII_thirtyseven_of_vandiverLemma1 (h : BernoulliRegular.FLT37.VandiverLemma1Thirtyseven) ⦃a b c : ℤ⦄ : a * b * c ≠ 0 → {a, b, c}.gcd id = 1 → 37 ∣ a * b * c → a ^ 37 + b ^ 37 ≠ c ^ 37
theorem BernoulliRegular.FLT37.caseII_thirtyseven_of_vandiverLemma1 (h : BernoulliRegular.FLT37.VandiverLemma1Thirtyseven) ⦃a b c : ℤ⦄ : a * b * c ≠ 0 → {a, b, c}.gcd id = 1 → 37 ∣ a * b * c → a ^ 37 + b ^ 37 ≠ c ^ 37
**caseII for ℓ = 37 from VandiverLemma1Thirtyseven.** The conditional theorem: given the 37-specific Vandiver Lemma 1 predicate (which encodes the case II descent for irregular 37 under the parity hypothesis), case II for 37 follows.
11.4.1. Where VandiverLemma1Thirtyseven comes from
The Lehmer–Vandiver machinery in BernoulliRegular/FLT37/LehmerVandiver/ formalises
the Washington 9.4 descent in the \sigma-stable product form recommended by the
2026-05-27 expert review. The descent proceeds as follows.
Starting from a putative case-II solution at level m \ge 1 (i.e.
x^p + y^p = \varepsilon \cdot ((\zeta-1)^{m+1} \cdot z)^p in
\mathcal{O}_{\mathbb{Q}(\zeta_p)} with \zeta - 1 \nmid y, z), one factors
x^p + y^p = \prod_\eta (x + y\eta) over the p-th roots of unity. The ideals
\mathfrak a(\eta) such that (\mathfrak a(\eta))^p is the \mathfrak p-coprime
part of \bigl((x + y\eta)/(\zeta-1)\bigr)/(\mathfrak m) are pairwise coprime
p-th powers and provide the descent ideals.
Because the raw quotient \mathfrak a(\eta)/\mathfrak a(\eta_0) is not fixed by
complex conjugation, the descent at the unit-class level is run on the
\sigma-stable product \mathfrak a(\eta) \cdot \mathfrak a(\eta^{-1}) and its
anchored ratio against \mathfrak a(\eta_0) \cdot \mathfrak a(\eta_0^{-1}). Under
37 \nmid h^+ this ratio is principal in \mathcal{O}_{K^+}, giving real descent
generators x, y \in \mathcal{O}_{K^+} with (x) \cdot J = (y) \cdot J_0. Combined
with the p-th-power identity coming from the polynomial factorisation, these
generators produce a Cramer-style Fermat-like equation
\varepsilon_1' \, X^{37} + \varepsilon_2' \, Y^{37} = Z^{37}
in \mathcal{O}_K with X, Y, Z real (fixed by complex conjugation) and
\varepsilon_1', \varepsilon_2' \in \mathcal{O}_K^\times explicitly constructed
units. Iterating the descent yields strictly decreasing \mathfrak p-adic exponents,
hence a contradiction.
The substantive open content is closing this chain: the Cramer Fermat identity is
shipped at \mathcal{O}_K level (file LehmerVandiver/CaseII/ProductDescent.lean);
discharging \mathrm{VandiverLemma1Thirtyseven} then requires using this identity to
produce a new \mathrm{RealCaseIIData37} at a strictly smaller \mathfrak p-adic
exponent, completing the infinite descent. This is the only remaining mathematical
input.