rationalSignCharacter_one
plain-language theorem explainer
The rational sign character evaluates to +1 at the unit 1. Anyone assembling real multiplicative characters for cost factorization on ratio orbits will cite this normalization. The proof is a one-line simplification of the piecewise definition.
Claim. The real sign character on rationals, which sends $0$ to $0$, positive rationals to $+1$, and negative rationals to $-1$, satisfies $\mathrm{sgn}_{\mathbb{Q}}(1)=1$.
background
In the real-character factorization of Recognition cost, one factors a candidate character on ratio orbits into a rational trace part and a sign part. The rational sign character is the ordinary sign map $\mathbb{Q}\to\mathbb{R}$, extended by zero at zero: it returns $0$ at $0$, $+1$ on positives, and $-1$ on negatives.
The ambient module builds real characters compatible with the Recognition Composition Law and with native cost uniqueness from the primitive recognition calculus. Unit normalization at the identity orbit is the first sanity check before comparing characters to the J-cost or to doubled-trace d'Alembert identities.
proof idea
One-line wrapper: unfold the piecewise definition of the rational sign character and simplify. Since $1\neq 0$ and $0<1$, the positive branch fires and returns $1$.
why it matters
Feeds directly into the unit law for the real character candidate: under the sans-anchor hypotheses on a map $F$ of ratio orbits, the candidate character at the identity orbit equals $1$, and the proof case-splits on the rational trace at $2$ then simplifies using this fact together with the identity orbit's rational representative.
That unit law is part of matching multiplicative characters to the unique J-cost forced by T5 in the forcing chain ($J(x)=(x+x^{-1})/2-1$), so sign normalization at $1$ is a small but mandatory step in the real factorization path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.