Registry · Definition III.D84 tau-effective formalized

III.D84 — E₂ Orbit Structure

Orbit of code c under decoder d at stage k. Orbit lengths exhibit diversity (not all equal), proving computational richness. E₁ orbits have length ≤ 2 (bipolar); E₂ orbits can have prime lengths 3, 5, etc.

Book III Part 7 Ch. 60

Dependency Graph

Depends on (1)

Depended on by (2)

Lean Formalization

Module: TauLib.BookIII.Computation.E2Witness

Symbol: orbit_length