abs_le_of_between
plain-language theorem explainer
If a signed orbit z lies between −n and n in the internal order, then its absolute value is at most n as a distinction-natural. Order-theory and certificate lemmas cite this direction of the sandwich characterization. The proof is a one-line reverse application of the iff form abs_le_iff_between.
Claim. Let $z$ be a signed orbit and $n$ a distinction-natural. If $-n \le z$ and $z \le n$ in the signed-orbit order (nonnegative difference), then the Boolean comparison $|z| \le n$ holds.
background
In the primitive recognition calculus, integers are built as signed orbits: pairs of finite δ-orbit positions (DistinctionNat) recording positive and negative counts. Absolute value is the absolute difference of those two positions. Negation swaps the two components. The internal order le says $a \le b$ when $b-a$ is nonnegative.
Boolean leq on DistinctionNat is the structural recursive order on orbit positions. Embedding a natural $n$ as a nonnegative signed orbit is ofOrbit n. The sandwich $-n \le z \le n$ is therefore the pair of order facts le (negate (ofOrbit n)) z and le z (ofOrbit n).
The sibling theorem abs_le_iff_between already equates Boolean $|z| \le n$ with that sandwich, via reduction to integer comparison on the underlying toInt embedding.
proof idea
One-line term proof. Apply the reverse direction (.mpr) of abs_le_iff_between z n, packing the two hypotheses into the conjunction that the iff demands. No further case analysis or arithmetic is needed here; all work lives in the iff lemma (rewrite through leq_eq_true_iff and le_iff_toInt_le).
why it matters
This is the convenient introduction form of the absolute-value sandwich: from order bounds one obtains Boolean |z| ≤ n. Downstream, between_mono uses the sandwich shape to enlarge the bound when $n \le m$, and integer_order_certificate packages the closed signed-orbit order surface (display lemmas for truncated subtraction, leq, absDiff, and nonneg). Together these close the integer-order layer of the foundation stack that underwrites later arithmetic and forcing-chain constructions, without yet touching J-cost or the T5–T8 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.