Registry · Theorem I.T02 established formalized

I.T02 — Iterator Ladder Saturation

The iterator ladder has exactly 4 levels (0-3); higher hyper-operations lose canonical injectivity because K6 prevents a 5th orbit channel.

Book I Part 2 Ch. 8

Dependency Graph

Depends on (3)

I.D06 I.D03 I.K6

Depended on by (4)

I.D13 I.T11 I.T11b I.T11c

Lean Formalization

Module: TauLib.BookI.Orbit.Ladder

Symbol: Tau.Orbit.ladder_saturation