den_toNat_ne_zero
plain-language theorem explainer
For any rational orbit display, the verifier natural number of the denominator is nonzero. Anyone building mediants, cross-multiplication orders, or reciprocal flags on RatioOrbit cites this bridge from the structure field den ≠ zero to Nat. The proof is a short contradiction: ofNat/toNat round-trip plus ofNat 0 = zero recovers the structure hypothesis.
Claim. Let $q$ be a rational orbit (signed-orbit numerator over a nonzero distinction-orbit denominator). Then the verifier natural number of the denominator satisfies $\mathrm{toNat}(q.\mathrm{den}) \neq 0$.
background
RatioOrbit (K4.7) is the primitive rational display in the recognition calculus: a SignedOrbit numerator over a DistinctionNat denominator, with a structure field asserting the denominator is not the zero orbit. DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and succ). The map toNat reads off the iteration count as an ordinary Nat; ofNat builds the orbit back from a verifier Nat, with ofNat 0 = zero and ofNat (toNat d) = d.
The module sits in PrimitiveRecognitionCalculus.IntegerRational, where rationals are kept as orbit pairs and equality/order are expressed by integer cross-multiplication rather than a classical ℚ display. The nonzero-denominator invariant must therefore be available both at the orbit level and at the Nat level used by Int bridges and cancellation lemmas.
proof idea
Contradiction on the Nat claim. Assume q.den.toNat = 0. Congruence under DistinctionNat.ofNat yields ofNat (q.den.toNat) = ofNat 0. Rewrite with ofNat_toNat and ofNat_zero to obtain q.den = DistinctionNat.zero. Discharge by the structure field q.den_ne_zero. No arithmetic beyond the ofNat/toNat round-trip is used.
why it matters
Every RatioOrbit construction that needs a positive Nat denominator routes through this lemma. Downstream, mediant uses it to prove the sum of two denominators is nonzero; leQ_trans and crossEq_trans cancel middle denominators after the Int bridge; den_cast_ne_zero and isZero inherit the Nat fact; IntegerOrder reciprocal-flag theorems and the choice-free equiv_trans triangle for regular sequences also depend on it.
In the Recognition stack this is bookkeeping under K4.7, not a forcing-chain step (T5–T8). It keeps rational orbit arithmetic on {propext, Quot.sound} by ensuring denominators stay nonzero before any cross-product cancellation, so later density and order results never smuggle Classical.choice via a ℚ display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.