ECCFamily
plain-language theorem explainer
The inductive definition enumerates the five canonical error-correcting code families in the J-cost model. Information theorists analyzing threshold rates on the phi-ladder cite this enumeration when bounding decodability via J(1/(1-r)) < J(phi). The definition is direct: five constructors with automatic derivation of DecidableEq, Repr, BEq, and Fintype.
Claim. Let $F$ be the inductive type whose elements are the five families: repetition codes, Hamming codes, BCH/Reed-Solomon codes, LDPC codes, and polar codes.
background
The module treats error-correction codes through J-cost, with five families fixed as configDim D = 5. Each family carries a threshold rate (Shannon capacity fraction) on the phi-ladder; adjacent families differ by the ratio 1/phi. A rate r < 1 is decodable precisely when J(1/(1-r)) lies below the canonical band J(phi) in (0.11, 0.13). The local setting is B16 Information Theory Depth, where the Shannon limit is the maximum rate 1.
proof idea
This is an inductive definition introducing the five constructors directly. Derivations of DecidableEq, Repr, BEq, and Fintype are automatic; no lemmas or tactics are invoked.
why it matters
The definition supplies the finite set required by the downstream ECCCert structure, which asserts cardinality exactly 5 together with positive and strictly decreasing threshold gaps. It anchors the enumeration step in the Recognition Science information layer, connecting to the phi-ladder and J-cost bounds on decoding thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.