Kummer's Criterion and Regular Primes in Lean

11.2. The case-decomposition🔗

Following flt-regular's organisation of Kummer's argument for regular primes, we split Vandiver III into a first-case half and a second-case half, defined after the MayAssume.coprime reduction that pulls a common factor out of (a,b,c).

Definition11.2.1
uses 1used by 1✓L∃∀N

\mathrm{VandiverIII} asserts: every prime \ell satisfying the parity hypothesis satisfies \mathrm{FermatLastTheoremFor}\ \ell.

Definition 11.1.2

Lean code for Definition11.2.1●1 definition
  • defdefined in BernoulliRegular/FLT37/Final.lean
    complete
    def BernoulliRegular.FLT37.VandiverIII : Prop
    def BernoulliRegular.FLT37.VandiverIII : Prop
    Vandiver's Theorem III as a quantified statement. Once tickets FLT37b–g
discharge this, the unconditional `FermatLastTheoremFor 37` is immediate.
Definition11.2.2
uses 1used by 1✓L∃∀N

\mathrm{VandiverIIICaseI} asserts: under the parity hypothesis, if \ell \nmid abc then a^\ell + b^\ell \neq c^\ell.

Definition 11.1.2

Lean code for Definition11.2.2●1 definition
  • defdefined in BernoulliRegular/FLT37/Final.lean
    complete
    def BernoulliRegular.FLT37.VandiverIIICaseI : Prop
    def BernoulliRegular.FLT37.VandiverIIICaseI :
  Prop
    The first-case half of Vandiver Theorem III: the parity hypothesis on
irregular indices implies Case I of FLT for `ℓ`. Used in the planned
decomposition `VandiverIIICaseI ∧ VandiverIIICaseII → VandiverIII`
(ticket FLT37g).
Definition11.2.3
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 11.2.4
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

\mathrm{VandiverIIICaseII} asserts: under the parity hypothesis, if a,b,c are coprime and \ell \mid abc, then a^\ell + b^\ell \neq c^\ell.

Definition 11.1.2

Lean code for Definition11.2.3●1 definition
  • defdefined in BernoulliRegular/FLT37/Final.lean
    complete
    def BernoulliRegular.FLT37.VandiverIIICaseII : Prop
    def BernoulliRegular.FLT37.VandiverIIICaseII :
  Prop
    The second-case half of Vandiver Theorem III: the parity hypothesis
implies Case II of FLT for `ℓ`. The hypothesis package mirrors
`flt-regular`'s `caseII` after the `MayAssume.coprime` reduction.
Theorem11.2.4
Statement uses 3
Statement dependency previews
Preview
Definition 11.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

\mathrm{VandiverIIICaseI} \land \mathrm{VandiverIIICaseII} \Longrightarrow \mathrm{VandiverIII}.

Definition 11.2.1 Definition 11.2.2 Definition 11.2.3

Lean code for Theorem11.2.4●1 theorem
  • theoremdefined in BernoulliRegular/FLT37/Final.lean
    complete
    theorem BernoulliRegular.FLT37.vandiverIII_of_caseI_caseII
  (hI : BernoulliRegular.FLT37.VandiverIIICaseI)
  (hII : BernoulliRegular.FLT37.VandiverIIICaseII) :
  BernoulliRegular.FLT37.VandiverIII
    theorem BernoulliRegular.FLT37.vandiverIII_of_caseI_caseII
  (hI :
    BernoulliRegular.FLT37.VandiverIIICaseI)
  (hII :
    BernoulliRegular.FLT37.VandiverIIICaseII) :
  BernoulliRegular.FLT37.VandiverIII
    **Vandiver III decomposition (FLT37g).**

The two halves combine into `VandiverIII` exactly as
`flt-regular`'s `flt_regular` combines `caseI` and `caseII`:

* reduce to integers via `fermatLastTheoremFor_iff_int`,
* coprimify via `MayAssume.coprime`,
* split on `ℓ ∣ a*b*c`.
Proof for Theorem 11.2.4
uses 0

Reduce \mathrm{FermatLastTheoremFor}\ \ell to the integer statement via fermatLastTheoremFor_iff_int and apply MayAssume.coprime to assume \gcd(a,b,c) = 1. Then split on \ell \mid abc: case II handles the divisibility branch, case I the non-divisibility branch.

Theorem11.2.5
Statement uses 2
Statement dependency previews
Preview
Theorem 11.1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

\mathrm{VandiverIIICaseI} \land \mathrm{VandiverIIICaseII} \Longrightarrow \mathrm{FermatLastTheoremFor}\ 37.

Theorem 11.1.3 Theorem 11.2.4

Lean code for Theorem11.2.5●1 theorem
  • theoremdefined in BernoulliRegular/FLT37/Final.lean
    complete
    theorem BernoulliRegular.FLT37.fermatLastTheoremFor_thirtyseven_of_caseI_caseII
  (hI : BernoulliRegular.FLT37.VandiverIIICaseI)
  (hII : BernoulliRegular.FLT37.VandiverIIICaseII) :
  FermatLastTheoremFor 37
    theorem BernoulliRegular.FLT37.fermatLastTheoremFor_thirtyseven_of_caseI_caseII
  (hI :
    BernoulliRegular.FLT37.VandiverIIICaseI)
  (hII :
    BernoulliRegular.FLT37.VandiverIIICaseII) :
  FermatLastTheoremFor 37
    **Direct conditional FLT for 37.** Assuming `VandiverIIICaseI` and
`VandiverIIICaseII`, `FermatLastTheoremFor 37` follows. This composes
the Case-decomposition (`vandiverIII_of_caseI_caseII`) with the
specialisation to `ℓ = 37` (`fermatLastTheoremFor_thirtyseven_of_vandiverIII`),
making the remaining mathematical content (FLT37e, FLT37f) the only
outstanding work.
Proof for Theorem 11.2.5
uses 0

Specialise Theorem 11.2.4 to \ell = 37 using the verified parity-hypothesis witness (Theorem 11.1.3).

This reduces \mathrm{FLT}_{37} to two named hypotheses \mathrm{VandiverIIICaseI} and \mathrm{VandiverIIICaseII} at \ell = 37. The next two sections describe the substantive mathematical content of each.