PauliError
plain-language theorem explainer
PauliError enumerates the four standard Pauli operators as the basis for modeling quantum errors in the Recognition Science 8-tick framework. Researchers deriving fault-tolerant codes from phase redundancy would cite this when expanding arbitrary errors E = αI + βX + γY + δZ. The declaration is a direct inductive definition with no additional axioms or computation.
Claim. The Pauli error basis consists of the four operators $I$ (identity, no error), $X$ (bit flip), $Y$ (combined bit and phase flip), and $Z$ (phase flip), forming the discrete error set used to expand any quantum channel error in the 8-tick phase model.
background
The module INFO-007 derives quantum error correction from 8-tick redundancy, where the eight phases supply natural redundancy and errors arise as phase shifts that correction must realign. The upstream phase definition supplies the concrete angles: phase (k : Fin 8) := (k : ℝ) * π / 4, periodic with period 2π. This inductive type supplies the discrete labels that map those phase deviations onto the standard Pauli expansion of an error operator.
proof idea
Direct inductive definition enumerating the four constructors I, X, Y, Z and deriving Repr together with DecidableEq; no lemmas or tactics are applied.
why it matters
This supplies the error alphabet required to construct the 8-tick logical codes and CSS/Steane variants listed as siblings in the same module. It directly implements the module's core claim that errors correspond to phase shifts within the eight-tick cycle, feeding the redundancy arguments that link to the EightTick.phase and ChurchTuringPhysicsStructure.Phase definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.