traceRootDenominator
plain-language theorem explainer
The ratio-orbit constant three, assembled as two plus one, serving as the denominator in the linear root formula that recovers a multiplicative character from a doubled trace. Native-cost uniqueness arguments cite it whenever they write χ(q)=(2T(2q)−T(q))/3. The body is a one-line orbit addition of the already-defined constants two and one.
Claim. Define the constant ratio orbit $3 := 2 + 1$. It is the denominator appearing in the linear root extraction $\chi(q) = (2\,T(2q) - T(q))/3$ that recovers a multiplicative character from a doubled-trace functional $T$.
background
In the primitive recognition calculus, rational values are carried by RatioOrbit: an integer numerator over a nonzero distinction-orbit denominator (K4.7). The constant two is the ratio orbit with numerator the signed orbit of two and denominator one; one is the unit ratio orbit. Their sum is therefore the orbit display of three.
The surrounding module develops native-cost uniqueness by matching a cost functional to a character via doubled traces. If $T(q)=\chi(q)+\chi(q)^{-1}$ and the axis value $\chi(2)=2$ is fixed, algebraic rearrangement yields the linear root $\chi(q)=(2T(2q)-T(q))/3$. The present definition packages that denominator as a first-class ratio orbit so later arithmetic stays inside the orbit type.
proof idea
One-line definition: form the sum of the ratio-orbit constants two and one via the orbit addition operation. No proof obligations; the structure fields (numerator, denominator, nonzero witness) are inherited from the sum constructor.
why it matters
Supplies the denominator constant consumed by the linear root candidate that extracts $\chi$ from a doubled trace $T$ at the distinguished axis two. Downstream, a simp lemma reduces the orbit to the ordinary rational three, and the root candidate itself feeds the character-trace matching lemmas that force native cost uniqueness.
In the broader Recognition chain this sits under J-cost uniqueness (T5) and the Recognition Composition Law: once the doubled-trace functional is known to obey a d'Alembert identity with axis value two, the only consistent multiplicative character is the one recovered by this root, pinning the native cost to the unique J-shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.