grayCodeCycleLength
plain-language theorem explainer
grayCodeCycleLength assigns the length of a Gray code cycle on D dimensions to exactly 2^D. Ledger uniqueness arguments in Recognition Science cite it to fix the cycle length when proving that only an 8-tick period satisfies 3D cube traversal. The definition is a direct power assignment with no auxiliary computation or constraints.
Claim. The length of a Gray code cycle on $D$ dimensions is $2^D$.
background
The LedgerUniqueness module resolves the objection that other discrete ledgers could exist by proving uniqueness of phi, the 3D cube, and the 8-tick cycle. A Gray code cycle of length T on D dimensions supplies the combinatorial traversal structure required for ledger compatibility with the cube. The module documentation states that cycles of length less than 8 cannot close the cube traversal. This definition supplies the explicit length formula used downstream. Upstream results supply completeness predicates and structure definitions from SAT backpropagation and simplicial ledgers, but the Gray code component is imported from Patterns.GrayCode.
proof idea
The definition is a direct assignment of the cycle length to 2^D.
why it matters
This definition is invoked by eight_tick_minimal, complete_ledger_uniqueness, and rs_ledger_is_unique. Those theorems close Gap 9 by showing that phi, Q3, and the 8-tick cycle are the only solutions satisfying their respective constraints. It supplies the 8-tick component referenced in the module documentation and aligns with the eight-tick octave (period 2^3) from the forcing chain T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.