cycleOpCert
plain-language theorem explainer
A verified certificate that the Gray-code cycle permutation on the eight vertices of the 3-cube has exact period 8, is injective, advances by single bit flips, and has chiral flip asymmetry. Anyone treating the cycle operator as the algebraic source of generation structure and mixing would cite it. The value is a structure instance filled by four proved lemmas plus one native decision for asymmetry.
Claim. There is a verified certificate for the cycle permutation $\sigma$ on $\mathrm{Fin}\,8$ asserting: $\sigma^{8}=\mathrm{id}$; for every $0<k<8$ one has $\sigma^{k}\neq\mathrm{id}$; $\sigma$ is injective; each step along the Gray order equals a single bit flip at the prescribed bit; and the two chiral bit-flip counts are unequal.
background
The module builds the cycle operator on $\mathbb{C}^{8}$ induced by the 8-tick Gray-code walk on the cube $Q_{3}$. The eight vertices form the standard basis; one tick advances along the Gray path by flipping exactly one coordinate. The associated permutation of $\mathrm{Fin},8$ is the combinatorial skeleton of the unitary $U_{\mathrm{cycle}}$, whose eigenvalues are the eighth roots of unity and whose eigenmodes feed Born-rule and mixing constructions.
CycleOperatorCert packages the structural facts needed before one promotes the permutation to a matrix or spectral object: exact period 8, minimality of that period, injectivity (hence bijectivity on a finite set), the step-as-bit-flip identity, and a chirality asymmetry on bit-flip counts. Upstream lemmas already prove period, non-identity before period 8, injectivity, and the bit-flip step identity by finite case analysis and native decision.
proof idea
Definitional structure instance, not a tactic proof. The four main fields are filled by direct application of the upstream theorems cyclePerm_period, cyclePerm_not_identity_before_8, cyclePerm_injective, and cycle_step_is_bitflip. The remaining field flip_asymmetry is discharged by native_decide on the inequality of the two Gray-code chirality bit-flip counts. No further rewriting is required.
why it matters
This certificate is the bookkeeping hinge between the combinatorial Gray cycle and the unitary cycle operator whose period-8 spectrum the module advertises as the source of generation structure and CKM-type mixing angles. It locks in the eight-tick octave (framework landmark T7): the walk is a genuine order-8 cycle of single bit flips, not a shorter loop or a multi-bit jump. With used_by currently empty, the object stands ready for downstream matrix, eigenvalue, and mixing developments named in the module doc (cyclePermMatrix, period-eight unitary identity, DFT-8 eigenmodes). It does not itself construct the CKM matrix; it certifies the discrete dynamics those constructions must rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.