qJ
plain-language theorem explainer
The rational recognition cost is the familiar J-function J(x)=(x+x^{-1})/2-1, now valued in ℚ rather than ℝ. Cosmogenesis simulation and ledger-cost lemmas cite it as the per-event cost kernel. The body is a one-line definition mirroring the unique T5 cost.
Claim. For any rational $x$, the recognition cost is $J(x) = \frac{x + x^{-1}}{2} - 1$, taking values in $\mathbb{Q}$.
background
Recognition Science forces a unique nonnegative cost on positive ratios: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ (forcing chain T5). The same algebraic expression appears as event cost in ObserverForcing, as ledger fold in LedgerForcing, and as derived comparator cost for multiplicative recognizers.
This module rebuilds PreBigBang/FirstTick cosmogenesis over $\mathbb{Q}$ so the simulation is #eval-able and conservation is kernel-checked. Events carry rational ratios; double-entry posts each event with its reciprocal. The cost of a list of events is the sum of $J$ on those ratios.
Upstream cost defs (RungCoarsen, LedgerForcing, MultiplicativeRecognizer, ObserverForcing, RecognizerBridge) all instantiate the same $J$ on $\mathbb{R}$ or quotient types. Here the codomain is $\mathbb{Q}$, so arithmetic stays exact and Fibonacci convergents of the self-similar recurrence remain rational.
proof idea
Pure definition: expand the arithmetic expression $(x + x^{-1})/2 - 1$ at a rational argument. No lemmas, no tactics. Downstream proofs unfold it and rewrite (e.g. reciprocal symmetry by inv_inv and ring, positivity by rewriting as $(x-1)^2/(2x)$).
why it matters
This is the computable mirror of the T5 J-cost inside the cosmogenesis simulator. Total ledger cost qcost is the sum of qJ over event ratios; qcost_addEvent shows each double-entry post raises cost by exactly $2J(r)$, matching FirstTick. Reciprocal symmetry qJ_recip and positivity qJ_pos (for $x>0$, $x\neq 1$) feed first-tick positivity for the seed-2 run and the TraceCertificates path.
Without a rational $J$, the eight-tick conservation story and the exact Fibonacci approach to $\varphi$ would stay noncomputable over $\mathbb{R}$. The def anchors the module's claim that the recognition ledger is mirrored exactly over $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.