Registry · Proposition IV.P11 tau-effective formalized

IV.P11 — Characters on T²

A character on T² is determined by (m,n) ∈ Z×Z via χ_{m,n}(θ_γ,θ_η) = exp(i(mθ_γ + nθ_η)). m = γ-winding (Radials), n = η-winding (Beacons).

Book IV Part 3 Ch. 17

Dependency Graph

Depends on (2)

Depended on by (2)

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.QuantumCharacters

Symbol: Tau.BookIV.QuantumMechanics.CharactersOnT