leQ_add_right
plain-language theorem explainer
Right-addition preserves the cross-multiplication order on ratio orbits: if p is at most q, then p+r is at most q+r. Ordered-arithmetic builders on the choice-free rational layer cite this for translation invariance. The proof bridges the order to ordinary integer comparison via a choice-free toInt map, multiplies the nonnegativity witness by a denominator square, and finishes by ring.
Claim. Let $p$, $q$, and $r$ be ratio orbits. If $p \le q$ in the cross-multiplication order, then $p+r \le q+r$ in the same order.
background
Ratio orbits are the delta-native stand-in for rationals in the Primitive Recognition Calculus grow layer: each pairs a signed numerator orbit with a positive denominator distinction. The cross-multiplication order declares $p \le q$ when the signed product of $p$'s numerator with $q$'s denominator is at most that of $q$'s numerator with $p$'s denominator (denominators cast in as positive signed orbits).
The module is deliberately choice-free. Integer comparison is routed through an explicit pos/neg Nat-cast difference (toInt) and a CF Nat bridge, never through choice-tainted signed-orbit order lemmas. Upstream, addition and multiplication of signed orbits commute with toInt, and the logic-nat multiplication recovery theorem says the forward iteration-count map sends LogicNat products to ordinary Nat products.
Local setting (module doc): choice-free unfold of toInt to its pos/neg Nat-cast difference, the substrate for ordered arithmetic without classical choice.
proof idea
Unfold the cross-multiplication order on both the hypothesis and the goal, then rewrite through the private choice-free bridge equating signed-orbit order with ordinary $\mathbb{Z}$ order on toInt. Expand ratio-orbit addition and simplify with the toInt homomorphism facts for signed multiplication, ofOrbit, scale-by-Nat, and addition, plus the logic-nat multiplication recovery. After push_cast, rewrite both sides as nonnegativity of an integer difference. The denominator of $r$ yields a square that is nonnegative in $\mathbb{Z}$; multiply the original nonnegativity witness by that square and finish by convert plus ring rearrangement of the two sides.
why it matters
Translation invariance under addition is the first algebraic compatibility the ordered ratio layer needs before it can support field-like reasoning higher in the stack. The declaration lives in Foundation.PrimitiveRecognitionCalculus.Grow and hardens choice-free ordered rationals built from pure distinction orbits. No downstream consumers are wired yet, so this is infrastructure: later monotonicity, ordered-field, and comparison lemmas that eventually feed mass-ladder and constant-forcing arguments will rest on it. It does not itself name a T0–T8 forcing step, the Recognition Composition Law, or J-cost uniqueness; it closes a concrete piece of the arithmetic substrate those landmarks presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.