one_eq
plain-language theorem explainer
Numeral 1 on PRC integers is definitionally the named unit constant. Anyone normalizing arithmetic or simp-rewriting in the K4.8 integer layer cites this. The proof is pure reflexivity: OfNat and the explicit one constructor unfold to the same quotient class.
Claim. In the type of PRC integers (signed-orbit quotient classes), the numeral $1$ equals the named multiplicative unit element.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation. A signed orbit carries a positive and a negative orbit display; the verifier map sends it to $\mathbb{Z}$ by $\mathrm{toInt}(z)=z_{\mathrm{pos}}-z_{\mathrm{neg}}$ in natural-number coordinates. The type is introduced as K4.8 scaffolding toward a ring structure whose display into $\mathbb{Z}$ is a homomorphism.
The module builds integers and rationals inside Primitive Recognition Calculus before real completion. Sibling material defines zero, the signed-orbit constructor, and the display toInt. The named constant one is the unit class; Lean also supplies the numeral via OfNat. This lemma ties those two presentations together so simp and ring tactics see a single object.
proof idea
Term proof by rfl. After unfolding the OfNat instance for PRCInt and the definition of the named unit, both sides are the same quotient representative, so definitional equality closes the goal. No lemmas are applied.
why it matters
K4.8 constructs integers as signed-orbit classes and aims at a ring whose verifier display is a homomorphism into $\mathbb{Z}$. Aligning numeral $1$ with the named unit is the bookkeeping step that lets additive and multiplicative simp sets fire cleanly when proving that display preserves structure.
No downstream dependents are recorded yet; the immediate neighborhood is the additive ring-homomorphism claim for toInt and the parallel rational construction PRCRat. In the broader Recognition stack this sits under the foundation forcing path that recovers discrete arithmetic before continuum and physical constants, not yet at T5–T8 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.