qJ_recip
plain-language theorem explainer
Reciprocal symmetry of the rational recognition cost: J(x^{-1}) equals J(x) for every rational x. Cosmogenesis and ledger proofs cite it when a paired event and its reciprocal must contribute the same cost. The proof unfolds the definition, rewrites the double inverse, and closes by ring arithmetic.
Claim. For every rational $x$, $J(x^{-1}) = J(x)$, where the rational recognition cost is $J(x) = \frac{x + x^{-1}}{2} - 1$.
background
The module CosmogenesisSim is a computable, kernel-checked mirror of the real-valued PreBigBang and FirstTick dynamics, run over $\mathbb{Q}$ so the simulation can be #eval'd with conservation proved in the kernel.
The canonical cost on rationals is $J(x) = (x + x^{-1})/2 - 1$, the same functional form forced uniquely by the Recognition Composition Law (T5). Events are posted double-entry: each QEvent is accompanied by its reciprocal (source/target swapped, ratio inverted). Total ledger cost qcost is the sum of $J$ over posted ratios.
Reciprocal symmetry is the algebraic fact that makes the paired contribution collapse to $2J(r)$ rather than $J(r)+J(r^{-1})$ with two independent terms.
proof idea
Term-mode, three steps. Unfold qJ to expose $(x + x^{-1})/2 - 1$. Rewrite with inv_inv so $(x^{-1})^{-1}$ becomes $x$. The two sides are then identical rational expressions; ring closes the equality.
why it matters
Feeds directly into qcost_addEvent: posting one paired event raises total cost by exactly $2\cdot J(\mathrm{ratio})$. That increment is the rational mirror of FirstTick.ledger_cost_add_event and is the per-tick cost step in the eight-tick cosmogenesis ledger.
In the forcing chain this is the rational shadow of T5 J-uniqueness: the same $J$ that satisfies the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is automatically even under $x\mapsto x^{-1}$. Without this identity the double-entry conservation argument (flow product multiplies by $r\cdot r^{-1}=1$) would not line up with the additive cost ledger.
It is a small algebraic lemma, but every later qcost identity in the cosmogenesis simulation routes through it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.