QECCodeFamily
QECCodeFamily enumerates the five canonical quantum error correction code families in the Recognition Science phi-ladder model. Researchers deriving threshold ratios or certifying error protection bounds cite this enumeration when establishing the family count equals five. The definition proceeds by direct inductive listing of the five constructors with automatic derivation of decidability and finiteness instances.
claimThe set of quantum error correction code families is the inductive type whose constructors are the repetition code, surface code, colour code, topological code, and concatenated code.
background
The module develops quantum error correction thresholds from the phi-ladder. It lists five families with characteristic thresholds: repetition near 50 percent, surface near 1 percent, colour near 0.5 percent, topological codes exhibiting phi to the minus k decay, and concatenated codes. Recognition Science predicts adjacent family thresholds stand in the ratio one over phi, with the surface threshold approximating phi to the minus nine, or roughly 1.3 percent. The setup identifies the five families with configuration dimension D equal to five.
proof idea
The declaration is a direct inductive definition that lists the five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances automatically with no additional lemmas or tactics required.
why it matters in Recognition Science
This enumeration supplies the base type for the downstream theorem establishing cardinality five and for the structure QECThresholdCert that encodes positivity and phi-inverse decay of thresholds. It realizes the B16 claim that five families correspond to configuration dimension D equals five, anchoring the phi-ladder predictions for error thresholds within the Recognition Science information domain.
scope and limits
- Does not assign explicit numerical threshold values to individual families.
- Does not prove the phi-decay relation between successive thresholds.
- Does not incorporate code families beyond the five enumerated constructors.
- Does not link families to concrete physical qubit layouts or hardware constraints.
formal statement (Lean)
25inductive QECCodeFamily where
26 | repetition | surface | colour | topological | concatenated
27 deriving DecidableEq, Repr, BEq, Fintype
28