doubledTrace_dAlembert_of_rcl
plain-language theorem explainer
Any map F on ratio orbits that obeys the Recognition Composition Law has doubled trace T satisfying the multiplicative d'Alembert identity T(xy)+T(x/y)=T(x)T(y). Cited by anyone deriving real-character factorizations of cost from RCL alone, without the anchor at two. Proof reduces cross-equality to rational equality, unfolds the doubled-trace definition, and closes by linear arithmetic.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the Recognition Composition Law: whenever the rational displays of $x,y$ are nonzero, $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ under cross-multiplication equality. Then the doubled-trace transform $T_F$ obeys $T_F(xy)+T_F(x/y)=T_F(x)\,T_F(y)$ under the same cross-equality, for all such nonzero $x,y$.
background
Ratio orbits are the Primitive Recognition Calculus carriers of rational displays: each orbit has a verifier map toRat into $\mathbb{Q}$. Equality of displays is expressed internally by crossEq (K4.10): two orbits match when cross-multiplication of numerator and denominator signed orbits balances. The lemmas add_toRat, mul_toRat, and crossEq_iff_toRat_eq identify orbit arithmetic with ordinary rational arithmetic on displays.
The Recognition Composition Law (RCL) is the functional equation forced on the J-cost in the foundation chain: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Here it is stated abstractly for an arbitrary orbit map $F$, still written with orbit addition, multiplication, and the constant orbit two.
The doubled-trace transform packages $F$ into a quantity whose composition law is multiplicative rather than the quadratic RCL shape. Classically this is the passage from $J$ to $x+x^{-1}$ (equivalently $2J+2$), which converts RCL into d'Alembert form. The module works entirely in the PRC native cost setting and isolates which hypotheses are needed for that conversion.
proof idea
Term-mode proof, four steps. Instantiate the RCL hypothesis at the given nonzero $x,y$. Rewrite both the hypothesis and the goal via crossEq_iff_toRat_eq, so the claim becomes an equality of rational displays. Unfold nativeCostDoubledTrace and doubledTraceValue, then simplify with the display lemmas mul_toRat, add_toRat, two_toRat, and one_toRat. The resulting rational identity is discharged by linarith. No induction and no special value of $F$ at two.
why it matters
This is the RCL-only engine behind real character factorization of cost. Downstream, doubledTrace_dAlembert_of_native specializes it to the native cost pack (using only that pack's RCL field), and doubledTrace_dAlembert_of_sansAnchor does the same under the weaker sans-anchor hypothesis bundle. Both feed SansAnchorRealCharacterFactorizationTarget_proved, whose doc-comment states that "the anchor-free doubled trace always factors through a real-valued principal character."
In the framework landmarks this sits under T5 (J-uniqueness) and the Recognition Composition Law: once RCL holds, the doubled trace is a multiplicative character equation, so cost factors without invoking the normalization anchor at two. That separation is what lets the sans-anchor factorization target close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.