pattern3
plain-language theorem explainer
pattern3 supplies the explicit assignment of each element of Fin 8 to a 3-bit pattern (Fin 3 to Bool) realizing the binary-reflected Gray code order. Workers formalizing Hamiltonian cycles on the 3-cube for ledger adjacency cite it to obtain the concrete state-to-pattern map. The definition is supplied by direct case analysis on the eight inputs.
Claim. Let $P_3$ denote the set of functions from Fin 3 to Bool. The map $p: $ Fin 8 $→ P_3$ is given by the eight cases: $p(0)$ constantly false; $p(1)$ true only at position 0; $p(2)$ true only at 1; $p(3)$ true at 0 or 1; $p(4)$ true only at 2; $p(5)$ true at 0 or 2; $p(6)$ true at 1 or 2; $p(7)$ constantly true.
background
The GrayCycle module upgrades the cardinality facts of Patterns to an explicit adjacent cycle on the hypercube. The state space is Pattern d := Fin d → Bool, with adjacency when two patterns differ in exactly one coordinate and a cycle a closed walk of length 2^d visiting each pattern once. The module is self-contained and uses the standard recursive BRGC construction rather than external Gray-code axioms.
proof idea
The definition is supplied directly by exhaustive pattern matching on the eight elements of Fin 8. Each case assigns the corresponding bit vector by deciding membership of the coordinate values 0, 1, 2.
why it matters
pattern3 supplies the concrete patterns consumed by grayCycle3Path and grayCycle3_oneBit_step. It therefore realizes the explicit 8-state cycle required for ledger-compatible adjacency in dimension 3, aligning with the eight-tick octave (T7) of the forcing chain. The module documentation states that the counting bound alone is insufficient and that the adjacent cycle object is the stronger structure needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.