rationalTrace_recip
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the rational doubled-trace display is invariant under reciprocal: T(x^{-1}) = T(x) for every rational x. Anyone building multiplicative characters from the doubled trace cites this reciprocity. The proof reduces to orbit reciprocity of the display after identifying the rational reciprocal with the orbit reciprocal via cross-equality.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base without the two-anchor, sign-reversing, monotone, and zero-calibrated doubled trace). For every rational $x$, the rational doubled-trace display of $F$ at $x^{-1}$ equals its value at $x$: $T_F(x^{-1}) = T_F(x)$.
background
This module builds a real character factorization of the native recognition cost on ratio orbits. The carrier-valued doubled trace is projected to a real by traceDisplay: convert the doubled-trace value to a rational, then to $\mathbb{R}$. The rational display rationalTrace F x is that real evaluated on the ratio orbit of the rational $x$.
SansAnchorHypotheses F packages the structural assumptions used throughout: a base law without a distinguished two-anchor, sign-reversal, monotonicity, and zero-calibration of the doubled trace. Upstream, traceDisplay_recip already gives reciprocity on orbits: the display of the reciprocal orbit equals the display of the orbit. Cross-equality of orbits is equivalent to equality of their rational verifier displays (crossEq_iff_toRat_eq).
The local goal is to lift orbit-level reciprocity to an honest function of rational arguments, so later character identities can be written in ordinary $\mathbb{Q}$ notation.
proof idea
Unfold both sides to traceDisplay on the corresponding ratio orbits. First identify the orbit of $x^{-1}$ with the reciprocal of the orbit of $x$: apply traceDisplay_eq_of_crossEq under the anchor-free pack, feeding a cross-equality proved by rewriting through crossEq_iff_toRat_eq, the toRat round-trips for ratioOrbitOfRat, and recip_toRat. The resulting display of the reciprocal orbit equals the original display by the upstream lemma traceDisplay_recip.
why it matters
Reciprocity of the rational doubled trace is the bridge from orbit-level native-cost structure to multiplicative character calculus on $\mathbb{Q}$. Downstream, nontrivialCharacterValue_recip_sum uses it to relate the sum of a nontrivial character value and its reciprocal to the rational trace, and nontrivialCharacterValue_mul sits in the same factorization chain for products.
In Recognition Science this is cost-side infrastructure for the unique $J$-cost (forcing step T5) and the Recognition Composition Law: the doubled trace is the real character whose d'Alembert-type identities encode $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Without rational reciprocity, the character cannot be treated as an even function of the log-ratio, which is required for the cosh form $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.