ErrorModel
plain-language theorem explainer
ErrorModel defines a probability distribution over the four Pauli operators with non-negative components that sum to one. Researchers deriving quantum error correction codes from eight-tick phase redundancy would cite this structure when specifying noise models. The declaration is a direct structure definition that bundles the four probabilities with their non-negativity and normalization conditions.
Claim. An ErrorModel consists of four real numbers $p_I, p_X, p_Y, p_Z$ satisfying $p_I, p_X, p_Y, p_Z ≥ 0$ and $p_I + p_X + p_Y + p_Z = 1$, where the components are the probabilities of the identity, bit-flip, Y-error, and phase-flip channels.
background
The module derives quantum error correction from the eight-tick redundancy of Recognition Science, where the eight discrete phases $kπ/4$ supply natural repetition for error detection. Upstream, the phase definition in EightTick supplies the periodic angles, while the probability definition in QuantumLedger returns Born-rule values as squared norms of state amplitudes. The structure of LedgerFactorization and PhiForcingDerived supply the underlying J-cost and factorization conventions used to calibrate error probabilities.
proof idea
This declaration is a structure definition that directly introduces four real fields together with three field conditions. No lemmas or tactics are invoked; the fields encode the probability simplex over Pauli errors by construction.
why it matters
ErrorModel supplies the noise model consumed by the depolarizing definition in the same module. It fills the basic error-distribution slot in the derivation of codes such as repetitionCode3 and eightTickLogicalCode that exploit eight-tick phase redundancy (T7). The structure supports the broader claim that quantum error correction emerges from the eight-tick octave without additional gauge assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.