Registry · Definition IV.D54 tau-effective formalized

IV.D54 — CR-Admissible Sublattice

The CR-admissible sublattice Λ_CR = {(m,n) ∈ Z² : m+n ≡ 0 mod 2}. Index-2 sublattice (checkerboard), generated by (1,1) and (1,-1).

Book IV Part 3 Ch. 16

Dependency Graph

Depends on (2)

IV.T16 IV.D52

Depended on by (10)

IV.D57 IV.D60 IV.P10 IV.P12 IV.P13 IV.R14 IV.T17 IV.T18 IV.T19 IV.T20

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.CRAddressSpace

Symbol: Tau.BookIV.QuantumMechanics.CradmissibleSublattice