rationalSignCharacter_nonzero
plain-language theorem explainer
On nonzero rationals the real sign character never vanishes: it returns +1 or −1 according to the sign of the input. Anyone assembling a multiplicative real character on ratio orbits cites this to keep the candidate off zero away from the origin. The proof is a two-branch case split on the sign of x followed by simplification of the piecewise definition.
Claim. For every rational $x \neq 0$, the real sign character of $x$ is nonzero. Explicitly, that character equals $0$ at $0$, equals $+1$ when $x > 0$, and equals $-1$ when $x < 0$; hence on $\mathbb{Q}\setminus\{0\}$ its values lie in $\{\pm 1\}$.
background
The ambient module builds real multiplicative characters on ratio orbits from the Recognition Composition Law and the native cost uniqueness results. The real sign character is the elementary piecewise map on rationals that sends zero to zero, positives to $+1$, and negatives to $-1$. It is the sign factor that will later be multiplied into a candidate character built from a doubled-trace functional on orbits.
The local setting is factorization of real characters for the cost calculus: one separates a rational sign piece from a positive real magnitude piece so that the full candidate remains multiplicative and never zero off the origin. Upstream, the definition of the sign character is pure case distinction; no deeper analytic input is required for the nonvanishing claim itself.
proof idea
From $x \neq 0$ obtain the dichotomy $x < 0$ or $x > 0$. In the negative branch, simplify the definition with the facts $x \neq 0$ and $\neg(0 < x)$, yielding $-1 \neq 0$. In the positive branch, the same simplification yields $+1 \neq 0$. No external lemmas are invoked beyond the definition and the order trichotomy on rationals.
why it matters
Nonvanishing of the sign factor is the first gate for the full real character candidate. The immediate parent is realCharacterCandidate_nonzero, which combines this fact with the positive magnitude piece under the SansAnchor hypotheses to conclude that the assembled candidate never hits zero on nonzero ratio orbits. That nonvanishing is required before one can treat the candidate as a genuine character in the cost factorization pipeline that feeds PRC-native cost uniqueness and the real-ratio character constructions. Within the broader Recognition framework it is bookkeeping rather than a forcing-chain step, but without it the later uniqueness and d'Alembert identities for doubled traces cannot be stated on the full multiplicative group of orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.