abs_le_trans
plain-language theorem explainer
If the absolute value of a signed orbit is at most n in the Boolean orbit-position order, and n is at most m, then the absolute value is at most m. Anyone building interval or truncation arguments on signed orbits cites this. The proof rewrites the Boolean order to ordinary Nat inequality and applies Nat transitivity.
Claim. Let $z$ be a signed orbit (pair of finite $\delta$-orbit positions, read as $\mathrm{pos}-\mathrm{neg}$) and let $n,m$ be finite $\delta$-orbit positions. If the Boolean order holds for $|z|\le n$ and for $n\le m$, then it holds for $|z|\le m$.
background
In the primitive recognition calculus, finite $\delta$-orbit positions are the type DistinctionNat, ordered by a Boolean predicate built by structural recursion only (true on zero in the left slot, false when a successor meets zero, and recursive on successors). That Boolean order is proved equivalent to the verifier Nat order via a choice-free structural induction (axiom footprint [propext]).
A signed orbit is a pair of such positions, intended as $\mathrm{pos}-\mathrm{neg}$. Its absolute value is the absolute difference of the two legs, again an orbit position. The local module develops the order surface on these signed objects: reflexivity, transitivity, totality, trichotomy, and sign-flag characterizations.
Upstream, ordinary Nat (and logic-nat) transitivity is already available; the Boolean-to-Nat bridge is the only non-trivial interface this lemma needs.
proof idea
Term-mode, two steps. Rewrite both hypotheses and the goal with the Boolean-order bridge (leq a b = true iff a.toNat \le b.toNat). The goal becomes ordinary Nat inequality on the absolute value and on $m$; discharge it by Nat.le_trans on the rewritten hypotheses. No case analysis on signs or on the orbit constructors.
why it matters
Closes a small but necessary monotonicity fact for absolute values under the internal Boolean order. Downstream, between_mono uses it to enlarge a two-sided bound: if $z$ lies between $-n$ and $n$ and $n\le m$, then $z$ lies between $-m$ and $m$. The same fact is wired into integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, Boolean order, absolute difference, and nonnegativity flags).
In the Recognition foundation stack this sits under arithmetic-from-logic and the primitive recognition calculus: integers are reconstructed as signed orbit differences before any classical Int API is assumed. It is not itself a forcing-chain landmark (T5–T8), but it is part of the certified integer-order layer those later constructions rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.