grayOrderInv
plain-language theorem explainer
Inverse Gray-code map from the eight vertices of the 3-cube to visit times on the closed 8-tick path. Anyone constructing the cycle permutation, its injectivity, or the unitary cycle operator on ℂ⁸ cites it. The body is an exhaustive case table on Fin 8, dual to the forward Gray order.
Claim. Define $g^{-1}:\{0,\ldots,7\}\to\{0,\ldots,7\}$ by sending each vertex index of $Q_3$ to the tick at which the Gray-code Hamiltonian cycle visits that vertex: $0\mapsto 0$, $1\mapsto 1$, $2\mapsto 3$, $3\mapsto 2$, $4\mapsto 7$, $5\mapsto 6$, $6\mapsto 4$, $7\mapsto 5$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary induced by the directed 8-tick Gray-code cycle on the 3-cube $Q_3$. The eight vertices form the standard basis; one full period of the Gray path yields a permutation matrix whose eigenvalues are the 8th roots of unity and whose eigenmodes are the DFT-8 modes used later for Born-rule forcing and CKM phases.
The forward Gray order maps tick index to vertex. This definition is the inverse map: vertex index to tick index. Together they identify the Gray Hamiltonian cycle with a pure cyclic shift on visit times. The ambient time quantum is the RS tick $\tau_0=1$, and one octave is eight ticks (the T7 period $2^3$).
proof idea
Pure definition by pattern match on Fin 8. Each constructor is assigned the unique tick at which that vertex appears in the Gray cycle; no lemmas are invoked. Downstream left- and right-inverse theorems discharge the bijection claim by fin_cases plus native_decide against this table and the forward order.
why it matters
This table is the coordinate change that turns the geometric Gray path into an algebraic cyclic shift. It is composed directly into the cycle permutation (next vertex = forward order of (inverse order of $v$ plus one)), and is the data used by the left- and right-inverse lemmas and by injectivity of the cycle permutation. Those facts underwrite the period-8 unitary $U_{\mathrm{cycle}}$, its 8th-root spectrum, and the generation/mixing phases that the module advertises as the source of the CKM matrix. Framework landmark: T7 eight-tick octave on $Q_3$ ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.