self_le_abs
plain-language theorem explainer
For any signed orbit z, z sits at most at its absolute value once that absolute value is re-embedded as a nonnegative signed orbit. Builders of the integer order layer from recognition primitives cite this as the standard upper bound |z| ≥ z. The proof is a short term extraction: reflexivity of natural order on |z| feeds the betweenness characterization of absolute value, and the right conjunct is projected.
Claim. For every signed orbit $z$, $z \le |z|$, where $|z|$ denotes the nonnegative signed orbit obtained by embedding the absolute orbit position of $z$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: each carries a positive and a negative distinction count. Absolute value returns the orbit position absDiff of those two counts, a bare DistinctionNat. The order on signed orbits is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative.
A companion lemma characterizes absolute value by betweenness: the natural comparison $|z| \le n$ holds if and only if $-n \le z \le n$ in the signed-orbit order. Natural order itself is the usual existential-witness order on LogicNat/DistinctionNat, with the standard reflexivity fact $n \le n$.
This module assembles the order surface (reflexivity, totality, trichotomy, sign flags) needed before the integer layer can be certified closed.
proof idea
Term-mode, two steps. First apply the reverse direction of the natural-order display leq_eq_true_iff at $(|z|,|z|)$ to the ordinary Nat.le_refl, obtaining $|z| \le |z|$ as a Boolean-true fact. Feed that into the forward direction of abs_le_iff_between at $(z,|z|)$, which yields the conjunction $-|z| \le z \land z \le |z|$. Project the second conjunct. No induction and no case split on the sign of $z$.
why it matters
The parent consumer is integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas (truncated subtraction, natural leq, absolute difference, signed nonnegativity and its flag) so downstream arithmetic can treat the signed-orbit order as a finished interface rather than an open construction.
Within the Recognition foundation stack this sits below the forcing chain (T0–T8) and the Recognition Composition Law: it is pure integer-order hygiene needed before mass ladders, eight-tick structure, or dimensional forcing can talk about signed quantities. It does not itself force $\varphi$ or $D=3$; it only guarantees the elementary bound $z \le |z|$ inside the primitive calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.