nativeCostDoubledTrace_dAlembert_of_native_hypotheses
plain-language theorem explainer
If a cost map F on ratio orbits meets the native PRC cost hypotheses, its doubled trace T_F = 2(F+1) obeys the native d'Alembert equation (RCL in multiplicative form). Anyone proving uniqueness of the native cost from the doubled-trace character cites this. The proof pulls the canonical RCL off the hypotheses, rewrites to rational equality, unfolds the orbit arithmetic, and closes by ring/linarith.
Claim. Let $F$ be a map on ratio orbits satisfying the native PRC cost hypotheses. Write $T_F := 2(F+1)$ for its doubled trace. Then for all ratio orbits $x,y$ with nonzero rational displays, the cross-equation $T_F(xy)+T_F(x/y)=T_F(x)\,T_F(y)$ holds on ratio orbits.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: equivalence classes of signed integer ratios with a rational display toRat. The Recognition Composition Law (RCL) is the functional equation that forces the J-cost in the continuous setting (T5 of the forcing chain). After the change of dependent variable $T=2(F+1)$, RCL becomes the multiplicative d'Alembert equation $T(xy)+T(x/y)=T(x)T(y)$.
PRCDoubledTraceDAlembert is exactly that identity written natively: both sides are compared by the orbit cross-equation (cross-multiplication of numerators and denominators), which by crossEq_iff_toRat_eq is equivalent to equality of rational displays. The doubled-trace constructor nativeCostDoubledTrace builds $T_F$ from $F$ via doubledTraceValue.
The hypothesis bundle PRCNativeCostHypotheses F already carries a canonical RCL instance on $F$ (field canonical_rcl). This lemma simply transports that instance across the $T=2(F+1)$ change of variable, staying entirely inside the RatioOrbit algebra (add_toRat, mul_toRat, one_toRat).
proof idea
Tactic proof, not a wrapper. Introduce nonzero-display orbits $x,y$ and pull hF.canonical_rcl hx hy as the RCL identity for $F$. Rewrite both that hypothesis and the goal through RatioOrbit.crossEq_iff_toRat_eq, converting orbit cross-equations into ordinary rational equalities. Unfold nativeCostDoubledTrace, doubledTraceValue, and the orbit arithmetic lemmas (add_toRat, mul_toRat, two_toRat, one_toRat) on both sides. Normalize by ring_nf, then close the resulting linear relation with linarith. The only substantive input is the canonical RCL field of the native-cost hypotheses; everything else is display arithmetic.
why it matters
This is the RCL-to-d'Alembert transport step inside native cost uniqueness for the Primitive Recognition Calculus. Downstream, nativeCostDoubledTrace_hypotheses_of_native_cost_hypotheses packages the full PRCDoubledTraceHypotheses bundle for $T_F$; the present lemma discharges the d'Alembert component of that package.
In the broader framework it is the discrete, orbit-level avatar of the Recognition Composition Law that forces J-uniqueness (forcing-chain T5: $J(x)=(x+x^{-1})/2-1$). Once the doubled trace is known to be a d'Alembert solution and to match the cost character, uniqueness of the native cost follows from the classical uniqueness theory for the multiplicative d'Alembert equation on positive rationals. Without this transport, the native-cost hypotheses would not speak the same language as the doubled-trace uniqueness pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.