signedQuotient
plain-language theorem explainer
Signed Euclidean quotient of a signed orbit difference by a nonzero orbit position: divide the absolute orbit magnitude, then restore the original structural sign. Ratio-normalization and native-cost uniqueness cite it when reducing signed numerators by a GCD. The body is a short case split on the nonnegative flag around the unsigned orbit quotient.
Claim. Given a signed orbit difference $z$ (intended as $\mathrm{pos}-\mathrm{neg}$) and a nonzero orbit position $d$, form the unsigned quotient $q$ of $|z|$ by $d$. Return the nonnegative embedding of $q$ if $z$ is structurally nonnegative, and its pointwise negation otherwise.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (Peano-style zero/successor). A SignedOrbit is a pair of such positions with intended meaning $\mathrm{pos}-\mathrm{neg}$. Its absolute value is the orbit absolute difference of the two sides; the computable nonnegative flag is the structural comparison $\mathrm{neg}\le\mathrm{pos}$.
Nonnegative embeddings send an orbit position $n$ to $\langle n,0\rangle$; negation swaps the two sides. The ambient module builds a native Euclidean algorithm on orbits (div/mod, gcd) without importing classical integers as primitives.
The unsigned quotient already divides one orbit magnitude by a nonzero divisor. This definition lifts that operation to signed differences while keeping sign data structural rather than classical.
proof idea
Definitional construction, not a proof. Compute the unsigned quotient $q$ of $z$'s absolute orbit by $d$ (using the nonzero hypothesis). Branch on the structural nonnegative flag of $z$: if true, return the nonnegative embedding of $q$; if false, return the negation of that embedding. Sign is therefore restored exactly by the same comparison that defines nonnegativity of signed orbits.
why it matters
Feeds ratio normalization: normalizeRatio divides a ratio's signed numerator magnitude and denominator by their native orbit GCD, restoring numerator orientation via this signed quotient. Companion lemmas record that the absolute value matches classical integer division and that, when $d$ divides $|z|$, multiplying the signed quotient by $d$ recovers $z$ as an integer.
Downstream native-cost uniqueness work uses it for sign-canonicity after division and for the canonical-normalization target on ratio orbits (cross-equivalent raw ratios should share one GCD-normalized representative). That target is part of closing quotient-respect for normalized invariants in the PRC native-cost uniqueness blocker certificate. Locally this is Euclidean bookkeeping on orbits; framework-wide it supports unique reduced displays before cost uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.