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.

Polarized Omega-Germ

Summary

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.

Statement

%
\label{def:polarized-germ}
Let $W[\omega]$ be a base omega-germ
for which the channel systems $(B_n)$ and $(C_n)$
are defined.
\begin{itemize}
    \item $W[\omega]$ is \textbf{B-polarized}
          if $(C_n)$ is eventually constant
          while $(B_n)$ refines nontrivially
          (is not eventually constant).
    \item $W[\omega]$ is \textbf{C-polarized}
          if $(B_n)$ is eventually constant
          while $(C_n)$ refines nontrivially.
\end{itemize}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 65
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part07/ch29-polarized-omega-germs.tex lines 116-131

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Polarity.PolarizedGerms
• Name: Tau.Polarity.BPolarized

Dependencies

• Canonical: I.D25, I.T05

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.