eccCert
plain-language theorem explainer
The definition constructs an explicit certificate asserting exactly five error-correction code families on the phi-ladder, each with positive and strictly decreasing threshold gaps. Information theorists in Recognition Science would cite it to confirm the canonical count of five families and their rate thresholds derived from J-cost. The definition is a direct record constructor that assembles the certificate from three prior lemmas on family cardinality and gap properties.
Claim. Define the certificate with fields: the cardinality of the set of error-correction families equals 5, the threshold gap is positive for every natural number $k$, and the threshold gap is strictly decreasing in $k$.
background
The module develops error-correction codes from the J-cost function. It identifies five canonical families (repetition, Hamming, BCH/Reed-Solomon, LDPC, polar) corresponding to dimension D=5. Each family has a decoding threshold gap on the phi-ladder, where adjacent-family ratios equal 1/phi and deeper families approach the Shannon limit of rate 1. Any rate r < 1 is decodable when J(1/(1-r)) lies below the canonical band J(phi) in (0.11, 0.13).
proof idea
This definition is a one-line record constructor that supplies the three fields of the certificate directly from the lemmas establishing family cardinality equal to 5, positivity of all threshold gaps via division of positives, and strict decrease via the growth of successive powers of phi.
why it matters
This declaration supplies the concrete certificate for the five-family structure in the B16 information theory section. It closes the local development by confirming the phi-ladder thresholds for the canonical ECC families. The result supports the broader claim that maximum achievable rate reaches 1 with decodability conditioned on J-cost bounds. It touches the open question of explicit mappings from J-cost to specific code parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.