Registry · Definition IV.D52 tau-effective formalized

IV.D52 — CR-Address

A CR-address is a pair (m,n) ∈ Z² labeling a character mode χ_{m,n} on fiber T². The full address lattice is Λ_full = Z².

Book IV Part 3 Ch. 16

Dependency Graph

Depends on (1)

Depended on by (2)

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.CRAddressSpace

Symbol: Tau.BookIV.QuantumMechanics.Craddress