instOne
plain-language theorem explainer
Primitive recognition calculus integers carry a multiplicative unit via Mathlib's One typeclass, witnessed by the canonical one of the signed-orbit quotient. Anyone assembling monoid, group, or ring structure on PRC integers cites this instance for the notation 1. The declaration is a one-line typeclass witness pointing at the existing one value.
Claim. The type of primitive recognition calculus integers (equivalence classes of signed orbits under the balanced-length relation) is equipped with a distinguished element $1$, i.e. it carries an instance of the multiplicative-unit typeclass.
background
In the primitive recognition calculus, integers are not postulated as $\mathbb{Z}$. They are built as PRCInt, the quotient of signed orbits by an internal balanced-length setoid (K4.8). The map that displays these classes as ordinary integers is a separate, downstream theorem; algebra is developed on the quotient first.
Mathlib's One typeclass supplies the field one and the notation $1$. Parallel structure exists for rationals (PRCRat: nonzero-denominator ratio-orbit quotients identified by cross-multiplication). The surrounding module also defines zero, signed-orbit constructors, and comparison helpers on the same quotient.
Local setting: IntegerRational develops the integer and rational layers of the recognition calculus from orbit arithmetic, before completeness and continuity results that target the reals.
proof idea
One-line instance: the existing value one in the PRCInt namespace is packaged as One.one. No algebraic laws are proved here; the declaration only registers the unit element for typeclass search and notation.
why it matters
Algebraic structure on recognition-native integers is a prerequisite for the foundation stack that later forces the J-cost, $\varphi$, the eight-tick octave, and $D=3$ (T5–T8). Without a registered unit, monoid and ring instances cannot form, and the integer ladder used in mass and constant formulas has no multiplicative identity in-type.
No downstream theorems currently list this instance as a direct edge, so its role is infrastructural: it closes the One slot so later arithmetic lemmas can write $1$ rather than a raw constructor. It sits beside the zero instance and the signed-orbit display theorems in the same K4.8 block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.