remainder
plain-language theorem explainer
Object-level remainder of one distinction-orbit count by another, taken as the second component of the Euclidean div-mod pair. Anyone building discrete orbit arithmetic on DistinctionNat cites this accessor. The body is a one-line projection of divMod; no separate proof content.
Claim. For distinction-orbit naturals $n$ and $d$ with $d \neq 0$, the remainder of $n$ by $d$ is the second component of the Euclidean quotient-remainder pair of $n$ divided by $d$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor that plays the role of the natural numbers at the object level of the primitive recognition calculus.
This module equips those orbits with Euclidean arithmetic. The upstream divMod computes a quotient-remainder pair by fuelled repeated subtraction; the fuel is the dividend itself, which is enough when the divisor is nonzero because each successful subtraction lowers the dividend by at least one.
remainder is the named second projection of that pair, parallel to the object-level quotient accessor.
proof idea
One-line definitional wrapper: return the second component of divMod n d hd. No tactics, no lemmas beyond the upstream Euclidean pair.
why it matters
Infrastructure for object-level Euclidean arithmetic on distinction orbits. Local consumers include the division-algorithm facts (remainder_lt_divisor, quotient_mul_divisor_add_remainder_eq) and the toNat bridge. Downstream the name appears across foundation and cost layers (Boltzmann $k_R$ bounds, J-cost linearization remainder, continuum-limit remainder estimates, discreteness forcing via $J_{\log}$ curvature, Hamiltonian emergence). In the Recognition stack it supports the discrete substrate under the continuous J-cost and the phi-ladder constructions; it does not itself encode a physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.