carried_ge_interface
plain-language theorem explainer
For a 2D L1 diamond world of radius t ≥ 1, the monochromatic carried edges outnumber the bichromatic interface edges: 8t² − 8t + 4 ≥ 8t − 4, with equality only at t = 1. Cosmology and coarsening arguments cite this as the ledger inequality that the bulk is carried free once the world exceeds a single shell. The proof rewrites both cardinalities to closed forms and finishes by elementary arithmetic.
Claim. For every natural number $t \ge 1$, the number of bichromatic (forced-distinction) ordered edges of the polarized birth field on the 2D L1 diamond of radius $t$ is at most the number of monochromatic (carried-internal) ordered edges: $|B(t)| \le |\mathrm{carried}(t)|$, equivalently $8t-4 \le 8t^2-8t+4$.
background
This module sits in the coarsening ledger for the polarized birth field on lattice balls. Every ordered adjacency is either a bichromatic interface edge (forced distinction the engine must post) or a monochromatic carried edge (internal to a locked domain, carried coarse for free). The interface set $B(t)$ is the Finset of ordered adjacent pairs with unequal polarization; its cardinality is the known closed form $8t-4$ in 2D.
The carried set is the complementary filter of the total ordered adjacency Finset $E(t)$: equal-charge edges. Upstream, carried_edge_card proves that this complement has exact size $8t^2-(8t-4)=8t^2-8t+4$, using the total edge count $8t^2$ from the volume-minus-boundary analysis of the diamond and the interface count. The module doc frames the asymptotic: the carried fraction tends to 1, so almost every adjacency is free once the world grows.
The local setting is the 2D diamond (4-neighbour L1 ball); the 3D octahedron analogues live in the same file under a separate namespace.
proof idea
One short tactic proof. Rewrite the left side by the Diamond interface closed form (interface_card_eq) and the right side by carried_edge_card, reducing the goal to $8t-4 \le 8t^2-8t+4$ for $t\ge 1$. Write $t=n+1$ via omega, expand $(n+1)^2$ by ring, and discharge the resulting polynomial inequality by omega. No further combinatorial work: both cardinalities are already closed forms.
why it matters
This is the exact inequality form of the coarsening north star for the 2D diamond: carry the bulk coarse, pay only for the interface. The doc-comment states the comparison $8t^2-8t+4\ge 8t-4$ with equality only at $t=1$, so the carried bulk strictly overtakes the posted interface as soon as the world is larger than a single shell. It packages the two closed forms (interface count from PolarizedBirthInterfaceCount and carried count from this module) into a single citation-ready dominance statement.
No downstream Lean users are wired yet (used_by is empty), but the module narrative positions it as the payoff of the total-versus-interface split that justifies free monochromatic carry in the polarized birth cosmology. It does not invoke the forcing chain T0–T8 or the J-cost directly; it is a pure lattice-combinatorics ledger fact supporting the RS coarsening picture in $D=2$ before the 3D octahedron counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.