Registry · Lemma II.L10 established formalized

II.L10 — Polarity Symmetry

The j-involution interchanges bipolar sectors: sigma_j(G_+) = G_- and sigma_j(G_-) = G_+, so one sector determines the full transformer.

Book II Part 7 Ch. 38

Dependency Graph

Depends on (6)

I.T05 I.D21 I.D22 I.D23 II.L08 II.L09

Depended on by (1)

II.T33

Lean Formalization

Module: TauLib.BookII.Regularity.ThreeLemmaChain

Symbol: polarity_symmetry_check