toNat3
plain-language theorem explainer
The definition toNat3 converts a 3-bit pattern, represented as a map from Fin 3 to Bool, into its integer value under standard binary weighting. Researchers constructing explicit Hamiltonian cycles on the 3-cube inside Recognition Science cite it to label vertices numerically before proving injectivity of the pattern3 map. It is realized by a direct three-term sum that tests each coordinate and scales the result by the corresponding power of two.
Claim. For a pattern $p :$ Fin $3$ $→$ Bool, define toNat3$(p) := (1$ if $p(0)$ else $0) + (2$ if $p(1)$ else $0) + (4$ if $p(2)$ else $0)$.
background
The GrayCycle module works with the state space Pattern 3 := Fin 3 → Bool, the vertices of the 3-dimensional hypercube whose edges connect patterns differing in exactly one coordinate. The module upgrades the earlier cardinality result that a surjection Fin 8 → Pattern 3 exists to an explicit adjacent cycle of length 8. Upstream, the Pattern abbreviation in Measurement and the definition in Patterns both identify a finite window of length d with a map Fin d → Bool; the Streams and Streams.Blocks variants add an integer functional Z counting the number of true entries.
proof idea
The definition is a direct term-mode expansion that adds the three bit contributions by testing the boolean value at each Fin index and weighting by 1, 2 and 4 respectively.
why it matters
toNat3 supplies the numerical coordinate used by the downstream lemmas pattern3_injective and toNat3_pattern3. Those lemmas certify that pattern3 : Fin 8 → Pattern 3 is bijective, realizing the eight-tick octave (T7) inside the GrayCycle construction and aligning the ledger-compatible adjacency story with the Recognition framework's 2^D counting bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.