zero_den_toNat
plain-language theorem explainer
The zero ratio-orbit display has denominator whose natural-number reading is exactly 1. Anyone normalizing zero in orbit-based integer or rational arithmetic cites this fact. The proof is a two-step rewrite: the zero display's denominator is succ of zero, and the orbit-to-Nat map sends that to 1.
Claim. If $0_{\mathrm{rat}}$ denotes the zero ratio orbit (integer numerator over a nonzero distinction-orbit denominator), then reading its denominator as a natural number yields $1$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, playing the role of the naturals without assuming Peano axioms up front. 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) is a rational display: a signed-orbit numerator over a nonzero DistinctionNat denominator. The zero ratio orbit is the canonical zero display in that structure; its denominator must be the unit orbit (successor of zero) so that the fraction is well-formed and represents zero.
Upstream arithmetic-from-logic supplies the same successor and toNat pattern on LogicNat; here the orbit module reuses that reading for distinction orbits.
proof idea
Term-mode proof by change-of-goal then rewrite. First show that the claim is (DistinctionNat.succ DistinctionNat.zero).toNat = 1, which is the unfolded denominator of RatioOrbit.zero. Then rewrite with DistinctionNat.toNat_succ and DistinctionNat.toNat_zero, reducing to Nat.succ 0 = 1 by definition.
why it matters
Local scaffolding for the zero element in ratio-orbit arithmetic. Downstream it is used (directly or via simp) in the PRC integer ring laws: zero_add, add_zero, add_negate, negate_add, zero_mul, and mul_zero, each of which reduces integer identities to toInt injectivity plus simplification. Without the denominator of zero reading as 1, those normalizations fail.
In the broader Recognition stack this sits in the foundation layer that builds integers and rationals from distinction orbits before the forcing chain (T0–T8) and the J-cost calculus. It is bookkeeping, not a landmark theorem, but it closes the zero case for K4.7 rational displays so later arithmetic lemmas stay sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.