Registry · Definition I.D06 established formalized

I.D06 — Iterator Ladder

The operator ladder: rho (raw iteration) -> mu (multiplication) -> nu (exponentiation) -> theta (tetration).

Book I Part 2 Ch. 8

Dependency Graph

Depends on (2)

I.D02 I.D03

Depended on by (10)

I.D10 I.D11 I.D12 I.D13 I.L01 I.P08 I.T02 I.T05 II.D30 II.T23

Lean Formalization

Module: TauLib.BookI.Orbit.Ladder

Symbol: Tau.Orbit.iterator_ladder