one_num_toInt
plain-language theorem explainer
The multiplicative unit of the rational orbit display has numerator whose integer readout is exactly 1. Anyone proving unit laws for PRC rationals or integers cites this identity. The argument is a one-line wrapper of the signed-orbit unit readout.
Claim. If $1_{\mathrm{rat}}$ denotes the multiplicative unit of the rational orbit display (numerator a signed orbit, denominator a nonzero distinction count), then the integer readout of its numerator equals $1\in\mathbb{Z}$.
background
In the primitive recognition calculus, integers are recovered from signed orbit differences. A signed orbit is a pair of distinction counts (pos, neg) with intended meaning pos - neg; its verifier map toInt sends it to (pos.toNat : ℤ) - (neg.toNat : ℤ). The unit signed orbit therefore reads out as 1.
A rational orbit display packages an integer numerator (a signed orbit) over a nonzero distinction-count denominator. The multiplicative unit of that display is built so its numerator is precisely the signed-orbit unit. This lemma records that fact at the integer readout layer, tying the rational unit back to the already-proved signed-orbit identity one.toInt = 1.
The surrounding module constructs integers and rationals from orbit arithmetic forced by the recognition calculus, rather than importing ℤ/ℚ as primitives.
proof idea
One-line wrapper: the goal is definitionally the signed-orbit statement that the unit signed orbit reads out as 1, so the proof is just an application of SignedOrbit.one_toInt (itself a rfl simp lemma on the unit constructor).
why it matters
Unit laws for PRC integer multiplication need the numerator of the rational/integer unit to evaluate to 1 under toInt. Downstream, one_mul and mul_one reduce via toInt_injective and simp, and mul_recip_cancel₀ likewise needs the unit numerator readout. Without this bridge, the rational display unit would not connect to ordinary integer arithmetic.
In the Recognition Science foundation stack this sits inside the construction of integers and rationals from forced orbit structure (the path that later supports the forcing chain and native constants). It is bookkeeping rather than a new physical claim, but it closes the unit case cleanly so later arithmetic lemmas stay simp-driven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.