Registry · Theorem I.T11c established formalized

I.T11c — Tetration Algebraic Degradation

Tetration is algebraically degraded: non-commutative (2^^3 != 3^^2), non-associative ((2^^2)^^2 != 2^^(2^^2)), no left identity >= 2. This is the algebraic obstruction to canonicality at the 4th operation level.

Book I Part 3 Ch. 12

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Orbit.Saturation

Symbol: Tau.Orbit.Saturation.tetration_algebraic_degradation