traceRootCandidate_recip_toRat_of_nonzero
plain-language theorem explainer
For a doubled-trace map T on ratio orbits that obeys the native PRC hypotheses and respects cross-equivalence, the rational display of the trace-root candidate at the reciprocal of q equals the display of T(q) minus the display of the root candidate at q (whenever q is nonzero). Cost-uniqueness proofs cite this when closing the reciprocal half of the quadratic root identity. The argument evaluates d'Alembert at the orbit two against q, transports values across cross-equivalence, and finishes by linear arithmetic on rationals.
Claim. Let $T$ be a map on ratio orbits satisfying the doubled-trace hypotheses (reciprocity, d'Alembert identity, unit and two-point normalizations) and respecting cross-equivalence of orbits. For every ratio orbit $q$ with nonzero rational display, the rational display of the trace-root candidate of $T$ at the reciprocal of $q$ equals the rational display of $T(q)$ minus the rational display of the trace-root candidate at $q$.
background
In the Primitive Recognition Calculus, ratio orbits are the internal carriers of rational displays: each orbit $q$ has a verifier value $q.\mathrm{toRat}\in\mathbb{Q}$. Two orbits are identified by cross-equivalence (cross-multiplication of numerator and denominator signed orbits), which is equivalent to equality of those rational displays.
A doubled-trace map $T$ is the native PRC stand-in for twice a cost character. The structure of doubled-trace hypotheses packages reciprocity ($T(q)$ cross-equivalent to $T(1/q)$), a d'Alembert functional equation, and fixed normalizations at the unit and at the orbit two. Quotient respect further requires that cross-equivalent inputs yield cross-equivalent $T$-values, so $T$ descends to the rational quotient.
The trace-root candidate is the algebraic half-step that recovers a putative root of the quadratic whose doubled trace is $T$. Upstream lemmas identify cross-equivalence with rational equality and transport addition and multiplication of orbits to ordinary rational arithmetic, which is what lets the present identity be stated entirely on $\mathbb{Q}$.
proof idea
First, reciprocity of $T$ and the nonzero hypothesis give that the reciprocal orbit is nonzero and that $T(1/q)$ has the same rational display as $T(q)$. The two-point normalization, rewritten through the native doubled-trace value, forces $(T(\mathrm{two})).\mathrm{toRat}=5/2$.
Cross-equivalence of $\mathrm{two}\cdot(1/q)$ with $\mathrm{two}/q$, together with quotient respect, equates their $T$-displays. d'Alembert at $(\mathrm{two},q)$ then yields $(T(\mathrm{two}\cdot q))+ (T(\mathrm{two}/q)) = (T,\mathrm{two})\cdot(T q)$ on rationals, hence the sum equals $(5/2)\cdot(T q)$.
Unfolding the root-candidate formula at both $q$ and $1/q$, substituting the transported values, and applying linear arithmetic closes the identity.
why it matters
Native cost uniqueness in PRC aims to force the doubled trace (and then the cost itself) to match the unique J-cost character coming from the Recognition Composition Law and the T5 forcing step. The root candidate is the bridge from the doubled-trace functional equation back to a linear character on the ratio ladder.
This reciprocal identity is the exact algebraic half needed by the two immediate parents: the theorem that the root candidate itself is reciprocal under the quadratic-target hypotheses, and the theorem that the root candidate reproduces the trace under those same hypotheses plus zero-calibration. Without the rational reciprocal relation, the quadratic-target package cannot close on both $q$ and $1/q$.
In the broader forcing chain the result sits inside the foundation layer that pins the cost functional before phi, the eight-tick octave, and $D=3$ are read off. It is a proved lemma, not scaffolding: it discharges a concrete arithmetic obligation rather than leaving a hypothesis interface open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.