instSub
plain-language theorem explainer
Registers subtraction on PRC integers so the type carries Lean's Sub instance. Anyone writing arithmetic on signed-orbit quotient classes cites this to use the `-` notation. The body is a one-line structure instance that packages the already-defined subtraction operation.
Claim. The type of PRC integers (signed-orbit quotient classes under the balanced-length relation) carries a subtraction operation, making $(PRC\mathbb{Z}, -)$ an instance of the abstract subtraction structure.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation (K4.8). The verifier map into ordinary $\mathbb{Z}$ is a later theorem; arithmetic is developed first on the quotient itself.
The surrounding module builds integer and rational structure from primitive recognition orbits: signed orbits give integers, ratio orbits with nonzero denominator give rationals. Sibling operations include truncated subtraction, absolute difference, and the order predicate used to define them.
This instance sits in the IntegerRational layer of the Primitive Recognition Calculus, after orbit arithmetic and before the rational quotient is fully equipped.
proof idea
One-line instance: the Sub structure is inhabited by the already-constructed subtraction map on PRCInt. No further proof obligations; Lean only needs the field of type PRCInt → PRCInt → PRCInt.
why it matters
Without a Sub instance, downstream arithmetic (differences of rung indices, signed gaps on the phi-ladder, integer parts of recognition counts) cannot use standard notation or typeclass-driven lemmas. The declaration closes the basic ring-like interface on PRC integers so later modules can treat them as ordinary additive objects while remaining inside the orbit-quotient semantics of Recognition Science foundation work.
No direct used-by edges are recorded yet; the instance is infrastructure for any proof that subtracts PRC integers rather than a step in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.