PRCDoubledTraceDAlembert
plain-language theorem explainer
Defines the native d'Alembert equation for a doubled-trace map T on ratio orbits: T(xy)+T(x/y) is cross-equal to T(x)T(y) whenever the rational displays of x and y are nonzero. This is the Recognition Composition Law rewritten after the change of unknown T_F=2(F+1). Cited by the native-cost uniqueness chain when packaging hypotheses on the doubled trace. Pure Prop definition; no proof content.
Claim. A map $T$ from ratio orbits to ratio orbits satisfies the doubled-trace d'Alembert property when, for all ratio orbits $x,y$ with nonzero rational displays, $T(xy)+T(x/y)$ is equivalent under cross-multiplication to the product $T(x)\,T(y)$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of two such displays is internal cross-multiplication (crossEq): the scaled numerators balance as signed orbits. Division of orbits is multiplication by reciprocal. The verifier map toRat only displays the orbit as a classical rational; the native relation is always crossEq.
The Recognition Composition Law (RCL) is the functional equation that forces the J-cost in the forcing chain (T5). After the affine change of unknown $T_F=2(F+1)$, RCL becomes the classical d'Alembert form $T(xy)+T(x/y)=T(x)T(y)$. This definition records that equation on ratio orbits, with products and sums taken in the orbit algebra and equality read via crossEq.
The ambient module develops uniqueness of the native PRC cost from character and trace data; the doubled-trace packaging sits between raw native-cost hypotheses and the character-trace matching lemmas.
proof idea
Definition only: a Prop-valued abbreviation. The body is a universal quantifier over ratio orbits with nonzero toRat displays, asserting crossEq between the orbit-sum of $T$ on the product and the quotient, and the orbit-product of the two $T$-values. No tactics, no lemmas applied.
why it matters
Packages the RCL in doubled-trace variables so the native-cost uniqueness argument can treat d'Alembert as a named hypothesis rather than an expanded formula. Downstream, nativeCostDoubledTrace_dAlembert_of_native_hypotheses shows that any $F$ satisfying the native cost hypotheses induces a doubled trace $T=\mathrm{nativeCostDoubledTrace},F$ that meets this Prop (by invoking the canonical RCL clause of those hypotheses). The structure PRCDoubledTraceHypotheses then bundles this d'Alembert clause with reciprocal symmetry and normalization invariance.
In the broader framework this is the orbit-level form of the composition law that, with regularity, forces $J(x)=(x+x^{-1})/2-1$ (forcing step T5) and thereby the self-similar fixed point $\varphi$ (T6). It does not itself solve the functional equation; it only names the equation the uniqueness theorems discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.