eccFamily_count
plain-language theorem explainer
The theorem asserts that the inductive type ECCFamily enumerating the five standard error-correction code families has finite cardinality exactly 5. Information theorists deriving bounds from the J-cost functional would cite this count to confirm the enumeration is complete before threshold calculations. The proof is a one-line decision procedure that evaluates the cardinality directly from the inductive definition with its five constructors.
Claim. The finite type of error-correction code families has cardinality five: $|ECCFamily| = 5$, where $ECCFamily$ consists of the repetition code, Hamming code, BCH/Reed-Solomon code, LDPC code, and polar code.
background
In the Error-Correction Codes from J-Cost module the Recognition Science framework constructs five canonical families whose threshold rates lie on the phi-ladder. The inductive definition ECCFamily lists repetition, hamming, bchReedSolomon, ldpc, and polar, deriving Fintype, DecidableEq, and Repr. Upstream gap functions from RSBridge.Anchor and Masses.AnchorPolicy supply the scaling $F(Z) = ln(1 + Z/phi)/ln(phi)$ that underlies J-cost thresholds for information defects. The module states that any rate $r < 1$ is decodable iff $J(1/(1-r)) < J(phi)$ in the band (0.11, 0.13).
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card ECCFamily = 5. Because ECCFamily derives Fintype from its five constructors, Lean computes the cardinality by exhaustive enumeration without invoking further lemmas.
why it matters
This cardinality supplies the five_families field of the eccCert certificate, which also records positive and strictly decreasing threshold gaps. It completes the enumeration step in the B16 Information Theory Depth section, confirming configDim D = 5 for J-cost derived families. The result sits inside the phi-ladder scaling and eight-tick octave structure, though its precise link to the spatial dimension D = 3 remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.