qecCodeFamilyCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive numerical threshold values for any family.
- Does not prove the phi-decay relation between thresholds.
- Does not address error models or physical implementations.
- Does not extend the enumeration beyond the five listed constructors.
Lean usage
five_families := qecCodeFamilyCountformal statement (Lean)
29theorem qecCodeFamilyCount : Fintype.card QECCodeFamily = 5 := by decide
proof body
30