Registry · Axiom I.K4 established formalized

I.K4 — No-Jump / Cover (K4)

rho is a successor within each orbit (no skipping); covers are primitive.

Book I Part 1 Ch. 3

Dependency Graph

Depends on (1)

I.D02

Depended on by (7)

I.D04 I.P02 I.P14 I.R01 I.T07 I.T08 IV.T34p

Lean Formalization

Module: TauLib.BookI.Kernel.Axioms

Symbol: Tau.Kernel.K4_no_jump