linearExtraction_recip_sum
plain-language theorem explainer
Under reciprocal invariance and the multiplicative d'Alembert law for a real map T on nonzero rationals, linear extraction against a nondegenerate root r of the two-anchor recovers T(x) when summed on a reciprocal pair. Cost-module character factorization cites this identity. The proof feeds the doubled relation at (2,x), rewrites T(2) via r+r^{-1}, and clears the denominator r^2-1 by field and ring algebra.
Claim. Let $T:\mathbb{Q}\to\mathbb{R}$ satisfy $T(x^{-1})=T(x)$ for all $x$ and $T(xy)+T(x/y)=T(x)T(y)$ for all nonzero $x,y$. Fix $r\in\mathbb{R}$ with $r\neq 0$, $r^2\neq 1$, and $r+r^{-1}=T(2)$. Define the linear extraction $L_r(x)=(r\,T(2x)-T(x))/(r^2-1)$. Then for every nonzero rational $x$, $L_r(x^{-1})+L_r(x)=T(x)$.
background
In the real character factorization of Recognition cost, one works with a real-valued map $T$ on rationals that is reciprocal-invariant and obeys the multiplicative d'Alembert identity $T(xy)+T(x/y)=T(x)T(y)$. That identity is the doubled-trace form of the Recognition Composition Law after centering; sibling lemmas record how it arises from native cost, from RCL, and from sans-anchor hypotheses.
Linear extraction against a chosen root $r$ is the explicit reconstruction $L_r(x)=(r,T(2x)-T(x))/(r^2-1)$. The root is anchored at the distinguished positive integer two by $r+r^{-1}=T(2)$, with nondegeneracy $r\neq 0$ and $r^2\neq 1$ so the denominator is live. The two-anchor is forced because the eight-tick and ratio-orbit calculus singles out the orbit of $2$ as the first nontrivial positive integer scale.
The present lemma is the reciprocal-sum identity for that extractor: adding the extractions at $x$ and $x^{-1}$ cancels the off-diagonal terms and returns $T(x)$ itself.
proof idea
Instantiate the d'Alembert hypothesis at the pair $(2,x)$. Rewrite $2/x$ as $2x^{-1}$, so the identity becomes $T(2x)+T(2x^{-1})=T(2),T(x)$. From the anchor $r+r^{-1}=T(2)$ obtain $T(2)=(r^2+1)/r$ by clearing the nonzero $r$.
Unfold both linear extractions and use reciprocal invariance $T(x^{-1})=T(x)$. The target sum is then a common-denominator expression whose numerator is $r,T(2x^{-1})-T(x)+r,T(2x)-T(x)$. Regroup to $r(T(2x)+T(2x^{-1}))-2T(x)$, substitute the doubled identity and the rewritten $T(2)$, and simplify by field arithmetic and ring to $(r^2-1)T(x)$. Cancel the nonzero denominator $r^2-1$ to finish.
why it matters
This is the algebraic engine that lets a nontrivial real character recover the rational trace on reciprocal pairs. Downstream, nontrivialCharacterValue_recip_sum applies it under SansAnchorHypotheses with a nondegenerate two-trace, obtaining
$\mathrm{ncv}(x^{-1})+\mathrm{ncv}(x)=\mathrm{rationalTrace}(x)$.
In the broader cost story, character factorization separates the J-cost (T5 uniqueness: $J(x)=\cosh(\log x)-1$) into multiplicative characters on the ratio orbit. The linear extraction is the concrete bridge from the doubled d'Alembert form back to the original cost values. Without the reciprocal-sum identity, the factorization would only control even combinations and could not pin the full trace on every nonzero rational.
The lemma is private scaffolding inside RealCharacterFactorization; its public payload is the nontrivial-character corollary that feeds later uniqueness and rigidity arguments for native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.