Registry · Definition I.D26 established formalized

I.D26 — Polarized Omega-Germ

B-polarized omega-germ: C-channel eventually constant while B-channel refines nontrivially. C-polarized: symmetric. Formalizes 'the B-channel wins' / 'the C-channel wins' as eventual stabilization of inverse system factors.

Book I Part 7 Ch. 29

Dependency Graph

Depends on (2)

Depended on by (4)

Lean Formalization

Module: TauLib.BookI.Polarity.PolarizedGerms

Symbol: Tau.Polarity.BPolarized