canonicalThreshold_pos
plain-language theorem explainer
The canonical error-correction threshold built from the J-cost at φ is strictly positive. Anyone using the RS Hamming-bound rate R = J(φ) ≈ 0.118 or the supported fraction t/n = J(φ)/2 needs this fact. The proof is a one-line unfold plus linear arithmetic from the elementary bound φ > 1.5.
Claim. The canonical error-correction threshold (the positive real constant obtained by unfolding the module's threshold definition in terms of $\varphi$) satisfies $0 < \ thr$.
background
This module derives a structural Hamming-bound capacity statement from the Recognition Science J-cost. The Hamming bound requires $2^{n-k} \ge V_H(n,t)$ with $V_H$ the ball volume; RS specializes to rate $R = J(\varphi) \approx 0.118$ and supported error fraction $t/n = J(\varphi)/2 \approx 0.059$.
The cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law (T5): $J(x) = (x+x^{-1})/2-1$. The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point (T6). The module defines a canonical threshold constant from these data; the present lemma only records its positivity.
Upstream, phi_gt_onePointFive supplies the tight elementary bound $\varphi > 1.5$ (from $\sqrt{5} > 2$).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting strict inequality by linarith using the single lemma $\varphi > 1.5$. No further algebraic identities are required.
why it matters
Positivity of the threshold is the minimal arithmetic fact needed before any certificate can assert a positive error-correction capacity at the J-cost rate. The module status is structural (0 sorry, 0 axiom); this lemma sits at the base of that certificate stack (ErrCorr3DeepCert, cert, cert_inhabited).
It ties the information-theoretic side of RS to the forcing chain: T5 uniqueness of $J$ and T6 forcing of $\varphi$. No downstream dependents are recorded in the graph yet; the lemma is local scaffolding for the three-deep error-correction claim rather than a widely reused library fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.