UnitStep
plain-language theorem explainer
UnitStep is the forced minimal-distinction property: an integer rung field on vertices changes by at most one across every ordered edge. Cosmology and ledger proofs cite it as the sole structural hypothesis for graded-rung cost. It is a pure Prop definition (no proof body), encoding that each adjacency is carried (gap 0) or a single-rung interface (±1).
Claim. For a rung assignment $k : V \to \mathbb{Z}$ and a finite ordered edge set $E \subseteq V \times V$, the unit-step property holds when every edge $(p,q) \in E$ satisfies $k(p)-k(q) \in \{0,+1,-1\}$.
background
Module GradedRungCost lifts the Phase-55 binary birth ledger to arbitrary integer rung profiles. Phase 55 treated charge in ${+1,0,-1}$; the live engine instead carries a multi-valued phi-rung field, coarsest rung each region allows. The cost law needs only one structural fact: across every adjacency the rung changes by at most one.
That fact is UnitStep. A unit recognition step resolves at most one phi-rung, so $k(p)-k(q)\in{0,+1,-1}$ on every edge. The lattice plus single-rung-step law forces it (the Phase-55 level_diff mechanism), and the engine keeps it because the T-3 refiner descends one rung at a time.
Related edge sets include the diamond adjacency Finset $E(t)$ and its carried (equal-charge) subset. The cost functional is built from the Recognition J-cost: equal-rung edges pay $J(\phi^0)=J(1)=0$; unit gaps pay $J(\phi^{\pm 1})=J(\phi)$ by reciprocal symmetry.
proof idea
Definition only: the body is the Prop
$\forall p\in E,; k(p_1)-k(p_2)\in{0,+1,-1}$.
No tactics or lemmas. Downstream theorems take hk : UnitStep k E and case-split on the three disjuncts (e.g. edgeCost_interface discards the zero gap via hne, then uses reciprocal symmetry of $J$ on $\pm 1$).
why it matters
UnitStep is the sole hypothesis of the Phase-56 graded-rung cost ledger. The headline t56_graded_cost_ledger states: under UnitStep, carried bulk costs zero, total cost equals interface cost, and total cost equals (interface edge count) times $J(\phi)$, with $J(\phi)>0$.
It feeds edgeCost_interface, interfaceCost_eq_card, totalCost_eq_card, and totalCost_eq_interfaceCost. Polarized birth recovers as the special case: polarized_unitStep discharges UnitStep from Phase-55 level_diff, and polarized_totalCost_card recovers the 2D closed form $(8t-4)\cdot J(\phi)$.
Framework link: T5 forces $J(x)=(x+x^{-1})/2-1$, so one-rung gaps cost exactly $J(\phi)$. The property is not fitted; it is the engine invariant from single-rung T-3 refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.