traceRootCandidate_nonzero_of_quadratic
plain-language theorem explainer
If a doubled-trace map T satisfies the linear-root quadratic identity, then the associated root candidate never vanishes on nonzero ratio orbits. Anyone calibrating native cost uniqueness from doubled-trace data cites this nondegeneracy step. The proof is a short contradiction: the quadratic forces the product of the candidate and its complement to equal 1, so the candidate cannot be zero.
Claim. Let $T$ send ratio orbits to ratio orbits. Suppose that for every nonzero rational display $q$, the product of the trace-root candidate of $T$ at $q$ with the difference $T(q)$ minus that candidate equals $1$ (as ratio orbits). Then for every such $q$, the rational display of the trace-root candidate is nonzero.
background
In the primitive recognition calculus, ratio orbits are integer-numerator / nonzero-denominator displays of rationals. Their verifier map toRat lands in $\mathbb{Q}$, and cross-equality of two orbits is equivalent to equality of those rationals. Multiplication and subtraction of orbits push forward to ordinary rational arithmetic.
The doubled-trace linear-root quadratic target is the structural identity that the candidate root $r(q)$ of a map $T$ and its complement $T(q)-r(q)$ multiply to the unit orbit whenever $q$ is nonzero. That identity is the algebraic content of treating $r(q)$ as a root of the monic quadratic $X(T(q)-X)=1$ on the ratio-orbit monoid.
This lemma lives in the native-cost uniqueness module: one wants the doubled-trace character to determine a unique calibrated cost, which requires the candidate root used in the calibration never to collapse to zero on the nonzero locus.
proof idea
Term-mode contradiction on a fixed nonzero $q$. Instantiate the quadratic target at $q$ to obtain the cross-equality of the product of the candidate with $T(q)$ minus the candidate against the unit orbit. Rewrite that equality into rational arithmetic via cross-equality iff toRat equality, together with the pushforwards of multiplication, subtraction, and the unit. Substitute the assumption that the candidate's rational is zero; the left side becomes $0$, and norm_num closes $0=1$.
why it matters
Feeds directly into the proof that the zero-calibrated linear-root target for doubled traces holds: that parent theorem builds the quadratic target from native doubled-trace hypotheses and then needs nonvanishing of the candidate to finish the calibration. Without this step, the linear-root branch of native cost uniqueness could hit a degenerate root and fail to pin down a unique cost character.
In the broader Recognition stack this is bookkeeping inside the primitive recognition calculus that underwrites uniqueness of the native cost before the forcing chain identifies $J$ (T5) and $\varphi$ (T6). It does not itself force $J$ or the octave; it keeps the doubled-trace route to native cost free of zero-root pathologies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.