one_den_toNat
plain-language theorem explainer
The unit rational orbit has denominator whose extracted natural is exactly 1. Anyone proving multiplicative unit laws for PRC integers or rationals cites this fact. The proof is a two-line rewrite: the denominator is successor of zero, and the orbit-to-Nat map sends that pair to Nat.succ 0.
Claim. If $1_{\mathrm{rat}}$ denotes the multiplicative unit in the rational-orbit display (signed numerator over a nonzero distinction-orbit denominator), then the natural number read off from its denominator equals $1$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, parallel to Peano naturals but generated from recognition steps rather than posited axioms. The map toNat reads off the iteration count, with the usual simp facts toNat(succ n) = Nat.succ(toNat n) and toNat(zero) = 0.
A RatioOrbit (K4.7) packages a signed orbit numerator with a nonzero distinction-orbit denominator. The unit rational is built so its denominator is exactly one distinction step above zero. This lemma records that structural choice in ordinary Nat language, which is what later arithmetic identities need when they compare denominators after multiplication.
proof idea
Term/tactic hybrid, essentially definitional. First show rewrites the goal to (DistinctionNat.succ DistinctionNat.zero).toNat = 1, exposing that the unit's denominator is successor of zero. Then a single rw applies DistinctionNat.toNat_succ and DistinctionNat.toNat_zero, reducing the left-hand side to Nat.succ 0, which is definitionally 1.
why it matters
Feeds the unit laws for PRC integer multiplication: one_mul, mul_one, and the reciprocal-cancellation lemma mul_recip_cancel₀. Those identities need the denominator of the multiplicative unit to extract as ordinary 1 so that simp and injectivity of the integer readout close. In the broader Recognition stack this sits in the K4 integer/rational layer that builds choice-free arithmetic from distinction orbits, upstream of mass-ladder and forcing-chain material that assumes ordinary ring structure on the extracted numbers. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.