instMul
plain-language theorem explainer
Registers multiplication on PRC integers (signed-orbit quotient classes) by packaging the existing orbit-level product as the Lean Mul instance. Anyone assembling monoid, group, or ring structure on the primitive-recognition integers cites this. Pure definitional instance: one constructor application, no proof obligations.
Claim. The type of PRC integers (equivalence classes of signed orbits under the balanced-length relation) carries a binary multiplication operation, given by the already-defined product on signed-orbit representatives.
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 doc-comment states: "PRC integers as signed-orbit quotient classes. The quotient is taken by the internal balanced-length relation; the verifier display into $\mathbb{Z}$ is a downstream theorem."
Multiplication must therefore be defined at the orbit level and shown (elsewhere) to descend to the quotient. This module sits in the foundation layer that builds integer and rational arithmetic from recognition orbits before completeness and continuity results produce the reals.
Sibling material in the same file supplies zero, signed-orbit constructors, and comparison primitives (leq, absDiff, truncated subtraction). The companion type PRCRat is the analogous quotient for ratio orbits with nonzero denominator.
proof idea
One-line definitional instance. The body is ⟨mul⟩: it feeds a pre-existing mul operation on PRCInt into the single field of the Mul typeclass. No tactics, no lemmas, no well-definedness proof at this site; those obligations live on the definition of mul itself.
why it matters
Without a Mul instance, later algebraic structure (semigroup, monoid, ring) cannot be stated in idiomatic Lean on PRCInt. This declaration is pure scaffolding for the K4.8 integer/rational layer of the Primitive Recognition Calculus: it lets orbit-derived integers participate in the same multiplicative notation used for ordinary $\mathbb{Z}$.
Downstream consumers are not yet wired in this graph (used_by is empty), but the parallel PRCRat construction and the real-completeness / product-continuity modules that mention PRCRat indicate the intended path: integer multiplication, then rational multiplication, then continuous extension to reals. In the broader Recognition forcing chain this is pre-physics bookkeeping, not a T5–T8 step; it equips the discrete arithmetic that later supports the $\phi$-ladder and cost calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.