anchorRoot_add_inv
plain-language theorem explainer
Under anchor-free native-cost hypotheses on a ratio-orbit map F, the principal real root extracted from the doubled trace at 2, plus its reciprocal, equals that same trace value. Character-factorization and nontrivial-character lemmas cite this identity. The proof is a one-line application of the general real-trace-root add-inverse law after checking the bound 2 ≤ T_F(2).
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost pack (base without two, sign-reversing, monotone, and zero-calibrated doubled trace). Write $T_F$ for the rational doubled-trace display and $\rho_F$ for the principal real root of $T_F(2)$. Then $\rho_F + \rho_F^{-1} = T_F(2)$.
background
In the real-character factorization module, cost data on ratio orbits are packaged without a fixed numerical anchor. The structure SansAnchorHypotheses collects the base axioms minus the two-anchor, plus sign-reversal, monotonicity, and zero-calibration of the doubled trace. The rational doubled trace $T_F$ evaluates that display on rational points via the ratio-orbit embedding.
The principal root at two is defined by feeding $T_F(2)$ into the real-trace-root extractor: $\rho_F := \mathrm{realTraceRoot}(T_F(2))$. Upstream, realTraceRoot_add_inv states that whenever $t \ge 2$, the root $r$ of that $t$ satisfies $r + r^{-1} = t$. Separately, traceDisplay_two_ge_two supplies the needed lower bound $2 \le T_F(2)$ from the anchor-free pack (via the positive-integer comparison at two).
The local setting is the passage from native PRC cost axioms to a real multiplicative character on nonzero rationals, with the value at two serving as the distinguished generator of the character.
proof idea
One-line wrapper. Apply the general identity realTraceRoot_add_inv to $t = T_F(2)$. The side condition $2 \le t$ is discharged by traceDisplay_two_ge_two hF, rewritten through the definition of rationalTrace via simpa. No further algebraic work is needed: the root-plus-inverse law already returns $t$.
why it matters
This identity is the bridge from the abstract real-trace-root calculus to the concrete anchor root used throughout the character factorization. Downstream it feeds anchorRoot_gt_one (strict inequality once the trace is nondegenerate), and the family of nontrivial-character lemmas: unit value at one, multiplicativity, reciprocal-sum recovery of the trace, and the evaluation at two itself equaling the anchor root.
In the Recognition framework this sits inside the cost layer that realizes the unique J-cost (T5) and the Recognition Composition Law on real characters. The add-inverse relation is exactly the hyperbolic identity behind $J(x) = (x + x^{-1})/2 - 1$, so fixing $\rho_F + \rho_F^{-1} = T_F(2)$ pins the character generator that later yields the native cost uniqueness path. It is fully proved scaffolding for the nontrivial-character package rather than an open interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.