Registry · Lemma I.L03 established formalized

I.L03 — No-Tie Determinism

Maximal tetration height C is uniquely determined. Tower atoms T(A,b1,c1) = T(A,b2,c2) implies (b1,c1) = (b2,c2). Super-exponential growth of tetration prevents ties.

Book I Part 5 Ch. 22

Dependency Graph

Depends on (3)

I.D19c I.P05 I.P07

Depended on by (1)

I.T04

Lean Formalization

Module: TauLib.BookI.Coordinates.NoTie

Symbol: Tau.Coordinates.no_tie