pattern3
pattern3 supplies the explicit mapping from each element of Fin 8 to a unique 3-bit boolean vector by extracting its binary digits. Researchers formalizing hypercube Hamiltonian cycles or ledger adjacency in Recognition Science cite it to ground the 3-dimensional case. The definition is realized by exhaustive case analysis on the eight inputs with no auxiliary lemmas.
claimDefine $p_3 :$ Fin $8$ $→$ (Fin $3$ $→$ Bool) by cases: $p_3(0) = $ constant false, $p_3(1) =$ true only at coordinate 0, $p_3(2) =$ true only at coordinate 1, $p_3(3) =$ true at 0 or 1, $p_3(4) =$ true only at coordinate 2, $p_3(5) =$ true at 0 or 2, $p_3(6) =$ true at 1 or 2, $p_3(7) =$ constant true.
background
In the GrayCycle module the state space is Pattern $d :=$ Fin $d$ $→$ Bool, the vertices of the $d$-dimensional hypercube. Adjacency requires patterns to differ in exactly one coordinate, and a cycle is a closed walk of length $2^d$ visiting each vertex once. For $d=3$ this yields the eight-tick period required by the Recognition framework.
proof idea
Direct definition by cases on Fin 8. Each case assigns the boolean vector whose support matches the binary digits of the input index, with the least significant bit at coordinate 0. No lemmas are invoked.
why it matters in Recognition Science
pattern3 supplies the concrete patterns used by grayCycle3Path to build the reordered cycle and by grayCycle3_oneBit_step to verify one-bit flips. It bridges the surjection of Patterns.period_exactly_8 to an adjacent cycle, aligning with the eight-tick octave at D=3 without invoking external Gray-code axioms.
scope and limits
- Does not prove that consecutive images under the Gray permutation differ by one bit.
- Does not establish injectivity or surjectivity of the map.
- Does not encode the Gray permutation gray8At.
- Does not connect to mass formulas, constants, or the forcing chain T0-T8.
- Does not generalize to dimensions other than 3.
Lean usage
def grayCycle3Path (i : Fin 8) : Pattern 3 := pattern3 (gray8At i)formal statement (Lean)
82def pattern3 : Fin 8 → Pattern 3
83| ⟨0, _⟩ => fun _ => false
84| ⟨1, _⟩ => fun j => decide (j.val = 0)
85| ⟨2, _⟩ => fun j => decide (j.val = 1)
86| ⟨3, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 1)
87| ⟨4, _⟩ => fun j => decide (j.val = 2)
88| ⟨5, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 2)
89| ⟨6, _⟩ => fun j => decide (j.val = 1 ∨ j.val = 2)
90| ⟨7, _⟩ => fun _ => true
91
92/-- Canonical 3-bit Gray order as a function `Fin 8 → Fin 8`.
93
94Sequence: [0,1,3,2,6,7,5,4]. -/