Registry · Proposition III.P34 tau-effective formalized

III.P34 — E₂ ⊋ E₁ Strict Witness

E₂ contains orbit structures of length > 2 that cannot be expressed as pure sector decompositions (E₁ content). E₁ orbits have length ≤ 2 from bipolar involution; E₂ orbits achieve lengths 3, 5, etc.

Book III Part 7 Ch. 60

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Computation.E2Witness

Symbol: e2_strict_3