polarized_unitStep
plain-language theorem explainer
The polarized birth field on the diamond lattice obeys the forced minimal-distinction property: every adjacency changes the rung by at most one. Cosmology cost-ledger work cites this to specialize the graded-rung total-cost law to the binary Phase-55 birth field. The proof splits equal-charge edges from flips, then applies the Phase-55 level-difference lemma to force flips into exactly ±1.
Claim. For every natural number $t$, the polarized birth field $k$ at time $t$ on the diamond ordered edge set $E(t)$ satisfies the unit-step property: for every ordered adjacency $(p,q)\in E(t)$, $k(p)-k(q)\in\{0,+1,-1\}$.
background
The graded-rung cost module lifts the Phase-55 recognition-cost ledger from a binary birth charge to an arbitrary integer rung field $k:V\to\mathbb{Z}$. The only structural hypothesis needed is UnitStep: across every edge of a finite ordered set $E$, the rung gap lies in ${0,+1,-1}$. A unit recognition step resolves at most one $\phi$-rung; the live engine keeps this invariant because T-3 refinement descends one rung at a time.
Here $E(t)$ is the total ordered adjacency Finset of the diamond ball at radius parameter $t$ (pairs of vertices linked by lattice adjacency). The polarized birth field is the Phase-55 sign-valued charge on that diamond. UnitStep for that field is exactly the forced minimal-distinction property the module needs before it can quote free bulk carriage and $J(\phi)$ per interface edge.
Upstream, Phase-55 already proved a level-difference fact on diamond adjacencies: if two adjacent vertices carry unequal polarized charge, their rung difference is exactly $+1$ or $-1$. That lemma is the bridge from the binary birth geometry to the abstract UnitStep predicate.
proof idea
Term-mode proof by cases on an arbitrary edge $p\in E(t)$. Unfold membership in $E$ to adjacency. If the polarized values at the two endpoints agree, the integer difference is $0$, giving the first UnitStep disjunct via sub_eq_zero.
If they disagree, apply PolarizedBirthInterfaceCost.Diamond.level_diff at those endpoints (using adjacency and inequality). That lemma returns a disjunction difference $=+1$ or $=-1$; each arm is re-injected into the remaining UnitStep clauses. No further arithmetic is required.
why it matters
This discharges UnitStep for the concrete polarized birth field, so the module's general cost identities (carried cost zero, total cost equals interface count times $J(\phi)$) specialize definitionally to the Phase-55 diamond ledger. The module doc records the recovery: polarized total cost is the graded totalCost at $k=\mathrm{polarized}$, with UnitStep supplied here (and the octahedron analogue elsewhere).
In the broader Recognition chain this is the geometric content of single-rung distinction on the birth lattice: free same-rung bulk, paid interface only at $J(\phi)$, matching the T5 cost $J$ and the $\phi$-ladder step. No downstream Lean users are wired yet in the graph, but the declaration is the explicit bridge named by the module for closing the binary-to-graded specialization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.