linearExtraction
plain-language theorem explainer
Linear extraction recovers a candidate multiplicative character value from a reciprocal real trace T at a rational argument x, given a chosen nondegenerate anchor root r. Cost and character-factorization arguments cite it when peeling a real ratio character out of a d'Alembert-type doubled trace. It is a pure closed-form definition: (r T(2x) - T(x))/(r^{2} - 1).
Claim. For a map $T:\mathbb{Q}\to\mathbb{R}$ and a real number $r$ with $r^{2}\neq 1$, the linear extraction at $x\in\mathbb{Q}$ is the real number $\dfrac{r\,T(2x)-T(x)}{r^{2}-1}$.
background
In the real-character factorization of Recognition cost, one works with reciprocal traces $T:\mathbb{Q}\to\mathbb{R}$ obeying a d'Alembert identity of the form $T(xy)+T(x/y)=T(x)T(y)$ (for nonzero rationals), together with $T(x^{-1})=T(x)$. Such a $T$ is the sum of a multiplicative character and its reciprocal: schematically $T(x)=\chi(x)+\chi(x)^{-1}$.
The anchor at two fixes the characteristic equation $t+t^{-1}=T(2)$. A chosen root $r$ of that equation (the nondegenerate anchor root) labels one of the two conjugate characters. Linear extraction is the elementary linear combination that isolates the $\chi(x)$ branch from the pair ${T(x),T(2x)}$ once $r$ is fixed.
Downstream, the same formula is specialized to the rational trace of a ratio-orbit map $F$, with $r$ taken to be the anchor root of $F$, yielding the nondegenerate symbolic character value.
proof idea
Pure definition: no proof obligations. The body is the single arithmetic expression $(r\cdot T(2x)-T(x))/(r^{2}-1)$. Nondegeneracy of the anchor is encoded only as the standing requirement that the denominator $r^{2}-1$ be nonzero in later lemmas; the definition itself does not assert that condition.
why it matters
This is the algebraic kernel of real character factorization in the cost calculus. It is the body of nontrivialCharacterValue, which extracts the nondegenerate symbolic character from the rational trace at a chosen anchor root. Private lemmas then establish the character axioms for the extraction: unit normalization (linearExtraction_unit: value 1 at 1 when $T(1)=2$ and $r+r^{-1}=T(2)$), multiplicativity, and the reciprocal-sum identity, all under the reciprocal and d'Alembert hypotheses on $T$.
Those facts feed nontrivialCharacterValue_two, which identifies the extracted value at 2 with the anchor root itself whenever the trace is nondegenerate ($T(2)\neq 2$). In the broader RS picture this is how a doubled-trace cost (the RCL/J side) is factored into a genuine multiplicative character on positive rationals, the step needed before matching native PRC cost uniqueness and building cost-from-character reconstructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.