toInt_sub
plain-language theorem explainer
Subtraction of primitive-recognition integers is compatible with the integer display: the display of a difference equals the ordinary difference of the displays. Anyone proving ring or arithmetic lemmas on the signed-orbit quotient would cite it. The proof unfolds subtraction as addition of a negation, rewrites by the add and negate display lemmas, and finishes with ring on ℤ.
Claim. For primitive-recognition integers $a,b$ (classes of signed orbits under the balanced-length relation), the verifier map into $\mathbb{Z}$ sends the difference $a-b$ to the ordinary integer difference of the images.
background
Primitive-recognition integers are the quotient of signed orbits by the internal balanced-length relation (K4.8). A signed orbit has positive and negative orbit components; its verifier display into $\mathbb{Z}$ is the difference of those components' natural lengths. The same display lifts to the quotient.
Subtraction on the quotient is not primitive: it is addition of the pointwise negation that swaps the two components. Companion results already show that the display preserves addition and negation, so the subtraction case is a short consequence.
The local setting is the Primitive Recognition Calculus integer/rational layer: orbit arithmetic is being packaged into a usable integer type before later foundation steps.
proof idea
Rewrite the goal by unfolding subtraction as $\mathrm{add},a,(\mathrm{negate},b)$. Apply the two display lemmas for addition and negation on the quotient. The resulting equality on $\mathbb{Z}$ is $a_{\mathbb{Z}}+(-b_{\mathbb{Z}})=a_{\mathbb{Z}}-b_{\mathbb{Z}}$, which ring closes. Term-mode proof; no induction on the quotient is needed here because the add and negate lemmas already discharge the quotient structure.
why it matters
This is infrastructure for the ring-axiom block on primitive-recognition integers that begins immediately after the proof. It makes the verifier map $\mathrm{PRCInt}\to\mathbb{Z}$ a homomorphism for subtraction, so later arithmetic, order, and comparison results can move between the internal quotient and ordinary integers without ad-hoc casework.
No recorded downstream consumers yet; the lemma is a building block rather than a leaf of the forcing chain. It does not invoke T5–T8, the Recognition Composition Law, or $\varphi$, but it supplies part of the integer substrate those later steps assume when they count ticks, rungs, or dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.