traceRootCandidate_zero
plain-language theorem explainer
The linear root candidate extracted from a split-trace map on ratio orbits vanishes at the zero orbit. Anyone reconstructing the multiplicative character from a doubled-trace functional needs this origin calibration before evaluating the formula elsewhere. The proof is a one-line rewrite: the definition branches on toRat, and the zero orbit maps to rational 0.
Claim. For every map $T$ from ratio orbits to ratio orbits, the trace-root candidate of $T$ at the zero orbit equals the zero orbit.
background
Ratio orbits are the PRC display of rationals: a signed-orbit numerator over a nonzero distinction-natural denominator. The zero orbit is the distinguished origin; the simp fact zero_toRat records that it embeds to the ordinary rational $0$.
The trace-root candidate is the linear reconstruction forced by a split-trace identity $T(q)=\chi(q)+\chi(q)^{-1}$ with axis normalization $\chi(2)=2$. Away from zero one recovers $\chi(q)=(2\cdot T(2q)-T(q))/3$; at zero the definition hard-wires the repaired zero-calibration field and returns the zero orbit.
The surrounding module develops native-cost uniqueness: cost-from-character constructions, doubled-trace d'Alembert hypotheses, and character-trace matching on the ratio-orbit lattice.
proof idea
One-line wrapper. Rewrite by the definition of the trace-root candidate. The guard is q.toRat = 0; RatioOrbit.zero_toRat discharges it, so if_pos selects the zero branch and the goal is immediate. No property of $T$ is used.
why it matters
Fixes the origin of the reconstructed multiplicative character before any uniqueness argument for the native cost can run. Sibling material in the same module (cost-from-character, doubled-trace d'Alembert, character-trace matching) assumes a well-defined root candidate on the whole ratio lattice; without zero calibration the formula is either undefined or inconsistent at the origin. No recorded downstream dependents yet; the lemma is the base case for evaluating the candidate along the lattice. It supports the T5 J-uniqueness pathway indirectly, by keeping character-trace data compatible with the recognition composition law at the calibrated zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.