quotient
plain-language theorem explainer
Object-level Euclidean quotient of two distinction-naturals: for nonzero divisor d, return the quotient half of the division pair of n by d. Cited wherever the primitive recognition calculus needs integer division on orbits (gcd fuel, toNat bridges, division identity). Proof shape is a one-line first-projection of divMod.
Claim. Let $n$ and $d$ be distinction-naturals with $d \neq 0$. The quotient of $n$ by $d$ is the first component of the Euclidean division pair $\mathrm{divMod}(n,d)$, i.e. the unique $q$ such that $n = q\cdot d + r$ with $r < d$ in the orbit order.
background
DistinctionNat (K2.12) is the base-neutral finite orbit of repeated distinction: an inductive copy of the naturals with constructors zero and succ, carrying DecidableEq. It is the carrier on which the primitive recognition calculus builds arithmetic before any external ℕ bridge.
This module equips that carrier with a Euclidean algorithm. The core operation is divMod: given n, d with d nonzero, it returns a pair (q, r) by fuelled repeated subtraction (fuel n suffices because each successful step strictly lowers the dividend). The sibling remainder is the second projection of the same pair.
Local setting is Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean: object-level div/mod/gcd on orbits, with later toNat lemmas tying the constructions back to ordinary natural arithmetic.
proof idea
One-line definitional wrapper. Apply divMod n d hd and project the first component of the resulting product type DistinctionNat × DistinctionNat. No tactics, no lemmas beyond the definition of divMod (itself a thin call to divModFuel n n d).
why it matters
Supplies the quotient half of the object-level division algorithm on DistinctionNat. Together with remainder it underwrites the Euclidean identity (quotient · divisor + remainder = dividend) and the remainder-strictly-less-than-divisor bound, which in turn feed the fuelled gcd on orbits.
In the Recognition stack this is pre-physics scaffolding: finite orbits of distinction must support exact division before rung arithmetic, phi-ladder mass formulas, or eight-tick bookkeeping can be stated without smuggling classical ℕ. Parent consumers in-module include quotient_toNat and quotient_mul_divisor_add_remainder_eq; the broader used-by graph is large but partly name-collides with Mathlib quotients and connectivity closures, so the durable role is the Euclidean layer, not those cosmology edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.