add_le_add
plain-language theorem explainer
Addition on signed orbits is monotone: if a ≤ b and c ≤ d then a+c ≤ b+d. Anyone building order-compatible arithmetic on the integer layer (cost bounds, defect distances, order certificates) cites this. The proof transports both inequalities to ℤ via the toInt bridge, rewrites sums, and closes with omega.
Claim. Let $a,b,c,d$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $a\le b$ and $c\le d$ in the internal order (nonnegative difference), then $a+c\le b+d$.
background
Signed orbits are the integer layer of the primitive recognition calculus: a structure with nonnegative distinction-nat components pos and neg, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Their internal order is defined by nonnegative difference: $a\le b$ means $\mathrm{sub},b,a$ is nonnegative.
That order is equivalent to the standard order on the integer image: $a\le b$ if and only if $a.\mathrm{toInt}\le b.\mathrm{toInt}$. Addition is compatible with that image: $(\mathrm{add},a,b).\mathrm{toInt}=a.\mathrm{toInt}+b.\mathrm{toInt}$. Upstream, the LogicNat order is the usual existential-witness form $n\le m\Leftrightarrow\exists k,,n+k=m$; the signed-orbit layer lifts the same arithmetic to differences.
This module closes the order surface on that integer layer (reflexivity, transitivity, totality, trichotomy, and the present monotonicity facts).
proof idea
Term-mode, three steps. Rewrite both hypotheses and the goal with le_iff_toInt_le, so everything is an inequality of integers. Rewrite the two sums with add_toInt, obtaining $a.\mathrm{toInt}+c.\mathrm{toInt}\le b.\mathrm{toInt}+d.\mathrm{toInt}$. Finish by omega, which discharges ordinary integer addition-monotonicity.
why it matters
This is a basic order-arithmetic lemma on the signed-orbit integer layer. It is listed among the facts that close the internal order surface in integer_order_certificate.
Downstream it is used wherever monotone addition of integer-valued costs or residuals is needed: the local quasi-triangle bound for defect distance (CostAlgebra, Prop. 2.6), the tick-work bound in cosmology (tickWork_le: a tick costs at most $2P$), choice-free transitivity of regular-sequence equivalence in the Grow/Eta completion path, and several gravity residual and recognition-ratio estimates. In the RS foundation stack it sits under the arithmetic-from-logic build that later supports the forcing chain and cost algebra, not as a T0–T8 step itself but as plumbing those steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.