Registry · Proposition IV.P10 tau-effective formalized

IV.P10 — Density Halving

Λ_CR has density 1/2 in Z². The CR parity constraint eliminates exactly half the naive mode space.

Book IV Part 3 Ch. 16

Dependency Graph

Depends on (2)

IV.D54 IV.T16

Depended on by (1)

IV.R13

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.CRAddressSpace

Symbol: Tau.BookIV.QuantumMechanics.DensityHalving