ECCCert
ECCCert defines a structure that bundles the assertion of exactly five error-correction families together with the positivity and strict decrease of their threshold gaps on the phi-ladder. Information theorists citing Recognition Science results on J-cost bounds would reference it to confirm the basic counting and ordering facts before invoking decodability criteria. The declaration is a pure structure with no internal lemmas or tactics.
claimLet ECCFamily be the inductive type with five constructors (repetition, Hamming, BCH/Reed-Solomon, LDPC, polar). The structure ECCCert asserts that the cardinality of ECCFamily equals 5, that the threshold gap function satisfies $1/phi^k > 0$ for every natural number $k$, and that $1/phi^{k+1} < 1/phi^k$ for every $k$.
background
Recognition Science places error-correction thresholds on the phi-ladder via the J-cost function. The inductive ECCFamily enumerates the five canonical families whose threshold rates are spaced by successive factors of 1/phi. The auxiliary definition thresholdGap(k) supplies the explicit gap $1/phi^k$ to the Shannon limit, with deeper families closer to capacity.
proof idea
This is a structure definition whose body is empty. It directly records the three required properties by referencing the inductive ECCFamily and the closed-form thresholdGap without applying any lemmas or tactics.
why it matters in Recognition Science
ECCCert supplies the bundled facts that the downstream definition eccCert instantiates via eccFamily_count, thresholdGap_pos and thresholdGap_strictDecr. It records the five-family count (configDim D = 5) and the phi-ladder spacing required for the J-cost decodability band J(phi) in (0.11, 0.13) inside the Recognition framework.
scope and limits
- Does not derive the explicit J-cost expression for any family.
- Does not prove these five families exhaust all possible codes.
- Does not compute numerical gap values beyond the phi formula.
- Does not address concrete decoding algorithms or error probabilities.
formal statement (Lean)
50structure ECCCert where
51 five_families : Fintype.card ECCFamily = 5
52 threshold_always_pos : ∀ k, 0 < thresholdGap k
53 threshold_strictly_decreasing : ∀ k, thresholdGap (k + 1) < thresholdGap k
54