span_lepton_eq_W
plain-language theorem explainer
The lepton generation span sums exactly to the number of distinct 2D wallpaper groups. Researchers deriving forced mass hierarchies from sector-dependent torsion would cite this to fix leptons in the middle of the generation ladder. The proof is a one-line unfolding of the wallpaper count definition followed by native arithmetic decision.
Claim. The lepton sector steps satisfy $11 + 6 = 17$, where 17 is the number of distinct two-dimensional wallpaper groups.
background
The SDGT Forcing Theorem shows that sector-dependent generation torsion is forced by three constraints: the partition sum of overlapping consecutive-pair spans must equal N₃ = 55, only the pair {11, 6} sums to the wallpaper count W = 17, and charge asymmetry selects the unique ordering. The upstream definition states that wallpaper_groups equals 17, the standard crystallographic constant proven by Fedorov in 1891. The Constants structure supplies the abstract bundle of CPM constants used to normalize the curvature fraction.
proof idea
One-line wrapper that unfolds the definition of wallpaper_groups to the constant 17 and applies native_decide to confirm the arithmetic equality 11 + 6 = 17.
why it matters
This theorem supplies the lepton uniqueness step inside the SDGT forcing theorem, which selects the unique assignment of spans {13, 11} for up quarks, {11, 6} for leptons, and {6, 8} for down quarks. It closes one of the three forcing constraints listed in the module documentation. The four step values themselves remain open for derivation from a single principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.