Registry · Axiom I.K3 established formalized

I.K3 — Orbit-Seeded Generation (K3)

Each generator g in {alpha, pi, gamma, eta} seeds its orbit ray O_g = {rho^n(g) : n >= 0}.

Book I Part 1 Ch. 3

Dependency Graph

Depends on (3)

I.D01 I.D02 I.K1

Depended on by (9)

I.D04 I.D05 I.P14 I.R01 I.T01 I.T07 I.T08 I.X01 V.T07

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.K3_orbit_seeded