cosmoEvent
plain-language theorem explainer
Packages one discrete recognition event at tick t: the oriented edge of the 3-cube Gray-code cycle from vertex v_t to v_{t+1}, labeled by the t-th rational iterate of r ↦ 1 + 1/r from a seed. Cosmogenesis folds eight of these (with double-entry) into the ledger. Pure structure constructor; no proof content.
Claim. Given a rational seed $s$ and tick $t\in\mathbb{N}$, the cosmogenesis event is the recognition triple $(v_t,\,v_{t+1},\,r_t)$, where $v$ is the Gray-code Hamiltonian cycle on the 3-cube (closed loop of length 8) and $r_t$ is the $t$-th iterate of the map $r\mapsto 1+1/r$ starting at $s$.
background
This module supplies a computable, kernel-checked mirror of cosmogenesis over $\mathbb{Q}$. The real-analytic dynamics live in PreBigBang and FirstTick; here every object is rational so the run is #eval-able and conservation is a proved equality, not a runtime check.
A recognition event over $\mathbb{Q}$ is a triple (source, target, ratio). The Gray-code cycle $v = [0,1,3,2,6,7,5,4,0]$ is the Hamiltonian walk on the 3-cube that closes after eight edges. The self-similar recurrence $r\mapsto 1+1/r$ produces the exact Fibonacci convergents $2,,3/2,,5/3,,8/5,\ldots$ to $\varphi$.
Double-entry posting pairs each event with its reciprocal (swap endpoints, invert ratio), so the multiplicative flow product at every agent is invariant under a full tick.
proof idea
Definition only: construct the QEvent structure with source $v_t$, target $v_{t+1}$ (defaulting missing indices to 0 via list lookup), and ratio equal to the $t$-th recurrence value from the seed. No tactics, no lemmas applied.
why it matters
Atomic building block of the eight-tick cosmogenesis ledger. The parent definition folds cosmoEvent seed t over $t=0..7$ with double-entry posting; the conservation theorem then shows the flow product equals 1 at every agent for any positive seed, and the length theorem records sixteen posted events (eight pairs).
Framework landmarks: the eight-tick octave (T7) and $D=3$ spatial dimensions (T8) appear concretely as the 3-cube Gray-code cadence. The recurrence sequence makes $\varphi$ emerge as exact rational convergents rather than an analytic fixed-point argument. Closes the computable side of the ledger story that the real modules only sketch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.