thresholdGap_pos
plain-language theorem explainer
Positivity of the threshold gap 1/phi^k holds for every natural number k. Information theorists modeling the five canonical ECC families on the Recognition Science phi-ladder cite it to guarantee strictly positive decoding margins below the Shannon limit. The term proof unfolds the definition of thresholdGap and applies div_pos one_pos together with pow_pos phi_pos k.
Claim. For every natural number $k$, the threshold gap satisfies $0 < 1/phi^k$, where $phi$ is the self-similar fixed point and the right-hand side is the gap $1-r$ for the $k$-th family on the $phi$-ladder.
background
The module treats error-correction codes derived from J-cost, defining five canonical families (repetition, Hamming, BCH/Reed-Solomon, LDPC, polar) whose threshold rates lie on the phi-ladder with adjacent-family ratios equal to 1/phi. The upstream definition thresholdGap k := 1/phi^k supplies the explicit gap 1-r for rung k, with the maximum achievable rate 1 at the Shannon limit and decodability conditioned on J(1/(1-r)) lying below the canonical band J(phi). This sits inside the broader Recognition Science setting where phi arises as the fixed point forced by the T0-T8 chain.
proof idea
Term-mode one-liner: unfold thresholdGap reduces the goal to 0 < 1/phi^k, after which div_pos one_pos (pow_pos phi_pos k) discharges the inequality using the standard positivity axioms for division, the unit, and positive-base exponentiation.
why it matters
The result populates the threshold_always_pos field inside the eccCert record that certifies the five families. It anchors the required positivity of all phi-ladder thresholds in the Information layer, directly supporting the J-cost band condition and the 1/phi spacing between families. No open scaffolding remains on this point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.