grayOrderInv_right_inv
plain-language theorem explainer
Composing the Gray-code tick-to-vertex map after the vertex-to-tick map recovers every vertex index on Fin 8. Anyone assembling the 8-tick cycle permutation (and thus the cycle operator on ℂ⁸) cites this right-inverse fact. The proof is exhaustive case split on Fin 8 discharged by native_decide.
Claim. For every vertex index $j \in \{0,\ldots,7\}$, if $t$ is the tick at which $j$ is visited along the Gray-code cycle on $Q_3$, then the vertex visited at tick $t$ is again $j$. Equivalently, the tick-to-vertex Gray order is a right inverse of the vertex-to-tick map.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary permutation matrix induced by the directed 8-tick Gray-code Hamiltonian cycle on the cube $Q_3$. The eight vertices form the standard basis; one full period is the Recognition Science eight-tick octave.
Two maps organize the path. The Gray order (alias of gray8At) sends tick index to the vertex visited at that tick. Its putative inverse sends each vertex to the unique tick when it is visited; the definition is the explicit table (vertex 0 at tick 0, 1 at 1, 2 at 3, 3 at 2, 4 at 7, and so on). The fundamental time quantum is one tick ($\tau_0 = 1$).
For the cycle to be a genuine permutation of all eight vertices, these two maps must be mutual inverses. The present statement is the right-inverse half of that bijection.
proof idea
Term/tactic hybrid on a finite type: introduce the vertex $j$, then fin_cases j splits into the eight concrete values of Fin 8. Each residual goal is a ground equality between concrete Fin 8 terms, closed by native_decide. No algebraic lemma is invoked; the proof is pure exhaustive evaluation of the two lookup tables.
why it matters
Without both inverse laws, the Gray path would not be certified as a permutation of every vertex, and the cycle operator $U_{\mathrm{cycle}}\in\mathrm{GL}(8,\mathbb{C})$ would not be well-defined as a period-8 unitary. The module's main results (cycle permutation, permutation matrix, $U^8=I$, eigenvalues the 8th roots of unity, DFT-8 eigenmodes feeding Born-rule and CKM structure) all rest on that permutation.
In the forcing chain this sits under T7 (eight-tick octave, period $2^3$). The sibling left-inverse closes the bijection; nearby siblings (cyclePerm, injectivity, exact period 8, bit-flip step) consume the same Gray tables. No downstream edges are recorded yet for this lemma alone, but it is load-bearing scaffolding for the cycle-operator stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.