sub_eq
plain-language theorem explainer
On PRC integers, the infix difference a − b is definitionally the named subtraction map sub. Anyone rewriting arithmetic on signed-orbit quotient classes cites this as a simp bridge. The proof is pure reflexivity: the notation is installed as that map.
Claim. For PRC integers $a,b$ (signed-orbit quotient classes), the notation $a - b$ equals the primitive subtraction operation $\mathrm{sub}(a,b)$.
background
Primitive Recognition Calculus builds integers before classical $\mathbb{Z}$. PRCInt is the type of signed-orbit quotient classes: orbits under the internal balanced-length relation, with a later verifier map into ordinary integers.
Subtraction on that type is introduced both as a named operation sub and via the standard infix -. Downstream arithmetic (absolute difference, order, and the passage to rationals and Cauchy reals) needs the two spellings to be interchangeable under simp.
The local module sits in the Foundation layer that constructs PRC integers and rationals from orbit data, importing orbit arithmetic and Mathlib only as scaffolding for the classical display maps.
proof idea
One-line definitional equality. The proof is rfl: the notation HSub.hSub (infix -) on PRCInt is defined to be exactly sub, so both sides reduce to the same term and reflexivity closes the goal. The @[simp] attribute makes the rewrite available automatically.
why it matters
Tiny but load-bearing notation glue. Downstream Cauchy-real material rewrites differences of PRC numbers when relating order and square-gap displays to classical rationals; the rational twin of this lemma appears explicitly in lt_iff_toRat_lt and PRCSquareGap_toRat (rw/simp on sub_eq before toRat_sub).
In the Recognition stack this keeps the K4.8 integer layer aligned with ordinary algebraic notation while the underlying objects remain signed-orbit quotients, so later forcing and continuum constructions never fork between "notation minus" and "primitive sub".
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.