pauliGroupSize_2cubed
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the Pauli group size from the J-cost function.
- Does not treat multi-qubit Pauli groups.
- Does not prove gate-set universality.
- Does not reference phi-ladder or alpha-band constants.
Lean usage
quantumComputingDepthCert where five_gates := quantumGateTypeCount, pauli_8 := pauliGroupSize_2cubed, universal_D := universalGates_eq_Dformal statement (Lean)
29theorem pauliGroupSize_2cubed : pauliGroupSize = 2 ^ 3 := by decide
proof body
Term-mode proof.
30
31/-- Universal gate set has 3 gates = D. -/