t58_unitStep_preservation_honest
plain-language theorem explainer
Active mean-move dynamics preserves the real unit-step rung invariant only under a local post-move edge condition, not globally. Phase 58 packages that local criterion with a three-site chain counterexample: levels 0,1,2 become 1/2,1/2,2 after resolving the first edge, so the second gap is 3/2. Cosmology and runtime-cost authors cite it to block a false global lemma. The proof is a one-line pairing of the local criterion with the explicit counterexample.
Claim. For every $n$, level field $x:\mathrm{Fin}\,n\to\mathbb{R}$, edge list $E$, and pair $(i,j)$, if $x$ is unit-step on $E$ (every edge has gap at most $1$) and every edge touching $i$ or $j$ still has gap at most $1$ after the mean-move that sends both endpoints to $(x_i+x_j)/2$, then the resolved field is unit-step on $E$. Moreover, on the three-site chain with levels $0,1,2$, resolving the first edge yields a field that is not unit-step.
background
Phase 56 proved the graded-rung cost law under the forced minimal-distinction invariant that adjacent rungs differ by at most one. Phase 57 wired that law into the runtime cost meter. The tempting next claim is that the active mean-move dynamics preserves the invariant automatically. That claim is false.
The mean-move sends both endpoints of a coupled pair to their arithmetic mean; it is the $\sigma=0$, $J$-minimal update the forward dynamics posts each tick. Because the move can create half-rungs from integer inputs, the right formulation is the real-valued unit-step condition: every listed edge has absolute level gap at most one. An edge touches the resolved pair if either of its endpoints is one of the two resolved vertices. Edges disjoint from the pair are unchanged, so the old invariant carries them for free.
This module records the honest layer: local preservation under a post-move audit of touching edges, plus an explicit three-site counterexample showing the audit is necessary.
proof idea
Term-mode pairing of two already-proved facts. The left conjunct is the local preservation criterion: given unit-step on the whole edge list and the post-move gap bound on every edge that touches the resolved pair, the resolved field is unit-step. The right conjunct is the named three-chain counterexample: the chain $0$--$1$--$2$ starts unit-step; after resolving the first edge the levels are $1/2,1/2,2$, so the second edge has gap $3/2>1$. No new algebra is done here.
why it matters
Phase-58 headline for recognition-unit-step dynamics in the cosmology layer. It blocks the false global theorem that mean-move preserves unit-step, and forces the live engine to audit or prove the local condition before applying the Phase-56 graded-rung cost law to an actively updated field. The module doc is explicit: a blind global preservation lemma would be false.
No downstream theorems currently depend on this packaging (used-by is empty); it stands as a boundary marker for runtime cost metering after active updates. It sits downstream of the forcing chain (T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick octave, T8 $D=3$) and of the Recognition Composition Law, in the layer that applies those structures to rung fields on lattice edges. HONEST STATUS is theorem, zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.