Fmono
plain-language theorem explainer
Defines the monochromatic edge list on the radius-t diamond: every 4-neighbour pair whose two cells carry the same polarized birth charge. Cosmology proofs that bound locked domains of the forced conjugate-birth field cite it as the connectivity graph. Construction is a one-line filter of the ordinary diamond edge list by equal polarized charge.
Claim. For each radius $t\in\mathbb{N}$, let $E_t$ be the list of ordered 4-neighbour pairs of cells in the diamond ball of radius $t$. The monochromatic edge list $F^{\mathrm{mono}}_t$ is the sublist of pairs $(u,v)\in E_t$ with equal polarized birth charge: $\mathrm{pol}_t(u)=\mathrm{pol}_t(v)$, where $\mathrm{pol}_t$ is $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$.
background
Module PolarizedBirthDomains fixes the carried state of the forced conjugate-birth field on the 2D diamond: charge $+1$ for $x>0$, $-1$ for $x<0$, and $0$ on the $x=0$ spine. Phase 48 (InterfaceComponentBound) already bounds locked domains by interface size for an arbitrary charge field; Phase 49 gives the diamond volume $2t^2+2t+1$. Here the charge field is specialized so that monochromatic connectivity collapses to three super-regions independent of $t$.
Upstream, edges t is the full 4-neighbour edge list on diamond vertices Vtx t (cells of the $\ell_1$ ball of radius $t$). The ordinary L1 height is $|x|+|y|$. The polarized field partitions cells by sign of $x$; monochromatic edges are those that never cross a charge interface. That restricted graph is the object this definition names.
proof idea
Pure definition: take the diamond edge list edges t and keep only those ordered pairs whose two endpoints have equal polarized t charge (via List.filter and decide). No lemma is applied; the body is the filter itself. Downstream membership is recovered by mem_Fmono (adjacency plus equal charge implies membership in the filtered list).
why it matters
This is the connectivity relation on which the whole carried-state argument runs. The monochromatic descent theorem hdesc steps along Fmono toward one of the three roots $(1,0)$, $(-1,0)$, $(0,0)$; clos_someRoot_of_descent and comp_le_of_roots then give at most three locked components. That feeds polarized_components_eq_three and the North-Star claim polarized_carried_subextensive: a $\Theta(t^2)$ world is carried as exactly three super-regions, so components/volume $\to 0$. It makes precise "carry each region at the coarsest $\varphi$-rung its recognition allows" for the birth configuration installed each cadence cycle, as a theorem rather than a numeric check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.