doubledTrace_dAlembert_of_native
plain-language theorem explainer
Under the PRC native cost hypotheses on a map F of ratio orbits, the doubled-trace T of F obeys the d'Alembert identity T(xy)+T(x/y)=T(x)T(y) via cross-multiplication. Cost-classification and real-character work on the discrete rational surface cite this. Proof is a one-line specialization of the RCL-only doubled-trace theorem through the native pack's canonical RCL field.
Claim. Let $F$ be a map on ratio orbits satisfying the PRC native cost hypotheses, and let $T$ be its doubled-trace. For all ratio orbits $x,y$ with nonzero rational displays, $T(xy)+T(x/y)=T(x)\,T(y)$ in the sense of cross-multiplication equality of ratio orbits.
background
Ratio orbits are the PRC discrete rationals: a signed-orbit numerator over a nonzero distinction-nat denominator, with verifier display toRat and internal equality by cross-multiplication (crossEq: balanced scaled numerators). Division is multiplication by reciprocal.
The Recognition Composition Law (RCL) on such a map $F$ is the discrete form of $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Doubling the trace converts that into the multiplicative d'Alembert shape $T(xy)+T(x/y)=T(x)T(y)$. The upstream result doubledTrace_dAlembert_of_rcl states exactly that identity from RCL alone: "The doubled-trace form of the composition law needs only the RCL. The anchor at two is not used."
PRCNativeCostHypotheses packages reciprocal symmetry, normalization invariance, and a canonical RCL field (plus a two-calibration that rules out the zero cost). nativeCostDoubledTrace F is the doubled-trace built from that pack.
proof idea
One-line wrapper. Feed the native pack's canonical_rcl field into doubledTrace_dAlembert_of_rcl, together with the nonzero-display hypotheses on $x$ and $y$. No extra algebra: the RCL-only theorem already delivers cross-equality of the summed doubled traces on $xy$ and $x/y$ against the product of the doubled traces on $x$ and $y$.
why it matters
Sits in the Cost real-character factorization path: it specializes the RCL-only d'Alembert form to the native cost pack so later character and uniqueness arguments can quote a clean multiplicative identity without reopening the full hypothesis structure. The parent module is building real ratio characters and cost-from-character reconstructions (siblings such as PRCRealRatioCharacter, costFromRealCharacter, and the sans-anchor variant).
Framework landmark: this is the discrete rational surface form of the Recognition Composition Law that forces the unique J-cost (T5: $J(x)=(x+x^{-1})/2-1$). Doubling the trace is the standard passage from the additive RCL to the multiplicative d'Alembert equation used in character factorization. No downstream users are wired yet in the graph; the lemma is infrastructure for the native-cost uniqueness and real-completion bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.