abs_le_iff_between
plain-language theorem explainer
Absolute value of a signed orbit is at most a distinction natural n exactly when the orbit lies between -n and n. Order-theory and integer-arithmetic proofs in the primitive recognition calculus cite this bridge. The argument rewrites both sides through the Int recovery map, then splits on the sign of z and finishes with omega.
Claim. For a signed orbit $z$ and a distinction natural $n$, $|z| \le n$ if and only if $-n \le z \le n$, where absolute value and order are the internal signed-orbit operations and $\le$ on the right-hand side is the nonnegative-difference order.
background
In the primitive recognition calculus, integers appear as signed orbits: pairs of distinction naturals (positive and negative legs) quotiented to a balanced representative. Absolute value of a signed orbit is the distinction-natural absolute difference of those legs; embedding a distinction natural $n$ as a nonnegative signed orbit is ofOrbit, and negation flips the legs.
Order on signed orbits is defined by nonnegative difference: $a \le b$ when $b-a$ is nonnegative. Distinction-natural comparison leq is the Boolean surface of the underlying natural order. Both surfaces are tied to classical Int by recovery maps: toInt on signed orbits and toNat on distinction naturals, with abs_toNat stating that internal absolute value displays as Int.natAbs.
The local module closes the integer-order surface: reflexivity, totality, trichotomy, and the usual absolute-value sandwich identities. This lemma is the iff form of that sandwich.
proof idea
Rewrite the Boolean leq via leq_eq_true_iff and both signed-orbit inequalities via le_iff_toInt_le. Simplify with negate_toInt, ofOrbit_toInt, and abs_toNat, reducing the claim to Int.natAbs(z.toInt) \le n.toNat iff -n.toNat \le z.toInt \le n.toNat.
Forward direction: cast the natural inequality to Int, then case on whether z.toInt \ge 0. Nonnegative case uses ofNat_natAbs_of_nonneg; nonpositive case uses ofNat_natAbs_of_nonpos. Each branch closes by omega.
Converse: unpack the two bounds, again case on the sign of z.toInt, rebuild natAbs from the matching identity, and omega yields the absolute-value bound; cast back to the natural comparison.
why it matters
This is the core sandwich equivalence for absolute value in the internal integer order. Downstream one-liners between_of_abs_le and abs_le_of_between are the two directions; neg_abs_le_self and self_le_abs instantiate it at $n = |z|$ to get $-|z| \le z \le |z|$.
Those facts feed the closed integer_order_certificate, which packages display lemmas for truncated subtraction, leq, absolute difference, and signed nonnegativity. In the Recognition foundation stack this sits under arithmetic-from-logic and integers-from-logic: once order and absolute value agree with classical Int, later forcing-chain and mass-ladder constructions can treat integer comparisons as already certified rather than axiomatic.
No open scaffold remains here; the claim is fully proved and only re-exported by the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.