jq_rcl
plain-language theorem explainer
The rational J-display obeys the Recognition Composition Law for every nonzero pair of rationals. Anyone assembling power-generated or signed-power native costs on gauge orbits cites this identity as the algebraic engine. The proof unfolds the closed form and finishes by field simplification plus ring arithmetic.
Claim. Let $J_{\mathbb{Q}}(t)=\frac{t+t^{-1}}{2}-1$ on $\mathbb{Q}$. For all $x,y\in\mathbb{Q}\setminus\{0\}$, $J_{\mathbb{Q}}(xy)+J_{\mathbb{Q}}(x/y)=2J_{\mathbb{Q}}(x)J_{\mathbb{Q}}(y)+2J_{\mathbb{Q}}(x)+2J_{\mathbb{Q}}(y)$.
background
In the primitive recognition calculus the native cost is displayed on rationals by the closed form $J_{\mathbb{Q}}(t)=(t+t^{-1})/2-1$. This is the rational shadow of the unique J-cost forced at T5 in the unified forcing chain (equivalently $\cosh(\log t)-1$ on positives). The same algebraic shape appears as the Recognition Composition Law (RCL) in the framework primer: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
The present module builds a structural ledger of native-cost identities on ratio orbits and displays. Nonzero rationals are required so that inverses and quotients stay defined; the display itself is a pure rational expression, so no analytic completion is needed for the identity.
Upstream, the display is the local definition jq. Downstream cost constructions treat RCL as the reason a whole power family of native costs can be generated from a single base character while preserving the ledger hypotheses.
proof idea
Term-level tactic proof with no external lemmas. Unfold the display definition on each of the four occurrences, clear denominators with field simplification (using $x\neq 0$ and $y\neq 0$), then close the resulting polynomial identity by ring normalization. No case splits and no positivity hypotheses beyond nonzeroness.
why it matters
This is the RCL identity on rational displays, the algebraic license for power families of native costs. It is consumed by powerGeneratedNativeCost_base and signedPowerNativeCost_base, which package reciprocal and related ledger hypotheses for power-generated and signed-power native costs on ratio orbits; both rewrite through the display and rely on the composition law (together with the reciprocal identity for the display) to stay inside the native-cost hypothesis interface.
In the Recognition framework this is exactly the composition law that makes J the unique cost compatible with multiplicative structure (T5 J-uniqueness, and the RCL landmark). Without it the gauge-orbit cost constructions cannot promote a single base display to an integer power family while keeping the structural ledger intact. The result is fully proved; it closes no sorry, it simply supplies the identity those parents quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.