rationalTrace_dAlembert
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the rational doubled-trace display obeys the multiplicative d'Alembert identity T(xy)+T(x/y)=T(x)T(y) for nonzero rationals. Character-factorization and uniqueness arguments cite it to move from orbit carriers to honest rational functions. The proof lifts the orbit-level identity by matching product and quotient displays via cross-equality of ratio orbits.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base-sans-two normalization, sign-reversal, monotonicity, and zero-calibrated doubled trace). Write $T_F:\mathbb{Q}\to\mathbb{R}$ for the real doubled-trace display of $F$ on rational inputs. Then for all nonzero $x,y\in\mathbb{Q}$, $$T_F(xy)+T_F(x/y)=T_F(x)\,T_F(y).$$
background
This module builds a real character factorization of native recognition cost on ratio orbits. A ratio orbit is an integer-rational carrier with a verifier display toRat; cross-equality of orbits is equivalent to equality of those rational displays. The doubled trace of a native cost map $F$ is first valued on carriers, then projected to a real traceDisplay.
rationalTrace F x is simply that display evaluated on the canonical orbit of the rational $x$: an honest function $\mathbb{Q}\to\mathbb{R}$. The hypothesis pack SansAnchorHypotheses is the anchor-free structural pack matching the PRC native-cost hypotheses without a fixed two-anchor: base-sans-two normalization, sign-reversing, monotone, and zero-calibrated doubled trace.
Upstream, traceDisplay_dAlembert already gives the same identity on nonzero ratio orbits, via doubledTrace_dAlembert_of_sansAnchor. The present theorem is the rational-display form of that d'Alembert law, the multiplicative skeleton behind the Recognition Composition Law for $J$.
proof idea
Form the canonical orbits ox, oy of the nonzero rationals $x,y$, and check their toRat displays remain nonzero. Invoke traceDisplay_dAlembert on those orbits to obtain the carrier-level identity.
Two bridge lemmas identify the product and quotient displays with the rational-trace values: traceDisplay_eq_of_crossEq plus crossEq_iff_toRat_eq, using mul_toRat and div_toRat together with ratioOrbitOfRat_toRat, show
traceDisplay F (ox·oy) = rationalTrace F (x y) and likewise for the quotient. Rewrite the orbit identity under those equalities to finish.
why it matters
This is the rational working form of the native-cost d'Alembert equation used throughout real character factorization. Downstream, nontrivialCharacterValue_mul and nontrivialCharacterValue_recip_sum build the multiplicative character and reciprocal-sum identities from it; nontrivialCharacterValue_two specializes at $x=y=2$ to pin the anchor root. The trivial branch uses it in rationalTrace_two_pow_eq_two and rationalTrace_pos_eq_two_of_two_eq_two to force $T\equiv 2$ on positive rationals once $T(2)=2$.
In the Recognition framework this is the multiplicative skeleton of the Recognition Composition Law (RCL) and of T5 $J$-uniqueness: the same d'Alembert shape that forces $J(x)=\cosh(\log x)-1$ appears here as a theorem about the doubled-trace display before the cost is recovered. It closes the passage from orbit carriers to rational functions needed for character uniqueness of native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.