grayCycle3_period
plain-language theorem explainer
The period of the 3-bit Gray cycle on the hypercube equals eight. Pattern formalizers in Recognition Science cite this to fix the cardinality for three-dimensional coverings that respect one-bit adjacency. The proof reduces to a single decision procedure that evaluates the power equality directly.
Claim. The Gray cycle on the three-dimensional hypercube has period satisfying $2^3 = 8$.
background
The module defines Pattern d as the set of functions from Fin d to Bool. Adjacency holds when two patterns differ in exactly one coordinate. A cycle is a closed walk of length 2^d that visits every pattern once. This upgrades prior surjection facts to an explicit Hamiltonian cycle on the hypercube, aligning ledger-compatible adjacency with the counting bound. The setting is self-contained and avoids external Gray-code axioms by using the standard recursive construction.
proof idea
One-line wrapper that applies the decide tactic to evaluate the arithmetic equality 8 = 8.
why it matters
This declaration fixes the period for GrayCover in dimension three, anchoring the eight-tick octave required by the forcing chain for D = 3. It supplies the cardinality step that later lemmas in the module use to certify full coverage under one-bit flips. The result closes the gap between pure counting and adjacent cycle structure without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.