cosmogenesis_tick_count
plain-language theorem explainer
Exactly eight discrete ticks appear in the rational cosmogenesis ledger, independent of the positive seed. Cosmology and ledger auditors cite it to pin the eight-tick cadence in kernel-checked trace certificates. The proof is pure reflexivity: the length of the range list 0..7 is definitionally eight.
Claim. For every rational seed, the length of the eight-tick index list equals $8$: $\lvert\{0,1,\ldots,7\}\rvert = 8$.
background
The module supplies a computable mirror of cosmogenesis over $\mathbb{Q}$, dual to the real-valued dynamics in PreBigBang and FirstTick. Events are posted by double-entry (addEvent with reciprocal), and total cost is summed $J$-cost with $J(x)=(x+x^{-1})/2-1$ (here qJ). The conserved multiplicative flow product stays identically $1$ after a full run.
Recognition Science forces an eight-tick octave (forcing chain T7, period $2^3$). The simulation therefore indexes ticks by List.range 8. Upstream cost and length notions (ledger cost, trace length) supply the surrounding vocabulary; this declaration only records the fixed cadence count itself.
proof idea
One-line term proof by rfl. Lean reduces (List.range 8).length definitionally to 8, so equality holds by reflexivity. The unused seed parameter is present only so the statement matches the seed-indexed certificate interface.
why it matters
Feeds the cadence_eight_ticks field of trace_certificates_seed2, the kernel-checked certificate bundle for the canonical seed-2 run (event count, $\sigma$-conservation, eight-tick cadence, closed nine-vertex cycle, positive first-tick cost). That bundle is the computable witness that the rational cosmogenesis ledger really runs an eight-tick octave.
In the broader framework this is the discrete T7 landmark inside the simulation layer: period $2^3$ is not an input parameter but the fixed length of the posted tick list. Together with flow-product conservation and positive first-tick $J$-cost, it closes the certificate that the $\phi$-convergent recurrence and double-entry ledger are running on the forced octave, not an ad-hoc horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.