signedQuotient_signCanonical_of_divides
plain-language theorem explainer
Whenever a nonzero distinction d divides the absolute value of a signed orbit z, the signed quotient of z by d is sign-canonical: it is literally the nonnegative orbit of its absolute value, or literally the negation of that orbit. Ratio-normalization and native-cost uniqueness cite this to lock the raw signed numerator into the canonical display form. The proof is a two-branch case split on the nonnegativity flag, with quotient nonzeroness on the negative side.
Claim. Let $z$ be a signed orbit and $d$ a nonzero distinction natural. If $d$ divides the absolute value of $z$, then the signed quotient of $z$ by $d$ is sign-canonical: either $0 \le q.toInt$ and $q$ equals the nonnegative orbit display of $|q|$, or $q.toInt < 0$ and $q$ equals the negation of that display.
background
In the Primitive Recognition Calculus, integers are recovered as signed orbits: pairs of distinction-naturals with a nonnegativity flag, and absolute value abs reading off the orbit position via absolute difference of the positive and negative legs. The recovery map toInt sends a signed orbit to an ordinary integer.
Sign-canonicity is a raw-representative condition, not mere integer equality: a signed orbit $z$ is sign-canonical when it is literally ofOrbit of its absolute value (nonnegative case) or literally the negation of that display (negative case). The operation signedQuotient z d builds the signed orbit whose absolute value is the ordinary quotient of $|z|$ by $d$, preserving the sign flag of $z$.
This sits in the native-cost uniqueness module, which forces the PRC cost character to match the doubled-trace d'Alembert form. Upstream arithmetic supplies toNat, toInt, and absolute-value lemmas used to compare orbit positions with ordinary naturals and integers.
proof idea
Unfold signedQuotient and case on the nonnegativity flag of $z$.
If the flag is true, take the left disjunct of sign-canonicity: simplify with the flag and ofOrbit_toInt, then rewrite the if_pos branch and apply signedOrbit_ofOrbit_abs_self so the result equals the nonnegative orbit of its absolute value.
If the flag is false, take the right disjunct. Derive toInt z < 0 from the flag-false characterization. Show $|z| \neq 0$ via abs_ne_zero_of_toInt_ne_zero, then that the ordinary quotient is nonzero by quotient_ne_zero_of_divides, hence its toNat is positive. Conclude with negate_toInt and ofOrbit_toInt for the integer inequality, and signedOrbit_neg_ofOrbit_abs_self for the raw equality after the if_neg branch.
why it matters
Native-cost uniqueness needs reduced, sign-canonical ratio displays so that cost characters are compared on a unique raw representative, not up to balanced-integer equivalence alone. The immediate parent normalizeRatio_reduced_signCanonical packages coprimality of the normalized ratio with this sign-canonicity fact: after dividing numerator and denominator by their gcd, the signed numerator is forced into the canonical orbit form.
That normalization feeds the blocker certificate prc_native_cost_uniqueness_blocker_certificate, which records the proved zero-calibrated factorization target and the refutation of the signed-admissible alternative. In the broader Recognition chain this is foundation plumbing under T5 J-uniqueness and the Recognition Composition Law: the cost functional is identified only after ratio displays are pinned to a single raw shape. Without this lemma, normalize-ratio would only guarantee coprimality, leaving a sign-display gap in the uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.