Pith. sign in
module module high

IndisputableMonolith.Foundation.CycleOperator

show as:
view Lean formalization →

Defines the cycle operator of the canonical 3-bit Gray walk on Q₃: the order map from tick index to vertex, its inverse, the induced 8-cycle permutation, and the single-bit-flip step. Anyone deriving CKM geometry, CP phase, or mass/weak bases from the eight-tick clock cites this. Proofs are mostly explicit Fin-arithmetic and injectivity/period checks on the Gray schedule.

claimOn the 3-cube $Q_3$ with vertices identified with $\mathrm{Fin}\,8$, the Gray order is a bijection $\mathrm{grayOrder}:\mathrm{Fin}\,8\to\mathrm{Fin}\,8$ sending tick index to vertex index (with inverse $\mathrm{grayOrderInv}$). The cycle permutation $\sigma$ is the 8-cycle advancing one Gray step; it has exact period $8$ and is not the identity for any proper divisor. Each step equals a coordinate bit-flip operator $F_i$, an involution.

background

Recognition Science takes a discrete eight-tick clock as fundamental (period $2^3$), with phases at multiples of $\pi/4$. The state space is the 3-cube $Q_3$: binary patterns of length 3, adjacent when they differ in exactly one bit. Upstream GrayCycle packages a Hamiltonian cycle as a closed adjacent walk of length $2^d$ that visits every pattern once.

This module specializes that cycle to the canonical 3-bit Gray code and treats it as an operator on tick time. FaceWinding and GrayCodeChirality already use directed face traversals of the same walk as the geometric seed of CP violation; GaugeFromCube extracts $SU(3)\times SU(2)\times U(1)$ from $\mathrm{Aut}(Q_3)$. CycleOperator supplies the concrete permutation and bit-flip calculus those stories need.

Notation: tick indices live in $\mathrm{Fin},8$; vertices are the same type under Gray reordering. The step map is the generator of the cyclic action; bit-flip operators are the elementary cube edges.

proof idea

Definition-heavy module with short supporting lemmas. grayOrder and grayOrderInv are explicit tables (or closed forms) for the Gray schedule; left/right inverse lemmas discharge bijectivity by computation on Fin 8. cyclePerm is the conjugation of +1 by that order; cyclePerm_explicit unfolds it, injectivity and period-8 follow from the Gray Hamiltonian property and finite checking that $\sigma^k\neq\mathrm{id}$ for $0<k<8$. bitFlipOp is the coordinate flip; involution is immediate ($F_i^2=\mathrm{id}$). cycle_step_is_bitflip identifies each Gray edge with the unique flipped coordinate, tying the abstract cycle to cube adjacency.

why it matters in Recognition Science

Closes the operator interface between the eight-tick octave (forcing landmark T7) and the cube geometry used for flavor. Downstream MassWeakBases builds mass and weak eigenstate bases on generation space whose overlap is the CKM matrix; it needs the directed cycle to fix how generations couple along the walk. CKMFromCube assembles the mixing matrix from $Q_3$, generation torsion, and Gray chirality $[4,2,2]$, importing this permutation as the discrete transport. CPPhaseDerivation reads $\delta_{\mathrm{CKM}}$ as the Berry phase of generation eigenstates carried around the same directed 8-cycle. Without a proved period-8 bit-flip cycle, those derivations lack a rigid clock action.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (20)