depolarizing
plain-language theorem explainer
The depolarizing definition supplies the uniform Pauli noise model as an instance of the error model structure, with no-error probability 1 minus p and each of the three Pauli errors carrying probability p over 3, for p between 0 and 1. Quantum information theorists working within the Recognition Science framework would reference this when analyzing noise on phase-encoded qubits. The construction directly populates the four probabilities and invokes linarith plus ring to discharge the non-negativity and normalization obligations.
Claim. The depolarizing channel with error probability $p$ (where $0 ≤ p ≤ 1$) is the error model given by $p_I = 1-p$, $p_X = p/3$, $p_Y = p/3$, $p_Z = p/3$, with the required non-negativity and normalization conditions holding.
background
In the Information.QuantumErrorCorrection module the error model is a structure that assigns probabilities to the identity (no error) and the three Pauli operators X, Y, Z, subject to non-negativity and summing to one. This sits inside the broader Recognition Science treatment of quantum error correction, which derives correction principles from the eight-tick phase structure: the eight phases supply natural redundancy so that an error appears as a detectable phase shift. Upstream, the phase definition supplies the eight discrete phases kπ/4, while the tick definitions establish the discrete time quantum underlying the encoding. The Physical structure from DataCore supplies the minimal positivity assumptions on constants that anchor such models.
proof idea
The definition is a direct construction of the ErrorModel record. It assigns p_I := 1-p, p_X := p/3 and similarly for Y and Z. Non-negativity of p_I follows from linarith on the right half of hp, while the three Pauli probabilities use the left half; normalization is discharged by ring.
why it matters
This supplies the canonical depolarizing noise model for the eight-tick error correction principle outlined in the module. It feeds the ErrorModel structure used in subsequent definitions such as the eight-tick logical code. Within the framework it instantiates the T7 eight-tick octave for error modeling, providing a concrete noise channel that can be paired with the phase-based syndrome detection. No open question is directly closed here, but it prepares the ground for proving correction thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.