CycleOperatorCert
plain-language theorem explainer
Certificate record that packages five structural facts about the Gray-code cycle permutation on the eight cube vertices: exact period 8, no smaller global period, injectivity, each step is a single prescribed bit flip, and asymmetric flip counts across bits. Cited by anyone assembling the eight-tick recognition operator or the unitary U_cycle on C^8. Pure interface definition; the proofs sit in the witness that fills the fields.
Claim. A cycle-operator certificate is a record asserting five facts about the Gray-code cycle permutation $P$ on $\mathrm{Fin}\,8$: (i) $P^8 = \mathrm{id}$; (ii) for every $0 < k < 8$ there is a vertex moved by $P^k$; (iii) $P$ is injective; (iv) at each tick $t$, $P$ sends the Gray-ordered vertex to the single-bit flip of the bit prescribed by the face-winding schedule; (v) over one full cycle, bit 0 and bit 1 are flipped a different number of times.
background
The module builds the cycle operator on $\mathbb{C}^8$ induced by the 8-tick Gray-code Hamiltonian path on the cube $Q_3$. The eight vertices form the computational basis; the Gray order maps tick index to vertex index, and its inverse recovers the visit time. The cycle permutation $P$ advances one step along that path: if $v$ is visited at tick $t$, then $P(v)$ is the vertex at tick $t+1$.
Each step flips exactly one coordinate of the three-bit label. The face-winding schedule names which bit flips at tick $t$, and the bit-flip operator realizes that coordinate change on $\mathrm{Fin},8$. Flip counts tally how often each of the three bits is toggled over the full period-8 loop; those counts are unequal, which is the chirality seed used downstream.
This sits inside the Recognition foundation that forces the eight-tick octave (T7): the directed cycle is the algebraic carrier of recognition dynamics, and its unitary lift has eigenvalues the 8th roots of unity (DFT-8 modes).
proof idea
No proof body: this is a structure (interface) definition. Its five fields are pure propositions about the already-defined cycle permutation, Gray order, bit-flip operator, flipped-bit schedule, and bit-flip counts. Instantiation is deferred to the witness that assigns each field to a proved lemma (period, minimality, injectivity, step-is-bitflip, and a native decision of flip asymmetry).
why it matters
Gives a single named bundle for the structural hypotheses that the cycle operator must satisfy before one promotes the permutation to a unitary on $\mathbb{C}^8$ and reads off eigenvalues, generation phases, and mixing. The sole direct consumer is the verified witness in the same module, which fills every field from the sibling lemmas on period, non-identity before 8, injectivity, and the step-is-bitflip identity.
In the broader framework this is the algebraic skeleton of the eight-tick octave (T7): period exactly 8, single-bit Gray steps, and flip asymmetry (chirality). Module documentation ties the same operator to DFT-8 eigenmodes used in Born-rule forcing and to the phase accumulation that feeds generation structure and CKM-type mixing. Without this certificate, downstream claims that $U_{\mathrm{cycle}}^8 = I$ with minimal period 8 would restate the same five facts ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.