PRCSignedOrbitSignCanonical
plain-language theorem explainer
A signed orbit is sign-canonical when it is exactly the nonnegative display of its absolute value, or exactly the negation of that display, matching the raw form produced by signed quotient. Ratio-reduction and native-cost uniqueness arguments cite this predicate to pin representatives, not merely integer equality. The body is a two-branch propositional definition on the integer recovery map and the of-orbit constructors.
Claim. A signed orbit $z$ is sign-canonical if either $z.\mathrm{toInt}\ge 0$ and $z$ equals the nonnegative orbit display of $|z|$, or $z.\mathrm{toInt}<0$ and $z$ equals the negation of that nonnegative display. Equivalently, the raw representative is the canonical signed form of its absolute orbit, not merely equal as a balanced integer.
background
In the primitive recognition calculus, costs and characters are tracked on orbit displays rather than bare rationals. A signed orbit packages an absolute distinction-nat orbit with a sign flag; toInt recovers the corresponding integer, while ofOrbit builds the canonical nonnegative display and negate flips sign.
Sign-canonicity is stricter than integer equality: the display must be literally the constructor form that signedQuotient emits. The module develops native-cost uniqueness via reduced ratio displays; the next definition, reduced-and-sign-canonical ratios, requires the numerator to satisfy this predicate and to be coprime to a positive denominator.
Upstream integer recovery (IntegersFromLogic.toInt) supplies the comparison $0\le z.\mathrm{toInt}$ versus $z.\mathrm{toInt}<0$ that splits the two branches.
proof idea
Definitional, not a proof. The predicate is the disjunction of two constructor equations: nonnegative integer recovery with equality to ofOrbit of the absolute orbit, or negative recovery with equality to negate of that same ofOrbit. No lemmas are applied; downstream theorems unfold this definition and case on the nonnegativity flag of signedQuotient.
why it matters
Native cost uniqueness in Recognition Science needs rigid ratio representatives so cross-equality of reduced displays forces identical numerators. This predicate is the signed-orbit half of that rigidity: PRCRatioReducedSignCanonical conjoins it with coprimality, and PRCReducedSignCanonical_num_eq_of_crossEq uses both sides to conclude numerator equality under cross-equality.
signedQuotient_signCanonical_of_divides shows the quotient constructor always lands in this form, so the raw representative condition is inhabited rather than vacuous. The pass-25 blocker certificate structure records that full native-cost uniqueness is not closed; sign-canonical reduction is part of the exact Lean surface those open factorization targets sit on. Framework-wise this is bookkeeping for the J-cost uniqueness chain (T5 and the Recognition Composition Law), not a new physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.