instAdd
plain-language theorem explainer
Equips PRC integers (signed-orbit quotient classes) with Mathlib addition by packaging the preexisting orbit-level add. Anyone writing arithmetic or ring structure on the primitive recognition calculus integers cites this. One-line typeclass instance: no new mathematics, only the Add wiring.
Claim. The type of PRC integers (quotient of signed orbits by the balanced-length relation) carries an addition operation, namely the lift of signed-orbit addition through that quotient.
background
In the Primitive Recognition Calculus, integers are not postulated as $\mathbb{Z}$. They are constructed as PRCInt: the quotient of signed orbits by an internal balanced-length setoid. The verifier map into ordinary $\mathbb{Z}$ is a later theorem; the native object is the quotient class.
Addition is defined first on signed-orbit representatives (in the orbit-arithmetic layer), then descended to the quotient. This declaration does not redefine that operation. It only registers it under Mathlib's Add typeclass so that + notation and generic additive lemmas apply to PRC integers.
The sibling rational type PRCRat is built analogously as a ratio-orbit quotient; integer addition is a prerequisite for the integer and rational arithmetic stack in this module.
proof idea
One-line typeclass instance. The body is ⟨add⟩: the preexisting add on PRCInt is supplied as the Add.add field. No tactics, no lemmas, no quotient induction at this site.
why it matters
Part of the K4.8 integer/rational construction inside Primitive Recognition Calculus. Without an Add instance, downstream additive notation, AddCommMonoid/Ring instances, and the path from signed orbits to rationals cannot use standard Mathlib interfaces.
No direct used_by edges are recorded for this instance itself; it is infrastructure for the arithmetic layer that supports later completeness and continuity results on PRC reals. It does not touch the forcing chain (T5–T8), RCL, or physical constants; it is pure foundation scaffolding for native integer arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.