neg_abs_le_self
plain-language theorem explainer
For every signed orbit z one has −|z| ≤ z in the internal signed-orbit order. Anyone assembling the integer-order certificate or proving sandwich bounds around absolute value will cite it. The argument is a one-line projection: reflexivity of |z| ≤ |z| plus the absolute-value sandwich equivalence yields the left half of −|z| ≤ z ≤ |z|.
Claim. For every signed orbit $z$, $-|z| \leq z$ in the internal order (nonnegative difference).
background
Signed orbits are the RS-native integers: each carries a positive and negative distinction count, with absolute value |z| the orbit-position absDiff of those counts, and negation swapping the two sides. The internal order a ≤ b means the difference b − a is nonnegative.
The key upstream fact is the sandwich characterization: |z| ≤ n (as a Boolean leq on distinction naturals) if and only if −n ≤ z and z ≤ n. Distinction-natural leq is the usual non-strict order, so reflexivity |z| ≤ |z| is immediate from Nat.le_refl.
This module builds the ordered-integer surface from primitive recognition calculus, before rationals and the forcing chain.
proof idea
Apply the sandwich equivalence abs_le_iff_between at n = |z|. The hypothesis |z| ≤ |z| is obtained by turning Nat.le_refl into a true leq via leq_eq_true_iff. The forward direction of the sandwich then gives the pair −|z| ≤ z and z ≤ |z|; project to the first conjunct. Pure term-mode, no tactics.
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (displays for truncated subtraction, leq, abs-diff, and nonnegativity). Without −|z| ≤ z, the absolute-value sandwich is incomplete and the certificate cannot assert that the order behaves like ℤ.
In the broader foundation this is ordinary ordered-integer hygiene: the phi-ladder, mass formula, and later forcing steps (T5–T8) sit on top of a trustworthy integer order. The lemma itself is not a physics claim; it is infrastructure that keeps the Recognition arithmetic layer free of order gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.