Registry · Theorem IV.T81 tau-effective formalized

IV.T81 — Exactly one derived sector

The lemniscate L = S^1 v S^1 has exactly one self-intersection point, so the sector decomposition admits exactly one derived sector omega = B cap C = gamma cap eta; no other pair of primitive sectors produces a derived sector.

Book IV Part 6 Ch. 45

Dependency Graph

Depends on (3)

Lean Formalization

Module: TauLib.BookIV.Particles.SectorAtlas

Symbol: Tau.BookIV.Particles.ExactlyOneDerivedSector