grayOrderInv_left_inv
plain-language theorem explainer
The inverse Gray-code map is a left inverse of the forward Gray order on Fin 8: composing tick→vertex then vertex→tick recovers every tick index. Anyone building the cycle permutation or the unitary cycle operator on ℂ⁸ needs this bijection half. The proof is a one-line case split on Fin 8 discharged by native_decide.
Claim. For every tick index $i \in \{0,\ldots,7\}$, if $v$ is the vertex visited at tick $i$ under the Gray-code order on $Q_3$, then the inverse Gray map sends $v$ back to $i$. In symbols: $\mathrm{grayInv}(\mathrm{gray}(i)) = i$ for all $i$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary permutation matrix induced by the 8-tick Gray-code cycle on the cube $Q_3$. Vertices of $Q_3$ are the standard basis of $\mathbb{C}^8$; each tick flips exactly one bit, so the path is a Hamiltonian cycle of length 8 (the eight-tick octave of the forcing chain).
grayOrder is the forward map tick index $\mapsto$ vertex index (alias of gray8At). grayOrderInv is the explicit inverse table vertex index $\mapsto$ tick index: it records when each vertex is visited. Together they identify the cyclic shift that defines the cycle permutation and, later, $U_{\mathrm{cycle}} \in \mathrm{GL}(8,\mathbb{C})$.
Left-invertibility is the half of the bijection that says every tick is recovered after reading the vertex it lands on. The companion right-inverse statement closes the other direction.
proof idea
Wrapper proof: introduce the tick $i$, case-split on all eight values of Fin 8, and discharge each concrete equality by native_decide. No external lemmas beyond the definitions of grayOrder and grayOrderInv; the finite table is checked exhaustively.
why it matters
Without left-invertibility the Gray order would not be a bijection, so the induced map on vertices would not be a permutation of Fin 8 and the cycle operator would not be a well-defined element of $S_8$ (hence not a unitary permutation matrix of period 8). The module’s main objects—CyclePermutation, cyclePermMatrix, period-eight, and the 8th-root eigenvalues used for generation structure and CKM mixing—rest on this identification of ticks with vertices along the Gray path.
In the broader Recognition framework this sits under T7 (eight-tick octave, period $2^3$) and the cube-gauge story: the directed Gray dynamics on $Q_3$ is the algebraic seed from which the cycle operator and its DFT-8 eigenmodes are extracted. No downstream theorems are recorded as direct users yet; the immediate siblings are the right-inverse and the cycle-permutation lemmas that consume both inverses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.