PauliError
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign probabilities or rates to the four error types.
- Does not define continuous or non-Pauli error channels.
- Does not include correction operators or decoding maps.
- Does not specify how these errors embed into a concrete qubit Hilbert space.
formal statement (Lean)
44inductive PauliError
45| I -- Identity (no error)
46| X -- Bit flip
47| Y -- Bit and phase flip
48| Z -- Phase flip
49deriving Repr, DecidableEq
50
51/-- Probability distribution over Pauli errors. -/