linearExtraction_multiplicative
plain-language theorem explainer
The linear extraction that recovers a real multiplicative character from a reciprocal d'Alembert-type rational trace T, anchored at a nondegenerate root r of T(2), is itself multiplicative on nonzero rationals. Anyone assembling real ratio characters from native cost data cites this. The proof expands the product of two extractions via several instances of the functional equation and cancels with the anchor identity r + r^{-1} = T(2).
Claim. Let $T:\mathbb{Q}\to\mathbb{R}$ satisfy $T(x^{-1})=T(x)$ and $T(xy)+T(x/y)=T(x)T(y)$ for all nonzero $x,y\in\mathbb{Q}$. Fix $r\in\mathbb{R}$ with $r\neq 0$, $r^2-1\neq 0$, and $r+r^{-1}=T(2)$. Then for nonzero $x,y\in\mathbb{Q}$, $$\frac{r\,T(2xy)-T(xy)}{r^2-1}=\Bigl(\frac{r\,T(2x)-T(x)}{r^2-1}\Bigr)\Bigl(\frac{r\,T(2y)-T(y)}{r^2-1}\Bigr).$$
background
In the real-character factorization of rational cost traces, one starts from a map $T:\mathbb{Q}\to\mathbb{R}$ that is reciprocal ($T(x^{-1})=T(x)$) and obeys the multiplicative d'Alembert identity $T(xy)+T(x/y)=T(x)T(y)$ on nonzero rationals. This is the doubled-trace form of the Recognition Composition Law, obtained after the usual shift that turns the native $J$-cost into a pure product law.
The linear extraction $$E_r(x)=\frac{r,T(2x)-T(x)}{r^2-1}$$ is the unique affine combination that peels a genuine multiplicative character out of such a $T$, once a nondegenerate root $r$ of the quadratic $t+t^{-1}=T(2)$ has been chosen (the "anchor"). The denominator $r^2-1\neq 0$ excludes the degenerate fixed points $\pm 1$.
The local module builds real ratio characters from native PRC cost data; the extraction is the bridge from the functional equation on $T$ to a homomorphism on $\mathbb{Q}^\times$.
proof idea
Clear nonzero denominators first (products and quotients of $x$, $y$, and $2$). Instantiate the d'Alembert identity four ways: on $(x,y)$, on $(2x,2y)$, on $(2x,y)$ and $(x,2y)$, and on $(2,x/y)$. Algebraic rewriting of products and quotients (ring/field_simp) plus reciprocity $T((xy)^{-1})=T(xy)$ produces two linear relations:
- $T(2x)T(2y)=T(2)T(2xy)-T(xy)+T(x/y)$,
- $T(2x)T(y)+T(x)T(2y)=2T(2xy)+T(2)T(x/y)$.
Rewrite the anchor as $T(2)=(r^2+1)/r$. Expand the numerator product $(rT(2x)-T(x))(rT(2y)-T(y))$, substitute the two relations and the original identity for $T(x)T(y)$, then simplify with the rewritten anchor; the cross terms cancel and one obtains exactly $(r^2-1)(rT(2xy)-T(xy))$. Unfolding the three extractions and clearing $r^2-1$ finishes the equality.
why it matters
Multiplicativity of the extraction is the algebraic heart of turning a reciprocal d'Alembert trace into a real character of $\mathbb{Q}^\times$. The sole downstream consumer is nontrivialCharacterValue_mul, which lifts the same identity to the nontrivial character value attached to a sans-anchor hypothesis package $F$ (when the rational trace at $2$ is not the degenerate value $2$).
In the broader Recognition chain this sits inside the cost-uniqueness track that feeds T5 ($J$-uniqueness via the RCL) and the subsequent forcing of $\varphi$ as the self-similar fixed point (T6). Without a multiplicative extraction one cannot pass from the native cost functional equation to a genuine ratio character, so the real factorization of cost data would stop at the doubled-trace level.
The result is fully proved (no sorry); it closes the elementary arithmetic step needed before character nontriviality and cost reconstruction lemmas can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.