den_cast_ne_zero
plain-language theorem explainer
For any ratio orbit, the denominator's natural-number readout is nonzero when cast into the verifier rationals. Anyone proving that orbit arithmetic matches field operations on ℚ cites this to justify division and field_simp. The proof is a one-line modular cast of the already-proved Nat nonzeroness of the denominator.
Claim. If $q$ is a rational orbit display (signed-orbit numerator over a nonzero distinction-nat denominator), then the cast $(q.\mathrm{den}.\mathrm{toNat}:\mathbb{Q})$ is nonzero.
background
In the Primitive Recognition Calculus, rationals are not taken as primitive. A RatioOrbit (K4.7) is an integer numerator packaged as a signed orbit together with a denominator that is a distinction-nat forced nonzero by a structure field. The verifier map toNat reads an orbit as an ordinary Lean natural by counting successor steps from zero.
The companion lemma den_toNat_ne_zero already shows that this natural readout of the denominator cannot be zero: if it were, transporting along ofNat/toNat would collapse the denominator to the zero distinction-nat, contradicting the structure hypothesis. The present statement lifts that fact one type level, into the rationals used by the display map toRat.
Local setting is the IntegerRational layer: building a field-like arithmetic on ratio orbits whose verifier images recover ordinary rational arithmetic.
proof idea
One-line wrapper. Apply exact_mod_cast to q.den_toNat_ne_zero, which already gives q.den.toNat ≠ 0 in Nat. Modular cast transports the inequality across the coercion Nat → ℚ, yielding (q.den.toNat : ℚ) ≠ 0.
why it matters
Every homomorphism lemma that compares ratio-orbit operations to rational field operations needs a nonzero denominator in ℚ before it can unfold toRat and run field_simp or cancel. Downstream consumers include add_toRat, mul_toRat, negate_toRat, recipNonzero_toRat, and crossEq_iff_toRat_eq (K4.10: cross-multiplication agrees with rational equality of verifier displays), plus normalizeRatio_toRat in the Euclidean layer and the signed-ratio decomposition target in PRC native cost uniqueness.
This is bookkeeping on the path from orbit arithmetic to a genuine rational field display. It does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law, but it is required scaffolding for any later identification of ratio coordinates with the cost-theoretic ratio used in CPT factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.