Kummer's Criterion and Regular Primes in Lean

11.7. Outlook🔗

Modulo the unconditional 37 \nmid h^+ (Theorem 11.4.1), the proof of \mathrm{FLT}_{37} in this project reduces to two named hypotheses. Case I: the per-solution Bernoulli-divisibility predicate \mathrm{MirimanoffBernoulliConclusion}\ 37, derived from Mirimanoff's classical theorem (\mathrm{MBI}) combined with the verified parity hypothesis. Case II: \mathrm{VandiverLemma1Thirtyseven}, encoding the Washington 9.4 / Lehmer–Vandiver descent under 37 \nmid h^+ on \sigma-stable real data. Both are explicit cyclotomic-integer statements at the single prime 37. Neither requires a fresh layer of class field theory beyond what flt-regular and the cyclotomic-units chapter already supply.