qcost
plain-language theorem explainer
Total ledger cost of a finite list of rational recognition events: sum the canonical J-cost of each event ratio. Cosmology and ledger auditors cite it when tracking cumulative cost across a cosmogenesis run. The body is a one-line map-and-sum over the rational J functional, mirroring the real-valued ledger cost from LedgerForcing.
Claim. For a finite list of recognition events with rational ratios $r_i$, the total ledger cost is $\sum_i J(r_i)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the canonical recognition cost over $\mathbb{Q}$.
background
This module supplies a computable, kernel-checked mirror of cosmogenesis over $\mathbb{Q}$. The real-valued dynamics live in PreBigBang and FirstTick; here every object is rational so the simulation is a Lean value one can #eval, with conservation proved in the kernel.
A recognition event carries a source agent, a target agent, and a positive rational ratio. The cost functional on a single ratio is the standard RS J-cost $J(x)=(x+x^{-1})/2-1$, forced uniquely by the Recognition Composition Law (forcing chain T5). Double-entry posting appends both an event and its reciprocal (source/target swapped, ratio inverted).
The total ledger cost is the sum of $J$ over every posted event. Its real counterpart is LedgerForcing.ledger_cost; the rational version is what the conservation and certificate theorems in this file consume.
proof idea
Pure definition: map each event to $J$ of its ratio, then take the list sum in $\mathbb{Q}$. No lemmas, no tactics. Downstream equalities (e.g. the paired-posting increment) unfold this definition and simplify with the reciprocal identity $J(r^{-1})=J(r)$.
why it matters
Gives the cumulative cost observable for the rational cosmogenesis ledger. The immediate parent is the paired-posting law: adding one double-entry event raises total cost by exactly $2J(r)$, mirroring FirstTick's real increment. Trace certificates for the canonical seed-2 run also depend on it (first-tick cost positivity and related checks).
In the broader framework this is the ledger-side accumulation of the T5 J-cost along the eight-tick octave (T7). Together with the multiplicative flow product (conserved at 1 under double-entry), it makes the full 8-tick cosmogenesis cost and conservation statements kernel-checkable over $\mathbb{Q}$, with $\varphi$ emerging as the Fibonacci convergent sequence of the self-similar recurrence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.