Registry · Proposition I.P05 established formalized

I.P05 — Tetration Injectivity

Tetration is injective on the canonical domain: distinct inputs yield distinct towers.

Book I Part 3 Ch. 12

Dependency Graph

Depends on (1)

I.D13

Depended on by (2)

I.L03 I.T04

Lean Formalization

Module: TauLib.BookI.Denotation.Arithmetic

Symbol: Tau.Denotation.tetration_injective