Registry · Definition IV.D259 tau-effective formalized

IV.D259 — Boundary character

A boundary character on L is a group homomorphism chi : pi_1(L) -> U(1) assigning a phase to each homotopy class of loops. Since pi_1(L, omega) = F_2 = (free group on two generators), the character variety is T^2, matching the fiber torus of the fibered product structure.

Book IV Part 1 Ch. 5

Lean Formalization

Module: TauLib.BookIV.Arena.BoundaryHolonomy

Symbol: Tau.BookIV.Arena.BoundaryCharacter