surfaceCodeThreshold
plain-language theorem explainer
The declaration assigns the constant 0.01 to the surface code threshold in RS-native units. Quantum information researchers estimating fault-tolerant computation under 8-tick phase redundancy would cite this value to bound physical error rates. The definition is a direct constant assignment with no reduction or lemma application.
Claim. The surface code threshold satisfies $p_ {threshold} = 0.01$.
background
The module derives quantum error correction from 8-tick redundancy, where the eight phases supply natural redundancy and errors appear as phase shifts restored by correction. The fundamental time quantum is the tick, defined as 1 in RS-native units, with phases given by $k π / 4$ for $k = 0,…,7$. This setting supplies the approximate threshold below which errors can be corrected indefinitely.
proof idea
The definition is a direct constant assignment of 0.01.
why it matters
The constant populates the ErrorCorrectionCert structure, which requires a positive threshold together with non-negative error-rate costs. It aligns with the eight-tick octave in the forcing chain and instantiates the module's RS prediction for surface codes derived from holographic boundary and phase-space redundancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.