rationalSignCharacter
plain-language theorem explainer
The sign character on the rationals, valued in the reals and set to zero at zero: +1 on positives, −1 on negatives. Cost and gauge-orbit arguments cite it as the degenerate real character extracted from a native cost. The body is a two-branch case split on the sign of the rational.
Claim. For $x \in \mathbb{Q}$, define $\mathrm{sgn}_{\mathbb{R}}(x) = 0$ if $x = 0$, $1$ if $x > 0$, and $-1$ if $x < 0$.
background
In the real-character factorization of Recognition costs, a real-valued multiplicative character on ratio orbits is peeled off a native cost functional. The degenerate case of that extraction is pure sign: no nontrivial power of the orbit coordinate remains.
The ambient module builds characters on rational ratio data (via trace roots and rational exponents) and ties them to PRC-native cost uniqueness. The sign map is the baseline character against which nontrivial power characters are compared when testing gauge orbits and d'Alembert-type identities for doubled traces.
Downstream, the same map is the explicit value of the real-character candidate on the sign-gauge native cost, and it is the witness that the extracted exponent vanishes.
proof idea
Definition by cases: zero at zero; otherwise the ordinary real sign of the rational. No lemmas are applied.
why it matters
This is the concrete character that the factorization theorem returns on the sign-gauge native cost: the candidate equals the rational sign character of the orbit's rational representative. Parent results then show the extracted exponent is zero and that the character is not any positive odd-integer power already at the anchor orbit of 2.
Sibling lemmas record that the map is multiplicative, nonzero off zero, and identically one on positives, so it behaves as a group homomorphism $\mathbb{Q}^\times \to {\pm 1}$ with the usual zero extension. In the broader cost story it marks the degenerate real character against which nontrivial ladder or power characters are distinguished when closing gauge-orbit uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.