Registry · Proposition I.P02 established formalized

I.P02 — rho Injectivity Per Orbit

rho is injective on each orbit ray (from K4 no-jump/cover property).

Book I Part 1 Ch. 3

Dependency Graph

Depends on (2)

I.K4 I.D02

Depended on by (2)

I.P04 I.P17

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.rho_injective