Registry · Axiom I.K2 established formalized

I.K2 — Omega Fixed Point (K2)

rho(omega) = omega; omega absorbs all operations.

Book I Part 1 Ch. 2

Dependency Graph

Depends on (2)

I.D01 I.D02

Depended on by (6)

I.D04 I.P14 I.R01 I.T07 I.T08 I.T36

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.K2_omega_fixed