quotient_toNat
plain-language theorem explainer
Object-level Euclidean quotient on finite distinction orbits agrees with ordinary natural division after the verifier map toNat. Anyone building δ-only arithmetic, ratio normalization, or the orbit Euclidean certificate cites this bridge. The proof is a one-line projection of the first conjunct of divMod_toNat.
Claim. For finite distinction orbits $n$ and $d$ with $d \neq 0$, if $q$ is the object-level Euclidean quotient of $n$ by $d$, then the verifier natural number of $q$ equals the ordinary natural quotient: $\mathrm{toNat}(q) = \mathrm{toNat}(n)\,/\,\mathrm{toNat}(d)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the K2.12 carrier for δ-only counting. Its verifier map toNat sends zero to 0 and succ to Nat.succ, so every orbit position has a unique Lean Nat reading.
In this module the Euclidean algorithm is rebuilt on DistinctionNat. The pair divMod returns an object-level quotient and remainder; quotient is defined as the first component of that pair. The companion theorem divMod_toNat states that both components transport: the quotient side becomes Nat division and the remainder side becomes Nat modulus.
The local setting is Primitive Recognition Calculus: arithmetic reconstructed from recognition orbits before integers or rationals are assumed as primitives. The IntegerRational and OrbitDivisibility imports supply the surrounding orbit arithmetic used downstream.
proof idea
Invoke divMod_toNat on the same $n$, $d$, and nonzero hypothesis. That lemma returns a conjunction equating the toNat-images of both components of divMod to Nat division and modulus. Project the first conjunct; by definition quotient is exactly the first component of divMod, so the desired equality is immediate. Term-mode, no induction at this layer.
why it matters
This is the display law for object-level quotient in the closed δ-only Euclidean surface. It is wired directly into orbit_euclidean_certificate as quotient_display, alongside divMod_toNat, remainder_toNat, the remainder bound, and the reconstruction identity.
Downstream, quotient_mul_divisor_add_remainder_eq uses it (with remainder_toNat and toNat injectivity) to prove $q\cdot d+r=n$ in orbit arithmetic. quotient_mul_divisor_toNat_of_divides reduces exact division to Nat.div_mul_cancel. signedQuotient_abs_toNat and normalizeRatio_coprime lift the same bridge to signed orbits and coprime ratio normalization via native orbit GCD.
In the Recognition foundation this sits under the forcing chain’s arithmetic layer: finite orbits must support Euclidean structure before phi-ladder mass formulas or continuum limits appear. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.