pauli_has_2cube
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish commutation relations or group structure on the elements.
- Does not extend the count to multi-qubit systems.
- Does not derive the cardinality from the Recognition Composition Law.
- Does not address physical interpretations such as spin or measurement.
Lean usage
two_cube_equicardinal pauli_has_2cube tick_has_2cubeformal statement (Lean)
52theorem pauli_has_2cube : HasTwoCubeCount PauliElement := by
proof body
One-line wrapper that applies unfold.
53 unfold HasTwoCubeCount; decide