remainder_toNat
plain-language theorem explainer
Object-level remainder on distinction orbits agrees with ordinary natural-number modulus under the verifier step-count map. Anyone moving Euclidean arithmetic from pure recognition orbits to Nat cites this bridge. The proof is a one-line projection of the second conjunct of the paired quotient-remainder transport theorem.
Claim. For finite distinction orbits $n$ and $d$ with $d$ nonzero, if $r$ is the object-level remainder of $n$ by $d$, then the verifier step-count of $r$ equals the ordinary modulus of the step-counts: $\mathrm{count}(r) = \mathrm{count}(n) \bmod \mathrm{count}(d)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive zero/successor type standing for pure recognition counts before any radix is fixed. Its verifier map reads each orbit as an ordinary natural by counting successor steps.
This module equips those orbits with Euclidean division. Object-level remainder is the second component of the native divMod pair. Upstream, the paired transport theorem already asserts that both quotient and remainder map to ordinary Nat division and modulus: "Euclidean quotient/remainder transports to verifier Nat division and modulus."
The local setting is Primitive Recognition Calculus arithmetic reconstructed from distinction alone, prior to signed or rational orbits.
proof idea
One-line wrapper. Apply the paired transport theorem on the same dividend, divisor, and nonzero hypothesis; that result is a conjunction whose second conjunct is exactly the remainder-modulus equality. Project the second component.
why it matters
This is the remainder half of the Euclidean display surface. It is wired in as the remainder display field of the closed orbit Euclidean certificate, which packages quotient transport, the remainder bound, and the reconstruction identity into one δ-only surface (including signed-rational normalization by native orbit GCD).
Downstream, residue transport in the factorization layer unfolds residue to remainder and applies this lemma directly. The reconstruction identity (quotient times divisor plus remainder recovers the dividend) rewrites through this transport then finishes in Nat arithmetic. The strict remainder bound likewise rewrites here and invokes ordinary modulus-less-than.
In the foundation chain this locks Euclidean structure on pure distinction orbits to verifier Nat before native factorization and residue classes can proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.