thresholdGap
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.