jq_two
plain-language theorem explainer
Evaluates the rational J-display at 2 and obtains the constant 1/4. Cited by anyone characterizing level sets of the native cost on rationals, especially the two-root case analysis at height J(2). Proof is a one-line numerical normalization of the definition of jq.
Claim. For the rational J-display $J_{\mathbb{Q}}(t)=\frac{t+t^{-1}}{2}-1$, one has $J_{\mathbb{Q}}(2)=\frac{1}{4}$.
background
In the Primitive Recognition Calculus, the native cost is displayed on rationals by the same algebraic form forced at T5: $J(t)=(t+t^{-1})/2-1$ (equivalently $\cosh(\log t)-1$ on positives). The local definition jq is exactly that map $\mathbb{Q}\to\mathbb{Q}$.
The structural ledger module records elementary closed values and sign/ordering facts for this display, so later uniqueness and minimality arguments can quote concrete constants rather than re-expand the formula. The ratio-orbit constant two is the integer 2 viewed as a ratio of distinction data; here only its underlying rational 2 is needed.
Upstream, jq is the bare definition; no deep lemma is required to evaluate it at a concrete nonzero rational.
proof idea
One-line term/tactic proof: norm_num after unfolding jq. Substituting $t=2$ gives $(2+2^{-1})/2-1=(5/2)/2-1=5/4-1=1/4$, discharged by rational arithmetic normalization. No external lemmas beyond the definition.
why it matters
Feeds jq_eq_two_cases, which classifies all nonzero rationals with $J_{\mathbb{Q}}(x)=J_{\mathbb{Q}}(2)$ as $x=2$ or $x=2^{-1}$. That case split is the ledger-level avatar of the symmetry $J(x)=J(x^{-1})$ built into the Recognition Composition Law and the T5 unique cost $J(x)=(x+x^{-1})/2-1$.
Pinning the numerical height $J(2)=1/4$ keeps later inequalities (values strictly between 1 and 2 lie below this height) and orbit comparisons free of field-simp noise. In the broader forcing chain this is bookkeeping for the unique J-cost, not a new physical claim, but without the constant the two-root characterization cannot even state its target level set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.