traceDisplay_recip
plain-language theorem explainer
Under the anchor-free native-cost hypotheses on a ratio-orbit map F, the real trace display is invariant under reciprocal of the orbit: the displayed cost of q and of q^{-1} agree. Cost and character-factorization arguments cite this to pass reciprocity from the carrier doubled trace down to the real display. The proof applies doubled-trace congruence for the reciprocal base map, converts cross-equality to rational equality, and casts.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). For every ratio orbit $q$, the real trace display of $F$ at the reciprocal orbit equals the display at $q$: $\mathrm{tr}_F(q^{-1})=\mathrm{tr}_F(q)\in\mathbb{R}$.
background
In the real character factorization of native cost, ratio orbits package a signed integer numerator over a nonzero distinction-nat denominator, with a rational verifier display toRat. The reciprocal of an orbit swaps the recognition direction in the usual way (inverse ratio).
The doubled native cost of a map $F$ on orbits is projected to a real by traceDisplay: cast the carrier doubled-trace value to a rational, then to $\mathbb{R}$. The hypothesis pack SansAnchorHypotheses is the anchor-free structural pack on $F$: base-sans-two, sign-reversing and monotone native cost, and zero calibration of the doubled trace.
Upstream, cross-multiplication equality of orbits is equivalent to equality of their rational displays (crossEq_iff_toRat_eq). Reciprocity of the base-sans-two data supplies a doubled-trace congruence between $q$ and its reciprocal, which is the algebraic input this lemma turns into real equality.
proof idea
Obtain doubled-trace congruence from the reciprocal instance of the base-sans-two field of the hypothesis pack: doubledTraceValue_congr (hF.base_sans_two.reciprocal q). Rewrite that congruence via crossEq_iff_toRat_eq so it becomes equality of rational displays. Unfold traceDisplay and nativeCostDoubledTrace, then finish by exact_mod_cast on the symmetric equality. Short term-mode reduction: carrier reciprocity to rational equality to real cast.
why it matters
Reciprocal invariance is the hallmark of the RS cost $J(x)=(x+x^{-1})/2-1$ (T5 J-uniqueness / RCL): cost cannot prefer a ratio over its inverse. This lemma pushes that symmetry from the carrier doubled trace down to the real display used in character factorization.
It is consumed immediately by rationalTrace_recip, which lifts the same identity to the rational-trace interface: rationalTrace F x^{-1} = rationalTrace F x. That step is part of matching the real character of native cost to the unique J-cost without an external anchor, inside the Cost.RealCharacterFactorization development fed by PRC native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.