thresholdGap
The declaration defines the threshold gap on the φ-ladder as Δ(k) = φ^{-k} for family index k. Information theorists modeling ECC families in Recognition Science cite it to quantify how deeper codes approach the Shannon limit via geometric shrinkage by 1/φ. The definition is a direct algebraic expression with no computational steps or lemmas required.
claimThe decoding threshold gap for the k-th family on the φ-ladder is defined by $Δ(k) := φ^{-k}$.
background
The module treats five canonical ECC families (repetition, Hamming, BCH/Reed-Solomon, LDPC, polar) whose threshold rates lie on the φ-ladder. Adjacent families differ by a factor 1/φ in their gap to capacity, with maximum rate 1. A rate r is decodable precisely when J(1/(1-r)) lies below the band J(φ) ∈ (0.11, 0.13). The definition supplies the explicit gap size 1-r = φ^{-k} used to certify these families.
proof idea
Direct definition: thresholdGap k is introduced as the term 1 / phi ^ k. No lemmas or tactics are invoked; the expression serves as the base for the positivity and strict-decrease theorems that follow.
why it matters in Recognition Science
This definition populates the ECCCert structure, which asserts five families together with positive and strictly decreasing gaps. It supplies the concrete φ-ladder spacing required by the B16 Information Theory Depth step, linking J-cost bounds to explicit ECC thresholds. In the Recognition framework the geometric shrinkage by φ^{-1} each step quantifies approach to the Shannon limit.
scope and limits
- Does not prove existence or completeness of the five families.
- Does not derive the J-cost decoding condition from first principles.
- Does not compute numerical thresholds for concrete codes.
- Does not address non-canonical or hybrid families.
formal statement (Lean)
34noncomputable def thresholdGap (k : ℕ) : ℝ := 1 / phi ^ k
proof body
Definition body.
35