gray8At_injective
The canonical 3-bit Gray code map from Fin 8 to Fin 8 is injective. Pattern enumeration work in Recognition Science cites it to guarantee distinct positions in the eight-tick cycle for D=3. The proof exhausts all input pairs with fin_cases on both arguments, then dispatches the equality hypothesis by cases and reflexivity.
claimThe function $g : {0,1,2,3,4,5,6,7} → {0,1,2,3,4,5,6,7}$ given by the sequence $[0,1,3,2,6,7,5,4]$ is injective.
background
The GrayCycle module works with the state space of all 3-bit patterns (functions Fin 3 → Bool). Two patterns are adjacent when they differ in exactly one coordinate. A Gray cycle is a closed walk of length 8 that visits every pattern once, supplying the explicit adjacency structure missing from the earlier cardinality result Patterns.period_exactly_8. The function gray8At encodes the standard binary-reflected Gray code order on these eight states.
proof idea
One-line wrapper that applies fin_cases to both indices, cases on the equality hypothesis, and closes each branch by rfl.
why it matters in Recognition Science
The result is invoked directly by grayCycle3_injective to obtain injectivity of the full cycle path grayCycle3Path. It supplies the uniqueness step required to align the eight-tick octave (T7) with ledger-compatible adjacency for D=3. The module note states that this stronger object is needed once cardinality facts are upgraded to Hamiltonian-cycle properties.
scope and limits
- Does not prove surjectivity of gray8At.
- Does not generalize injectivity to Gray codes on Fin (2^d) for d > 3.
- Does not establish the one-bit adjacency property of the cycle.
- Does not relate the ordering to J-cost or defectDist.
Lean usage
have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij); exact gray8At_injective h0formal statement (Lean)
109theorem gray8At_injective : Function.Injective gray8At := by
proof body
Term-mode proof.
110 intro i j h
111 -- brute-force on the 8 cases
112 fin_cases i <;> fin_cases j <;> cases h <;> rfl
113
114/-! ## A small helper: 3-bit patterns can be re-encoded as a Nat in [0,8) -/
115
116/-- Convert a 3-bit pattern to a Nat by the usual binary expansion. -/