pauliGroupSize_2cubed
plain-language theorem explainer
The declaration confirms that the single-qubit Pauli group cardinality equals eight, matching two to the power of the spatial dimension. Quantum information researchers applying Recognition Science to gate sets would cite this equality when assembling depth certificates. The proof is a direct decision procedure that evaluates the numerical identity between the constant definition and the exponential expression.
Claim. The cardinality of the single-qubit Pauli group equals $2^3$.
background
Recognition Science treats quantum computation as sequences of J-cost-minimizing recognition operations. The single-qubit Pauli group comprises the eight elements ±I, ±X, ±Y, ±Z, and the module defines its size as the constant eight. This aligns with the assignment of three spatial dimensions D, yielding 2^D equals eight. The upstream pauliGroupSize definition fixes the value at eight. The local module setting equates five canonical gate types to configDim D equals five and notes that universal sets of three gates equal D generate all unitaries.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the equality between the constant definition and the power expression.
why it matters
This result supplies the pauli_8 field inside the QuantumComputingDepthCert definition, which certifies the quantum computing depth parameters under RS_PAT_043. It links the Pauli group size directly to the spatial dimension D equals three from the forcing chain. The module connects the equality to the observation that universal gate sets of three elements equal D generate all unitaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.