cyc_length
plain-language theorem explainer
The Gray-code cadence walk on the 3-cube is a closed loop with nine vertices (eight edges). Cosmology and ledger-forcing arguments cite it to lock the eight-tick posting schedule to a concrete cycle. The proof is a one-line native decision on the explicit vertex list.
Claim. The Gray-code Hamiltonian cycle on the 3-cube, written as the vertex list $[0,1,3,2,6,7,5,4,0]$, has length $9$ (eight edges, returning to the start).
background
This module mirrors cosmogenesis over $\mathbb{Q}$ so the ledger is a Lean object one can evaluate, with conservation proved in the kernel. Events are posted by double-entry; the flow product (multiplicative $\sigma$) stays $1$ after the full run.
The cadence is the Gray-code Hamiltonian cycle on the 3-cube. The list cyc is exactly $[0,1,3,2,6,7,5,4,0]$: eight steps that visit every vertex and close. Cosmogenesis folds eight ticks, one per edge of that walk, onto the empty ledger.
Upstream, cosmogenesis builds that eight-tick ledger from a positive rational seed; the length fact here only concerns the cycle list itself, not the ledger contents.
proof idea
Term-mode proof by native_decide on the concrete finite list. No lemmas are invoked: Lean evaluates List.length of $[0,1,3,2,6,7,5,4,0]$ and checks equality with $9$.
why it matters
Pins the closed eight-edge cadence that drives the computable cosmogenesis run. Downstream, trace_certificates_seed2 packages kernel-checked certificates for the canonical seed-2 simulation and sets cyc_closed_nine_vertices to this theorem, alongside event count, $\sigma$ conservation, and first-tick cost positivity.
In the Recognition forcing chain this is the concrete witness for the eight-tick octave (T7) on the 3-cube that forces $D=3$ (T8): nine vertices mean eight edges and a return to the origin. Without the closed length, the certificate bundle cannot assert that the walk is a genuine closed cadence rather than an open path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.