pauli_has_2cube
plain-language theorem explainer
The Pauli elements realize the 2³ count with exactly eight members. Cross-domain universality arguments cite this to place the single-qubit Pauli group inside the D = 3 cube structure. The proof is a one-line wrapper that unfolds the cardinality predicate and lets decide confirm the equality.
Claim. Let $P$ be the set of Pauli elements with members $I, -I, X, -X, Y, -Y, Z, -Z$. Then $|P| = 2^3$.
background
The module collects instances of the count 8 = 2³ across Recognition Science domains as the maximal periodic structure for spatial dimension D = 3. HasTwoCubeCount is the predicate asserting that a finite type T satisfies Fintype.card T = 2^3. PauliElement is the inductive type whose eight constructors are the signed Pauli matrices, equipped with a derived Fintype instance.
proof idea
The proof is a one-line wrapper. It unfolds HasTwoCubeCount to the statement Fintype.card PauliElement = 8 and applies the decide tactic, which succeeds because the Fintype instance is derived and the cardinality is manifest.
why it matters
This supplies the Pauli instance inside twoCubeUniversalityCert, which aggregates all 2³ domains. It is invoked directly by pauli_tick_equicardinal to establish equicardinality with tick phases. The result fills the C14 claim that the D = 3 recognition cube has count 8, consistent with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.