zero_num_toInt
plain-language theorem explainer
The numerator of the zero ratio-orbit displays as the integer 0 under the signed-orbit verifier map. Anyone proving PRC integer or rational arithmetic identities via the toInt hub cites this as a simp fact. The proof is a one-line wrapper of the signed-orbit zero display lemma.
Claim. If $z_0$ is the zero ratio-orbit (integer numerator over a nonzero orbit denominator), then the integer display of its numerator equals $0$.
background
In the Primitive Recognition Calculus integer/rational layer, a signed orbit is a difference of two distinction naturals (intended meaning pos minus neg). Its verifier map toInt sends that pair to the ordinary integer difference of their Nat displays.
A ratio-orbit packages a signed-orbit numerator with a nonzero distinction-Nat denominator. The zero ratio-orbit is the canonical zero display in that structure; its numerator is the zero signed orbit.
The local module builds PRC rationals as the quotient of ratio-orbits by cross-multiplication equivalence, and proves field-style laws choice-free by reducing through the integer cross-multiplication hub rather than through classical ℚ.
proof idea
One-line wrapper: the goal is definitionally the statement that the zero signed orbit displays as integer 0, which is exactly SignedOrbit.zero_toInt (itself a rfl simp lemma on the difference of two zero Nats).
why it matters
This private display fact sits under the PRC integer arithmetic suite. Downstream consumers include zero_add, add_zero, add_negate, negate_add, zero_mul, mul_zero, and the reciprocal-cancellation path mul_recip_cancel₀. Those proofs typically apply toInt_injective and close by simp; without the numerator-of-zero fact, the integer identities do not fire.
In the broader Recognition foundation, ratio-orbits and signed orbits are the constructive integer/rational layer forced before cost calculus and the forcing chain (T0–T8). Keeping zero's integer display on the {propext, Quot.sound} basis supports the choice-free field laws for PRC rationals described in the module section on cross-multiplication proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.