thresholdGap_strictDecr
plain-language theorem explainer
The theorem shows that the decoding threshold gap decreases strictly as the error-correction family index k increases on the phi-ladder. Researchers formalizing the five canonical ECC families in Recognition Science cite this result to establish the ordering of repetition, Hamming, BCH, LDPC, and polar codes. The proof proceeds by unfolding the definition of thresholdGap and applying the strict monotonicity of powers of phi together with the reciprocal inequality for positive terms.
Claim. For every natural number $k$, the threshold gap satisfies $1/phi^{k+1} < 1/phi^k$, where the gap for family $k$ is defined as $1/phi^k$.
background
The module derives error-correction codes from the J-cost functional in Recognition Science. The thresholdGap function is defined as $1/phi^k$ for natural number $k$, representing the decoding threshold gap $1-r$ on the phi-ladder, with deeper families having smaller gaps. The local setting specifies five canonical ECC families with adjacent-family threshold ratio $1/phi$, and maximum rate 1 corresponding to the Shannon limit.
proof idea
The proof unfolds the definition of thresholdGap to reduce to showing $1/phi^{k+1} < 1/phi^k$. It establishes positivity of $phi^k$ and the strict growth $phi^k < phi^{k+1}$ using one_lt_phi and nlinarith after rewriting the successor power. The final step applies the lemma one_div_lt_one_div_of_lt to the positive terms.
why it matters
This theorem supplies the strict decrease property required by the ECCCert structure, which certifies the five families with positive and strictly decreasing thresholds. It fills the chain step for ordering the families on the phi-ladder in the information theory depth of the framework. The result supports the claim that deeper families approach the Shannon capacity more closely, consistent with the phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.