rationalSignCharacter_mul
plain-language theorem explainer
The rational sign map (0 at zero, otherwise ±1 by sign) is completely multiplicative on ℚ. Anyone assembling a real multiplicative character from a ratio-orbit cost needs this identity. The proof is exhaustive case analysis on zeros and signs, discharging each branch by simplification.
Claim. For all rationals $x,y\in\mathbb{Q}$, if $\sigma:\mathbb{Q}\to\mathbb{R}$ is the sign character with $\sigma(0)=0$, $\sigma(x)=1$ for $x>0$, and $\sigma(x)=-1$ for $x<0$, then $\sigma(xy)=\sigma(x)\,\sigma(y)$.
background
In the cost module, the real sign character on rationals is the piecewise map that sends zero to zero and nonzero rationals to $\pm 1$ according to sign. It is the discrete factor that will later sit beside a positive real magnitude character when one factors a candidate real character on ratio orbits.
The local setting is RealCharacterFactorization: one builds multiplicative real characters from Recognition-native cost data (d'Alembert/RCL structure, sans-anchor hypotheses) so that a cost functional can be recovered from its character. Multiplicativity of the sign piece is the elementary arithmetic ingredient before the orbit-level statement.
Upstream, the definition itself is the only conceptual dependency; the proof also uses standard nonzero-product facts (product of nonzero rationals is nonzero) and sign-of-product rules for the four nonzero sign combinations.
proof idea
Tactic proof by cases. First handle $x=0$ and $y=0$ separately: both sides collapse to $0$ by the definition of the sign character. For the remaining nonzero pair, record $xy\neq 0$ via the nonzero-product lemma, then split on the four sign patterns $(x,y)\in{<0,>0}^2$. In each branch compute the sign of $xy$ (product of two negatives is positive; mixed signs give negative; two positives give positive) and simplify the definition on both sides to matching $\pm 1$ products.
why it matters
This lemma is the rational-level multiplicativity step feeding realCharacterCandidate_mul, which lifts the same identity to ratio orbits under sans-anchor hypotheses: the candidate real character of a product orbit equals the product of the characters. Without sign multiplicativity, the factorization of a real character into magnitude times sign would fail to be a group homomorphism on the multiplicative monoid of nonzero rationals.
In the Recognition cost story, real characters are the bridge from native cost uniqueness (PRC native cost, RCL/d'Alembert structure on the doubled trace) to a concrete real-valued multiplicative functional. The sign factor is the discrete half of that bridge; the continuous half lives on positive magnitudes. The result is pure arithmetic and does not itself invoke J-uniqueness or the forcing chain, but it is required scaffolding for any cost-from-character reconstruction that must respect multiplication of ratio data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.