jq_eq_two_cases
plain-language theorem explainer
On nonzero rationals, the native J-display equals its value at 2 only at x=2 and x=1/2. Anyone calibrating structural cost characters on positive integer orbits cites this uniqueness. The proof reduces jq x = jq 2 to a quadratic, factors it, and splits on the zero-divisor law.
Claim. Let $x\in\mathbb{Q}$ with $x\neq 0$. If $J(x)=J(2)$, where $J(t)=(t+t^{-1})/2-1$, then $x=2$ or $x=2^{-1}$.
background
In the Primitive Recognition Calculus ledger, the rational J-display is $$J_q(t)=\frac{t+t^{-1}}{2}-1,$$ the restriction of the unique cost functional forced by the Recognition Composition Law (T5). It is nonnegative for $t\neq 0$, vanishes only at $\pm 1$, and is invariant under $t\mapsto t^{-1}$.
The module builds a structural native-cost ledger on ratio orbits. Values of $J_q$ at small integers serve as calibration anchors: $J_q(2)=1/4$ is computed by direct arithmetic (jq_two). The present lemma classifies the full preimage of that anchor on $\mathbb{Q}^\times$.
Upstream, the zero-divisor property on the logic integers (and hence on $\mathbb{Q}$) supplies the case split once the equation is rewritten as a product equal to zero.
proof idea
Rewrite the hypothesis with $J_q(2)=1/4$ and unfold $J_q$. Clear denominators to obtain the linear relation $4(x+x^{-1})-8=2$. Using $x\cdot x^{-1}=1$, rearrange into the quadratic identity $$(x-2)(2x-1)=0.$$ Apply the zero-divisor law: either $x-2=0$ or $2x-1=0$. The first branch is $x=2$; the second is $x=1/2=2^{-1}$. All steps are field simplification, linear arithmetic, and one nonlinear arithmetic call.
why it matters
Downstream, structural_character_calibrated_on_positive_integers (the round-5 engine) asserts that any character attached to a structural native cost agrees with the identity display on every positive integer orbit, up to reciprocal orientation invisible to the cost. That calibration needs to know that matching $J_q$ at the integer 2 forces the orbit representative to be 2 or its reciprocal; this lemma is exactly that uniqueness step.
In the broader forcing chain, $J$ is the unique cost (T5) and $\varphi$ is its self-similar fixed point (T6). Pinning level sets of $J_q$ on $\mathbb{Q}^\times$ is the arithmetic skeleton on which integer-orbit characters are later identified, before the eight-tick and $D=3$ layers attach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.