exists_top_descent_unitStep
plain-language theorem explainer
For any nonempty edge set carrying a unit-step integer rung field, the realised maximum rung M is attained on some edge vertex, and descending exactly the cells at that top rung preserves the unit-step invariant. Cosmology and cost-meter authors cite this as the parameter-free existence of a safe one-rung relaxation. The proof reads M off the finite image of k on edge vertices and feeds the top-rung cut lemma.
Claim. Let $k:V\to\mathbb{Z}$ be a rung field and $E$ a nonempty finite set of ordered edges. If every edge changes $k$ by at most one (the unit-step property), then there exists an integer $M$ attained as $k(v)$ for some vertex $v$ incident to $E$, such that after shifting every cell with $k(v)=M$ down by one rung, the unit-step property still holds on $E$.
background
Phase 56 introduced the forced minimal-distinction invariant UnitStep: across every adjacency in $E$, the integer rung gap lies in ${0,+1,-1}$. A unit recognition step resolves at most one $\varphi$-rung; the live engine maintains this because T-3 descends one rung at a time. Phase 57 wired that law into the runtime cost meter. Phase 58 showed that a blind global claim for the real-valued mean move is false; only a local post-move criterion survives.
Phase 59 (this module) supplies the positive half on the object the cost meter actually charges: the integer field $k:V\to\mathbb{Z}$. The engine does not move integer rungs by real means; it descends a region by exactly one rung when a distinction is forced. The vertices that appear in $E$ are collected as edgeVerts (image of first and second projections). The one-rung descent operator shiftDown lowers $k$ by 1 on a chosen set $S$ and leaves it fixed elsewhere.
Upstream, shiftDown_top_unitStep already proves that when $S$ is the top rung $M$ (an upper bound on all rungs present in $E$), the cut condition discharges for free: a top cell's neighbour must sit exactly one rung below, so after descent the cut gap is $0$.
proof idea
Nonemptiness of $E$ yields a nonempty edgeVerts via the first-projection membership lemma. The image of $k$ on that finite set is therefore nonempty; take $M$ to be its max'. Membership of the max in the image supplies a witness vertex $v$ with $k(v)=M$.
The remaining goal is unit-step after shiftDown of the level set ${k=M}$. Apply the upstream lemma shiftDown_top_unitStep, which needs only that every endpoint of every edge has rung $\le M$. Both endpoints lie in edgeVerts, so each $k$-value is in the image whose maximum is $M$; Finset.le_max' closes both inequalities.
why it matters
This is the existence capstone of Phase 59: a preserving top-rung descent always exists with no externally supplied $M$, and it is nontrivial because the maximum is attained. Together with shiftDown_top_unitStep it answers the open item left by Phases 56/57: the forced top-rung descent keeps UnitStep cycle to cycle, so the Phase-56 graded cost law applies to the next cycle.
The dual raise of the bottom rung and the necessity counterexample (descending a non-top cell on the chain $0,1,2$ breaks unit-step) sit in the same module; this theorem is the constructive positive half. In the broader Recognition chain it backs the integer dynamics that T-3 uses when descending one rung at a time, without appealing to the false global real-valued preservation claim of Phase 58. No downstream consumers are wired yet (used_by is empty), so it is currently a leaf that closes the Phase-59 obligation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.