toNat3_pattern3
plain-language theorem explainer
The lemma shows that converting a Fin 8 index to a 3-bit pattern via pattern3 and back via toNat3 recovers the original index value exactly. Researchers formalizing hypercube cycles or the eight-tick structure in Recognition Science cite it when proving bijectivity of the pattern mapping. The proof is an exhaustive case split over the eight elements of Fin 8 followed by direct decidable computation.
Claim. For any $w$ in Fin 8, if $p$ is the 3-bit pattern whose $j$-th coordinate is true precisely when the $j$-th bit of $w$ is set, then the integer value of $p$ obtained by summing $p_0 + 2p_1 + 4p_2$ equals the natural-number value of $w$.
background
The GrayCycle module defines Pattern d as the type Fin d → Bool and equips it with one-bit adjacency to obtain an explicit Hamiltonian cycle on the 3-cube. The definition pattern3 sends each element of Fin 8 to a concrete 3-bit pattern by testing individual bits (all-false for 0, bit 0 for 1, bit 1 for 2, etc.). The definition toNat3 recovers a natural number from any such pattern by the standard binary weighting 1 + 2 + 4. The present lemma records that these two maps are inverses on the domain Fin 8, supplying the missing direction needed for injectivity arguments.
proof idea
The term proof invokes fin_cases on the hypothesis w : Fin 8, producing eight subgoals. Each subgoal is discharged by the decide tactic, which evaluates the concrete expressions toNat3 (pattern3 w) and w.val and confirms they are equal.
why it matters
The lemma is invoked inside pattern3_injective to convert equality of patterns into equality of their integer indices, thereby establishing that pattern3 is injective. In the Recognition Science setting this supplies the bijective correspondence between Fin 8 and the 3-bit patterns required by the eight-tick octave (T7) and the derivation of D = 3. It completes a small but necessary step in the ledger-compatible adjacency construction without invoking external Gray-code axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.