Registry · Theorem I.T04 established formalized

I.T04 — Hyperfactorization Theorem

HINGE THEOREM 1: Every x in Obj(tau) has a unique canonical NF via three critical lemmas (tetration injectivity, no-tie determinism, strict remainder descent). Provable in ZFC.

Book I Part 5 Ch. 24

Dependency Graph

Depends on (4)

I.P05 I.L03 I.L04 I.D17

Depended on by (18)

I.C01 I.C04 I.D19 I.D19e I.D31 I.R38 I.T05 II.D02 II.D18a II.D18b II.D24 II.D26 II.R04 II.R06a II.T01 II.T03 II.T11 II.T20

Lean Formalization

Module: TauLib.BookI.Coordinates.Hyperfact

Symbol: Tau.Coordinates.hyperfact_check