cosmogenesis_length
plain-language theorem explainer
The cosmogenesis ledger always contains exactly sixteen recognition events, independent of the rational seed. Anyone citing the eight-tick double-entry simulation or the seed-2 trace certificates needs this count. The proof is a one-line application of the fold-length lemma for paired postings, followed by arithmetic.
Claim. For every rational seed $s$, the cosmogenesis ledger built from $s$ is a list of length $16$.
background
This module is the computable $\mathbb{Q}$-mirror of the real cosmogenesis dynamics in PreBigBang and FirstTick. Events are rational recognition edges (QEvent); addEvent posts each edge together with its reciprocal (double-entry), so every tick contributes two list entries.
cosmogenesis s folds eight ticks over the empty list: at tick $t$ it posts cosmoEvent s t, the edge of the 3-cube cadence carrying the $t$-th self-similar recurrence ratio from seed $s$. The fundamental period is the eight-tick octave ($\tau_0=1$ tick; one octave $=8$ ticks).
Upstream, foldl_addEvent_length states that $n$ paired postings from the empty ledger yield a list of length $2n$. That is the only nontrivial input to the length claim.
proof idea
Instantiate foldl_addEvent_length at $f=\mathrm{cosmoEvent},s$ and $n=8$. The fold that defines cosmogenesis s therefore has length $2\cdot 8$. Close with omega to rewrite $2\cdot 8$ as $16$. No induction or case analysis appears in this proof itself; the induction lives inside the fold-length lemma.
why it matters
Fixes the event cardinality of the kernel-checked cosmogenesis run: eight ticks, each double-entered, give sixteen posts. Downstream, trace_certificates_seed2 packages this as the event_count field of the seed-2 certificate bundle (alongside $\sigma$-conservation, cadence, cycle closure, and first-tick cost positivity).
In the Recognition framework this is the discrete footprint of the T7 eight-tick octave on the 3-cube cadence (T8 forces $D=3$). It is not a dynamical law; it is the bookkeeping identity that lets later certificates quote a concrete, seed-independent length without #eval or decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.