doubledTrace_dAlembert_of_sansAnchor
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the doubled-trace cost T satisfies the multiplicative d'Alembert law: T(xy)+T(x/y) equals T(x)T(y) as ratio orbits under cross-multiplication. Cited by anyone closing real-character factorization of the cost, or transporting the identity to rational displays. Proof is a one-line wrapper: extract the RCL clause from the hypothesis pack and apply the RCL-only d'Alembert lemma.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the anchor-free native-cost pack (base composition without the anchor at two, sign-reversing, monotone, zero-calibrated doubled trace). Write $T$ for the doubled-trace native cost of $F$. For ratio orbits $x,y$ with nonzero rational displays, $$T(xy)+T(x/y)\;\equiv\;T(x)\,T(y)$$ under cross-multiplication equality of ratio orbits.
background
Ratio orbits are the PRC internal display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality is not bare structural equality; crossEq is the K4.10 cross-multiplication relation (balanced scaled numerators), which agrees with ordinary rational equality of the verifier displays toRat.
The Recognition Composition Law (RCL) is the functional equation forced on the cost. For the doubled-trace form $T$ built from a native cost $F$, RCL rearranges into the multiplicative d'Alembert identity $T(xy)+T(x/y)=T(x)T(y)$, the same algebraic shape that $x+x^{-1}$ satisfies. Division of ratio orbits is multiplication by the reciprocal.
SansAnchorHypotheses is the anchor-free pack matching the structural native-cost hypotheses without fixing the value at two: it bundles a base-sans-two clause (which carries a canonical RCL), sign-reversal, monotonicity, and zero-calibration of the doubled trace. Upstream, doubledTrace_dAlembert_of_rcl already proves the identity from RCL alone; the anchor at two is not used.
proof idea
One-line term wrapper. From hF : SansAnchorHypotheses F project hF.base_sans_two.canonical_rcl to obtain the RCL hypothesis on $F$, then apply doubledTrace_dAlembert_of_rcl at the given nonzero displays hx, hy. No extra algebraic work happens at this site.
why it matters
This is the bridge from the abstract hypothesis pack to the concrete d'Alembert identity used by the corrected factorization target. Downstream, traceDisplay_dAlembert transports the same identity to ordinary rational arithmetic on the verifier display, and SansAnchorRealCharacterFactorizationTarget_proved uses the pack to show that every anchor-free doubled trace factors through a real-valued principal character (candidate character, cost agreement, small-trace rationality).
In the Recognition framework this is the cost-side shadow of T5 (J-uniqueness) and the RCL $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$: the doubled trace is the linear change of variables that turns RCL into pure multiplicative d'Alembert, the functional equation solved by $x\mapsto x+x^{-1}$ and hence by $\cosh\circ\log$. Dropping the anchor at two keeps the factorization target honest: uniqueness and calibration are handled by the remaining pack clauses, not by a hard-wired value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.