qreciprocal
plain-language theorem explainer
The reciprocal of a rational recognition event swaps its source and target agents and inverts the posted ratio. Cosmogenesis simulation code cites it to enforce double-entry bookkeeping on the ledger. Construction is a one-line structure rebuild: target becomes source, source becomes target, ratio is inverted.
Claim. Given a recognition event $e$ over $\mathbb{Q}$ with source $s$, target $t$, and ratio $r$, its reciprocal is the event with source $t$, target $s$, and ratio $r^{-1}$.
background
This module supplies a computable cosmogenesis over $\mathbb{Q}$ that mirrors the real-valued dynamics of PreBigBang and FirstTick. The recognition ledger is kept as an exact Lean object one can #eval, with conservation proved in the kernel.
A QEvent is a triple (source agent, target agent, ratio in $\mathbb{Q}$), the rational mirror of a LedgerForcing.RecognitionEvent. The canonical recognition cost on positive ratios is $J(x)=(x+x^{-1})/2-1$, which is reciprocal-symmetric: $J(x)=J(x^{-1})$. Double-entry posting therefore pairs every event with its reciprocal so that cost increments by exactly $2J(r)$ and the multiplicative flow product at each agent is unchanged.
Upstream cost definitions (observer forcing, multiplicative recognizer L4, rung coarsening) all treat event cost as this $J$-cost; the rational mirror inherits the same algebraic identity.
proof idea
Pure definition: rebuild the QEvent structure by swapping the two agent fields and taking the field inverse of the ratio. No lemmas, no tactics.
why it matters
Double-entry is the ledger invariant that makes cosmogenesis conservation computable. addEvent posts an event together with this reciprocal. qcost_addEvent then shows the cost rises by exactly $2\cdot J(r)$ via reciprocal symmetry of $J$. flowContribution_pair shows an event and its reciprocal contribute a factor $r\cdot r^{-1}=1$ at every agent, so the flow product is invariant under posting.
That invariance is the rational form of the conserved $\sigma$ quantity: after the full eight-tick cosmogenesis the flow product is exactly $1$ at every agent for any positive seed. The construction is the rational counterpart of the real ledger's reciprocal pairing and sits inside the T7 eight-tick octave story of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.