qecCodeFamilyCount
plain-language theorem explainer
The inductive type enumerating canonical quantum error correction code families contains exactly five elements. Workers assembling threshold certificates in the Recognition Science information module cite this cardinality when populating the five_families field. The proof is a one-line decision procedure that invokes the derived Fintype instance on the five-constructor inductive definition.
Claim. Let $QECCodeFamily$ be the finite type whose elements are the five families repetition, surface, colour, topological and concatenated. Then $|QECCodeFamily| = 5$.
background
The module treats quantum error correction thresholds as arising from the phi-ladder. It lists five canonical families (repetition, surface, colour, topological, concatenated) whose thresholds are predicted to stand in ratios governed by powers of phi, with the surface-code threshold near phi^(-9). The local claim is that these five families exhaust the configuration dimension D = 5 in the Recognition Science setting. The upstream inductive definition supplies the Fintype instance used by the cardinality statement.
proof idea
One-line wrapper that applies decide to the Fintype.card computation. The derived DecidableEq, Repr, BEq and Fintype instances on the five-constructor inductive type allow the tactic to evaluate the cardinality directly.
why it matters
The result supplies the five_families component of qecThresholdCert, which packages the cardinality together with positivity and phi-decay statements. It thereby closes the enumeration step required by the module's claim that five families realise configDim D = 5 and that adjacent thresholds differ by the factor 1/phi. The declaration sits inside the information-domain fragment of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.