Registry · Proposition I.P08 established formalized

I.P08 — Dimension Theorem (dim_tau = 4)

dim_tau = 4: the four ABCD coordinates are pairwise independent (sufficiency) and no three suffice (necessity). Dimension is earned from arithmetic hierarchy, not postulated.

Book I Part 4 Ch. 20

Dependency Graph

Depends on (2)

I.D17 I.D06

Depended on by (6)

I.P46 I.R39 II.D03 II.D15 II.P03 II.T11

Lean Formalization

Module: TauLib.BookI.Coordinates.ABCD

Symbol: Tau.Coordinates.dim_tau_eq_four