rationalSignCharacter_recip
plain-language theorem explainer
For any nonzero rational $x$, the real sign character of $x^{-1}$ equals the reciprocal of the sign character of $x$. Cost and character-factorization arguments cite this when transporting sign data across inversion on $\mathbb{Q}$. The proof is a two-case split on the sign of $x$, followed by simplification of the piecewise definition.
Claim. Let $x\in\mathbb{Q}$ with $x\neq 0$. Write $\mathrm{sgn}_{\mathbb{Q}}(x)$ for the real-valued sign map that sends $0$ to $0$, positives to $1$, and negatives to $-1$. Then $\mathrm{sgn}_{\mathbb{Q}}(x^{-1})=(\mathrm{sgn}_{\mathbb{Q}}(x))^{-1}$.
background
In the real-character factorization layer of the cost module, the rational sign character is the piecewise map $\mathrm{sgn}_{\mathbb{Q}}:\mathbb{Q}\to\mathbb{R}$ with value $0$ at zero, $1$ on positives, and $-1$ on negatives. It is the discrete sign factor that later multiplies a positive real magnitude character on ratio orbits.
The local setting is factorization of real ratio characters under Recognition-native cost hypotheses (including sans-anchor and PRC-native uniqueness imports). Inversion on nonzero rationals must preserve the multiplicative character law, so the sign piece needs a clean reciprocity identity before the full candidate character is assembled.
Upstream, the definition itself is the only direct dependency: the piecewise if on zero and positivity. No deeper cost identity is required for this lemma.
proof idea
Term-mode proof by cases on the sign of the nonzero rational $x$ via lt_or_gt_of_ne.
If $x<0$, then $x^{-1}<0$ by inv_lt_zero, and both sides evaluate to $-1$ after unfolding the piecewise definition (with nonzero guards). If $x>0$, then $x^{-1}>0$ by inv_pos, and both sides evaluate to $1$. Each branch finishes by simp on the definition and the sign facts.
why it matters
The lemma is the sign half of reciprocity for the full real character candidate. Downstream, realCharacterCandidate_recip applies it (together with magnitude reciprocity) to show that the candidate character on ratio orbits sends reciprocal orbits to reciprocal values under the sans-anchor hypotheses.
Within Recognition Science cost structure, characters factor the native cost along orbits; sign reciprocity is bookkeeping needed so inversion on the rational skeleton stays compatible with the multiplicative form of the Recognition Composition Law and with PRC-native uniqueness. It does not itself force $J$, $\varphi$, or dimension, but it is a necessary algebraic step in the real-character pipeline that feeds those uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.