sub
plain-language theorem explainer
Subtraction of signed orbits is defined by adding the first argument to the pointwise negation of the second. Anyone assembling integer arithmetic on distinction-orbit displays cites this. The body is a one-line composition of addition with component swap.
Claim. For signed orbits $a,b$ (each a pair of distinction naturals read as positive part minus negative part), the difference is $a-b:=a+(-b)$, where negation swaps the two components.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals (pos, neg) whose intended meaning is the difference pos - neg (K4.6). These displays are the raw carriers before quotienting to PRC integers by the balanced-length relation.
Pointwise negation swaps the two components: negate a has positive part equal to a.neg and negative part equal to a.pos. Addition of signed orbits is the companion binary operation already defined in the same module; together they give the usual group-law skeleton on displays.
The surrounding module builds PRC integers and rationals as quotients of signed and ratio orbits. Subtraction is introduced at the display level so that the quotient constructions inherit a difference operation once well-definedness is proved.
proof idea
One-line definitional wrapper: sub a b is definitionally add a (negate b). No lemmas are applied; the meaning is entirely by composition of the already-defined addition and the component-swap negation.
why it matters
This is the display-level difference needed before PRC integers (signed-orbit quotients by balanced length) and, downstream, PRC rationals can carry a full arithmetic signature. It sits in the K4.6–K4.8 layer that turns orbit displays into integer and rational types with a verifier map into classical $\mathbb{Z}$.
No parent theorem currently depends on it in the graph (used_by is empty), so its role is infrastructural: it closes the additive groupoid interface on signed orbits so later well-definedness and homomorphism proofs have a named subtraction to quote. It does not itself touch the forcing chain (T0–T8), the J-cost, or physical constants; it is pure carrier arithmetic for the recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.