between_of_abs_le
plain-language theorem explainer
If the absolute value of a signed orbit z is at most a natural orbit position n, then z lies between −n and n in the signed-orbit order. Order-theory and certificate proofs cite it to turn a Boolean bound on |z| into a two-sided inequality. The proof is a one-line application of the forward direction of the absolute-value betweenness equivalence.
Claim. Let $z$ be a signed orbit and $n$ a finite $\delta$-orbit position. If the Boolean comparison $|z| \le n$ holds, then $-n \le z \le n$ in the internal signed-orbit order (i.e. $z$ is nonnegative after subtracting $-n$, and $n-z$ is nonnegative).
background
In the primitive recognition calculus, integers are realized as signed orbits: pairs of finite $\delta$-orbit positions (DistinctionNat) recording positive and negative counts. Absolute value of a signed orbit is the absolute difference of those two positions. Negation swaps the two components. The internal order $a \le b$ means the difference $b-a$ is nonnegative.
Boolean $\le$ on DistinctionNat is defined by structural recursion only (zero is least; successors compare after stripping). The companion equivalence states that $|z| \le n$ (as a Boolean) if and only if $-n \le z$ and $z \le n$ in the signed-orbit order; its proof rewrites through the Boolean-to-Prop bridge and the integer embedding of signed-orbit order.
This module builds the order surface on those signed orbits so that later certificates can treat integer comparison as closed recognition structure rather than an external axiom.
proof idea
One-line term proof: apply the forward (.mp) direction of abs_le_iff_between at $z$ and $n$ to the hypothesis that the Boolean $|z| \le n$ holds. That equivalence already reduces both sides to integer comparisons via leq_eq_true_iff and le_iff_toInt_le, so no further casework is needed here.
why it matters
Feeds between_mono, which widens a betweenness interval when the outer bound increases, and is listed among the display lemmas assembled by integer_order_certificate ("The internal signed-orbit order surface is closed"). Closing that certificate is foundation work: integer order must be native before the forcing chain can treat discrete structure (eight-tick octave, $D=3$) as forced rather than postulated. The lemma is the convenient one-direction form used when a proof already has a Boolean absolute bound and needs the two-sided order statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.