Registry · Lemma VII.L05 tau-effective formalized

VII.L05 — No-New-Lobe Lemma

Five generators {α,π,γ,η,ω} are exhaustive; lemniscate ∂(τ³) produces exactly four orbits under ρ-action; no sixth generator constructible.

Book VII Part 1 Ch. 8

Dependency Graph

Depends on (1)

VII.T03

Depended on by (2)

VII.P30 VII.T06

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.NonewlobeLemma