PauliElement
plain-language theorem explainer
The inductive type enumerates the eight single-qubit Pauli operators as plusI, minusI, plusX, minusX, plusY, minusY, plusZ, minusZ. Cross-domain Recognition Science researchers cite it to instantiate the shared 2^3 cardinality for D=3 structures. The declaration is a direct inductive definition that automatically derives DecidableEq, Repr, BEq and Fintype.
Claim. The type of single-qubit Pauli elements consists of the eight operators $I, -I, X, -X, Y, -Y, Z, -Z$, equipped with decidable equality, representation, Boolean equality and finite-type structure.
background
The CrossDomain.TwoCubeUniversality module assembles instances of the structural claim that 8 = 2^3 appears uniformly across RS domains as the maximal-periodic count for spatial dimension D=3. PauliElement supplies the single-qubit Pauli group instance alongside DFTMode, Q3Vertex and TickPhase. The module proves all listed instances satisfy HasTwoCubeCount, which asserts cardinality exactly 8. No upstream lemmas are required; the definition stands alone before the equicardinality theorems.
proof idea
The declaration is an inductive definition that introduces exactly eight constructors and derives the four type-class instances in one step. No tactics or lemmas are applied; the Lean kernel constructs the type and its decidability and finiteness properties directly from the constructor list.
why it matters
PauliElement supplies the pauli_is_2cube field inside the TwoCubeUniversalityCert structure and is used by pauli_has_2cube and pauli_tick_equicardinal. The latter shows Fintype.card PauliElement equals Fintype.card TickPhase via two_cube_equicardinal. In the framework it instantiates the T7 eight-tick octave and D=3 landmark, confirming that the Pauli group order matches the recognition-cube count |F_2^3|.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.