Module

GeneratorGap.lean

Nyll.ProCGroups.GolodShafarevich.GeneratorGap

1 declaration indexed from sourceView source ↗

Module documentation

The numerical Golod--Shafarevich gap used by the Martinet seed

This is the arithmetic step that turns a 3-class rank of at least six and the Shafarevich upper bound r <= d + 2 into the non-strict inequality needed to contradict the finite Golod--Shafarevich bound.

Imports1

Mathlib.Data.Nat.Basic

Imported by1

Nyll.ProCGroups.GolodShafarevich.All

theorem

four_mul_add_two_le_sq

L21 ↗

ClassFieldTower.Martinet.four_mul_add_two_le_sq

Documentation

For generator rank at least six, four times the Shafarevich upper bound d + 2 is at most the square of the generator rank.

Source context 1 command

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTower.Martinet

Lean source · statement

theorem four_mul_add_two_le_sq {d : ℕ} (hd : 6 ≤ d) :
    4 * (d + 2) ≤ d ^ 2

Module documentation

The numerical Golod--Shafarevich gap used by the Martinet seed

Declarations

four_mul_add_two_le_sq