costFromCharacter_negativeOne_forces_signed_unit
plain-language theorem explainer
If a ratio-orbit character generates the native J-cost at the signed unit −1, then the character itself must fix −1. Anyone closing signed-admissible factorization of a PRC native cost cites this calibration step. The proof reduces cross-equivalence to rational equality and solves x + x⁻¹ = −2 over ℚ\{0}, forcing x = −1.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal on ratio orbits). Write $J$ for the PRC cost $J(q)=((q+q^{-1})/2)-1$ on ratio orbits. If $J(\chi(-1))$ is cross-equivalent to $J(-1)$, then $\chi$ is signed-unit calibrated: $\chi(-1)$ is cross-equivalent to the signed-unit orbit $-1$.
background
Primitive Recognition Calculus works with ratio orbits: integer numerators over nonzero orbit denominators, compared by cross-multiplication rather than definitional equality. Cross-equivalence of two orbits is equivalent to equality of their verifier rationals under the display map toRat.
A ratio-orbit character is a map on ratio orbits that fixes the unit orbit, is multiplicative, and intertwines reciprocals, all up to cross-equivalence. The native PRC cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$. Cost generated from a character is the composite $J\circ\chi$; the identity character recovers the canonical cost.
Signed-unit calibration asks that $\chi$ fix the orbit of $-1$. The module develops uniqueness of native costs via character factorization; prime-direction data alone does not force the sign at $-1$, so a separate calibration hypothesis or forcing lemma is required.
proof idea
Transport everything to rationals. Nonzeroness of $-1$ and the character's nonzero-preserving property give $x:=(\chi(-1)).\mathrm{toRat}\neq 0$. Cross-equivalence iff rational equality, together with the character-cost and native-cost displays at $-1$, rewrites the cost hypothesis as $J(x)=J(-1)$ in $\mathbb{Q}$. That identity is $x+x^{-1}=-2$. Multiplying through by $x$ and clearing the denominator yields a quadratic identity; nlinarith forces $x=-1$, which is signed-unit calibration after transporting back via cross-equivalence.
why it matters
This is the algebraic pin that turns a character factorization of a native cost into a signed-admissible character. Downstream, the zero-calibrated and prime-signed strengthened uniqueness targets invoke it when promoting a factor character to signed-unit calibration; the structural ledger uniqueness theorem and the slim-ledger "forces $J$" theorem sit above those targets.
In the Recognition framework this supports T5-style J-uniqueness at the PRC native layer: once the cost matches $J$ at $-1$, the character cannot flip the signed unit. Without this step, factorization would leave an unresolved sign ambiguity and signed-admissible rigidity would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.