grayCodeCycleLength
plain-language theorem explainer
The Gray code cycle length on D dimensions equals 2 to the power D. Uniqueness arguments for the RS ledger cite this assignment to fix the cycle for the three-dimensional cube. The declaration is introduced by direct equating to the power-of-two expression.
Claim. The cycle length $T$ of a Gray code traversal on $D$ dimensions satisfies $T = 2^D$.
background
Module Meta.LedgerUniqueness addresses Gap 9: why the RS ledger must use phi, the three-dimensional cube, and an eight-tick cycle rather than other discrete structures. The Gray code cycle length supplies the combinatorial object needed to enforce the eight-tick constraint via compatibility with cube traversal. Upstream results include the completeness predicate on backpropagation states and the collision-free predicate on empirical programs; the module setting requires any discrete conservative ledger to be isomorphic to the RS ledger.
proof idea
The declaration is a direct definition that equates the cycle length to the indicated power-of-two expression.
why it matters
The definition is invoked by eight_tick_minimal and rs_ledger_is_unique. The latter asserts that the RS ledger is the unique discrete conservative structure because phi is the sole cost fixed point, D=3 is the sole linking dimension, and eight is the sole complete cycle length; this closes Gap 9. The construction aligns with the eight-tick octave forced at T7 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.