UnitStepReal
plain-language theorem explainer
The real-valued unit-step invariant says every listed edge has absolute level gap at most one. Cosmology authors cite it when applying the Phase-56 graded-rung cost under active mean-move updates, where half-rungs appear. It is a one-line Prop definition packaging that edgewise bound for later local-preservation and counterexample theorems.
Claim. For a real assignment $x$ on $n$ sites and an edge list $E$, the unit-step property holds if and only if $|x_i-x_j|\le 1$ for every edge $(i,j)\in E$.
background
Phase 56 established the graded-rung cost law under a minimal-distinction invariant: adjacent rungs differ by at most one. Phase 57 wired that law into the runtime cost meter. Active recognition dynamics then apply mean-move pair resolution, which can send integer rungs to half-rungs, so the invariant must be stated over reals rather than integers.
This module sits in that honest layer. The global claim that every mean-move preserves unit-step is false; only a local post-move check on edges touching the resolved pair is sound. The real-valued formulation is exactly the predicate those local and counterexample theorems quantify over.
An edge list here is an ordinary list of ordered site pairs (as in the engine's adjacency export). The absolute difference bound is the level gap on that edge.
proof idea
Pure definition: the proposition is the universal quantification that every edge $e$ in the list satisfies $|x(e_1)-x(e_2)|\le 1$. No lemmas, tactics, or proof obligations.
why it matters
This predicate is the common interface for the Phase-58 honesty package. The local criterion pairResolve_unitStep_of_local assumes it on the input field and concludes it after the mean-move once every touching edge still has gap at most one. The three-site chain theorems use it both positively (levels $0,1,2$ start unit-step) and negatively (after resolving the first edge, levels $1/2,1/2,2$ break the second edge with gap $3/2$).
The headline t58_unitStep_preservation_honest packages that dichotomy: global preservation fails, local preservation is the exact audit condition before reusing the Phase-56 cost law on an actively updated field. Without the real-valued form, half-rung mean-moves would fall outside the integer unit-step language and the counterexample could not be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.