between_mono
plain-language theorem explainer
If a signed orbit z lies between −n and n, and the nonnegative orbit index n is at most m, then z also lies between −m and m. Order-theory and integer-construction proofs cite this to enlarge symmetric bounds without leaving the interval. The argument converts betweenness to an absolute-value inequality, transports it along n ≤ m, and converts back.
Claim. Let $z$ be a signed orbit and let $n,m$ be finite distinction-orbit indices. If $-n \le z \le n$ in the internal signed-orbit order and $n \le m$ holds for the Boolean order on distinction naturals, then $-m \le z \le m$.
background
This lives in the primitive recognition calculus for integer order: signed orbits are the internal model of integers built from finite $\delta$-orbit positions (DistinctionNat) with a sign. The internal order on signed orbits is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative.
Betweenness for a radius $n$ means $-n \le z \le n$, where $\pm n$ are the signed embeddings of the orbit index $n$. Absolute value $z.\mathrm{abs}$ is the underlying nonnegative orbit size. Upstream, abs_le_iff_between (via abs_le_of_between and between_of_abs_le) equates $|z| \le n$ with that two-sided bound. The Boolean leq on distinction naturals is the structural recursive $\le$ on finite orbit positions; abs_le_trans is ordinary transitivity of that order after decoding to Nat.
proof idea
Term-mode composition of three local lemmas. First abs_le_of_between turns the hypothesis $-n \le z \le n$ into $|z| \le n$. Then abs_le_trans with $n \le m$ yields $|z| \le m$. Finally between_of_abs_le converts that absolute inequality back into $-m \le z \le m$. No case splits; the bridge is the abs/between equivalence plus Nat-order transitivity.
why it matters
Closes a monotonicity fact for symmetric integer intervals in the signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate packages display lemmas (truncated subtraction, leq, abs-diff, nonnegativity) that certify the order API is coherent.
In the Recognition foundation stack this is arithmetic scaffolding under the forcing chain, not a T5–T8 physics step: it ensures interval bounds on the integer model expand monotonically, which later supports comparison and truncation lemmas used when integers and rationals are built from recognition orbits. No open sorry remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.