Registry · Proposition I.P01 established formalized

I.P01 — Generator Distinctness

All five generators are pairwise distinct (immediate from K1 strict order).

Book I Part 1 Ch. 1

Dependency Graph

Depends on (1)

I.K1

Depended on by (3)

I.P03 I.T07 I.T08

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.gen_distinct