Registry · Theorem IV.T16 tau-effective formalized

IV.T16 — CR Parity Constraint

A character mode χ_{m,n} is CR-admissible on τ³ iff m+n ≡ 0 mod 2. Only modes with even parity sum are compatible with the CR-structure.

Book IV Part 3 Ch. 16

Dependency Graph

Depends on (3)

IV.L01 IV.D50 IV.D51

Depended on by (5)

IV.C02 IV.D54 IV.P10 IV.R13 IV.T17

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.CRAddressSpace

Symbol: Tau.BookIV.QuantumMechanics.CrParityConstraint