cyc
plain-language theorem explainer
Gray-code Hamiltonian cycle on the 3-cube: the nine-entry list that visits every vertex once and returns to the start. Cosmogenesis simulation uses it as the eight-tick cadence walk along which recognition events are posted. The declaration is a literal constant list; length nine and closed-loop use are checked downstream.
Claim. The constant sequence $(0,1,3,2,6,7,5,4,0)$ is a closed Gray-code Hamiltonian walk on the vertices of the $3$-cube: consecutive labels differ by one bit, every vertex in $\{0,\ldots,7\}$ appears exactly once before the final return to $0$, yielding eight edges.
background
The module supplies a computable rational mirror of the real-valued PreBigBang and FirstTick dynamics. Recognition events are posted along a fixed eight-tick cadence on the 3-cube, matching the eight-tick octave (T7) and $D=3$ spatial dimensions (T8).
Vertices of the 3-cube are labeled $0..7$ by bitstrings. A Gray-code cycle flips one bit per step, so each consecutive pair is a geometric edge. Upstream holography defines ledger closure on plaquettes and glued dominoes as even-parity bit loops; interface edge lists enumerate adjacent ordered pairs. The circle-winding chain records that closed loops carry integer winding.
This list is the concrete walk the simulation posts against: eight edges, nine vertex entries including the closing return.
proof idea
Literal definition only: the list is written out by hand as $[0,1,3,2,6,7,5,4,0]$. No lemmas are applied and no proof obligations attach to the def. Downstream, length equality is discharged by native_decide on the concrete list.
why it matters
Feeds the cosmogenesis event constructor, which posts the $t$-th recognition event on the edge from the $t$-th to the $(t+1)$-st entry, carrying the $t$-th recurrence ratio. Also feeds the length theorem (nine vertices, eight edges) and the trace-certificate field that records the closed nine-vertex cadence.
Together these pin the eight-tick cosmogenesis walk on the 3-cube so the conservation theorem can prove the flow product is identically $1$ at every agent after the full double-entry ledger, for any positive rational seed. The walk is the discrete skeleton of the T7 octave inside $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.