traceDisplay_dAlembert
plain-language theorem explainer
Under anchor-free native-cost hypotheses, the real display of the doubled trace on ratio orbits obeys the multiplicative d'Alembert law: T(xy)+T(x/y)=T(x)T(y) whenever the rational displays of x and y are nonzero. Cost and character-factorization arguments cite this when moving from carrier-level identities to real arithmetic. The proof is a short cast: apply the orbit-level doubled-trace identity, then transport via toRat add/mul and cross-equality.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost package (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). Write $T_F(q)$ for the real number obtained by casting the rational display of the native doubled trace of $F$ at $q$. For ratio orbits $x,y$ with nonzero rational displays, $$T_F(xy)+T_F(x/y)=T_F(x)\,T_F(y).$$
background
This module works in the Primitive Recognition Calculus cost setting, where costs live on ratio orbits (signed rational displays with denominator data) rather than bare reals. The native doubled trace of a map $F$ is a carrier-valued object; traceDisplay is its real readout: cast (nativeCostDoubledTrace F q).toRat to $\mathbb{R}$.
SansAnchorHypotheses is the anchor-free pack matching the structural native-cost hypotheses without an anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Nonzero toRat hypotheses keep multiplication and division of orbits well-defined on the rational display.
Upstream, doubledTrace_dAlembert_of_sansAnchor already proves the same identity at the orbit level as a crossEq of sums and products of doubled traces. The IntegerRational layer supplies the bridge: crossEq_iff_toRat_eq ("cross-multiplication agrees with rational equality of the verifier displays"), plus add_toRat and mul_toRat.
proof idea
Term-mode reduction, not a fresh functional-equation argument. Invoke doubledTrace_dAlembert_of_sansAnchor on the same hypotheses to obtain an orbit-level crossEq between the sum of doubled traces at $xy$ and $x/y$ and the product of doubled traces at $x$ and $y$.
Rewrite that crossEq with crossEq_iff_toRat_eq, then expand the left and right sides by add_toRat and mul_toRat, so both sides become ordinary rational equalities of toRat values. Unfold traceDisplay (real cast of those rationals) and finish by exact_mod_cast.
why it matters
This is the real-display form of the multiplicative d'Alembert identity for native doubled traces under the anchor-free pack. It is the direct parent of rationalTrace_dAlembert, which restates the same law on bare nonzero rationals via ratioOrbitOfRat.
In the Recognition framework the d'Alembert shape is the character form behind cost uniqueness: the classical J-cost satisfies the Recognition Composition Law, and the doubled/shifted trace factors as a multiplicative character (linked to T5 J-uniqueness, $J(x)=\cosh(\log x)-1$). Establishing the identity first on orbits, then on real displays, then on $\mathbb{Q}$, is the factorization ladder that lets native PRC cost match the unique real cost character without smuggling analytic assumptions into the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.