Registry · Axiom I.K5 established formalized

I.K5 — Beacon Non-Successor (K5)

omega is NOT in the image of rho restricted to any orbit ray; omega is unreachable by finite iteration.

Book I Part 1 Ch. 2

Dependency Graph

Depends on (2)

I.D01 I.D02

Depended on by (8)

I.D04 I.P03 I.R01 I.T01 I.T07 I.T08 I.T36 II.R13

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.K5_beacon_non_succ