pauliGroupSize
plain-language theorem explainer
The single-qubit Pauli group is assigned cardinality 8. Researchers modeling quantum computation as J-cost-minimizing recognition sequences cite this constant to equate the Pauli set with 2^D. The declaration is a direct constant assignment requiring no lemmas or computation.
Claim. The single-qubit Pauli group has cardinality $8$.
background
The module treats quantum computation as sequences of J-cost-minimizing recognition operations under the Recognition Science framework. Five canonical gate types (Pauli, Clifford, T-gate, CNOT, Toffoli) are set equal to configDim D = 5, while the eight single-qubit Pauli elements (±I, ±X, ±Y, ±Z) are identified with 2^D. This definition supplies the constant 8 to support later equalities with the eight-tick octave.
proof idea
The declaration is a direct constant definition that assigns the natural number 8. No lemmas are invoked and no tactics are executed; the body is simply the literal value.
why it matters
The definition is referenced by pauliGroupSize_2cubed, which proves equality to 2^3, and by the structure QuantumComputingDepthCert that records five gates, Pauli size 8, and three universal gates. It implements the RS_PAT_043 / B15 claim that eight Pauli elements equal 2^D and that a three-element universal set generates all unitaries. The assignment ties directly to the eight-tick octave (T7) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.