linearExtraction_unit
plain-language theorem explainer
If a real-valued rational map T has T(1)=2 and a nondegenerate root r of the doubled-trace identity at 2, then the linear extraction of that root at argument 1 equals 1. Character-factorization arguments cite this to fix the unit value of the extracted ratio character. The proof is a short field-arithmetic reduction after rewriting the trace identity as a rational expression in r.
Claim. Let $T:\mathbb{Q}\to\mathbb{R}$ and $r\in\mathbb{R}$ satisfy $T(1)=2$, $r\neq 0$, $r^2-1\neq 0$, and $r+r^{-1}=T(2)$. Then the linear extraction $\frac{r\,T(2\cdot 1)-T(1)}{r^2-1}$ equals $1$.
background
In the real-character factorization of Recognition cost, one starts from a rational trace $T:\mathbb{Q}\to\mathbb{R}$ obeying the doubled-trace d'Alembert relation inherited from the Recognition Composition Law. A nondegenerate anchor root $r$ is a real number with $r\neq 0$, $r^2\neq 1$, and $r+r^{-1}=T(2)$.
Linear extraction is the explicit formula $$\mathrm{lin}_T(r;x)=\frac{r,T(2x)-T(x)}{r^2-1},$$ which peels a putative multiplicative character off the trace once an anchor root is chosen. The present lemma evaluates that formula at the unit rational $x=1$.
The ambient module builds real ratio characters from native PRC cost uniqueness and rational-orbit traces; the unit evaluation is the first sanity check before nontrivial character values are identified.
proof idea
From $r+r^{-1}=T(2)$ and $r\neq 0$, rewrite $T(2)=(r^2+1)/r$. Substitute into the extraction formula at $x=1$, using $T(1)=2$ and $2\cdot 1=2$. The resulting rational expression simplifies by field arithmetic (denominator $r^2-1\neq 0$) and a final ring identity to $1$. No external lemmas beyond the definition of linear extraction are required.
why it matters
Downstream, nontrivialCharacterValue_one applies this unit evaluation under Sans-anchor hypotheses: once the rational trace is nontrivial at 2, the extracted nontrivial character value at 1 is forced to 1. That pins the multiplicative character on the positive rational orbit at the identity, which is the base case for the full real-character factorization of native PRC cost.
In the broader Recognition chain this sits inside the cost layer that realizes J-uniqueness (T5) and the RCL functional equation as a concrete real character on ratio orbits. Without the unit value, the character would not be normalized and the factorization into cost-from-character would fail at the identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.