Registry · Proposition IV.P35 tau-effective formalized

IV.P35 — Photon as Boundary Character

Under the Central Theorem isomorphism, the photon corresponds to a boundary character on L supported on the B-sector lobe with no Hartogs extension.

Book IV Part 4 Ch. 26

Dependency Graph

Depends on (3)

IV.D82 IV.T33 IV.T34

Lean Formalization

Module: TauLib.BookIV.Electroweak.PhotonMode

Symbol: Tau.BookIV.Electroweak.PhotonAsBoundaryCharacter