cosmogenesis
plain-language theorem explainer
Eight ticks of the 3-cube cadence are posted, each with its reciprocal, onto the empty rational recognition ledger from a rational seed. Cosmologists and RS auditors cite this as the computable cosmogenesis run over ℚ. The object is built by folding double-entry posting over the eight cadence events from the self-similar recurrence.
Claim. Given a rational seed $s\in\mathbb{Q}$, the cosmogenesis ledger is the list of rational recognition events obtained by starting from the empty list and, for each tick $t=0,\ldots,7$, double-entry posting the cadence event whose endpoints are successive vertices of the 3-cube walk and whose ratio is the $t$-th term of the recurrence $r\mapsto 1+1/r$ seeded by $s$.
background
This module is a computable, kernel-checked mirror of cosmogenesis over $\mathbb{Q}$. The real-analytic dynamics live in PreBigBang and FirstTick; here every object is a Lean value one can #eval.
A recognition event over $\mathbb{Q}$ is a triple (source, target, ratio). Double-entry posting appends both an event and its reciprocal (endpoints swapped, ratio inverted), mirroring the real ledger law. The cadence walk on the 3-cube has nine vertices and eight edges; each tick posts one edge carrying the corresponding recurrence ratio. The map $r\mapsto 1+1/r$ yields the Fibonacci convergents $2, 3/2, 5/3, 8/5,\ldots$ approaching $\varphi$.
The conserved multiplicative quantity is the flow product at an agent: the product of ratios of all events touching that agent. Each paired posting multiplies by $r\cdot r^{-1}=1$, so the product is invariant.
proof idea
Pure definition, no proof obligations. Start from the empty list and fold over List.range 8: at tick $t$, double-entry-post the cadence event generated from the seed at that tick (endpoints from the 3-cube walk, ratio from the recurrence sequence). Each posting prepends the event and its reciprocal, so the result is a list of sixteen events (eight pairs).
why it matters
Central ledger object of the rational cosmogenesis simulation. Downstream, σ-conservation proves that after the full run the flow product equals $1$ at every agent for any positive seed, with no decide and no sorry. A companion length theorem records exactly sixteen events. Trace certificates and seed-2 evaluations hang off the same object; the fold-invariance lemma for the flow product is the engine behind conservation.
Framework-wise this realizes the T7 eight-tick octave on the $D=3$ cube: eight edges of the 3-cube cadence, each paired by double-entry. Recurrence ratios are the exact Fibonacci convergents to $\varphi$ (T6), so $\varphi$-emergence is visible as a rational sequence under evaluation. It mirrors the real FirstTick ledger while keeping conservation inside the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.