Registry · Definition IV.D115 tau-effective formalized

IV.D115 — Crossing-Point Action Space

The crossing-point action space V_A := C^2 carrying the natural action of the pi-generator on two-component boundary values at x_0 in L.

Book IV Part 4 Ch. 31

Dependency Graph

Depends on (2)

Depended on by (4)

Lean Formalization

Module: TauLib.BookIV.Electroweak.WeakHolonomy

Symbol: Tau.BookIV.Electroweak.CrossingpointActionSpace