codeThreshold_pos
plain-language theorem explainer
The theorem shows that the QEC code threshold, given explicitly as the reciprocal of phi to the power k, is strictly positive for every natural number k. Workers on quantum error correction in the Recognition Science setting cite it to anchor the positivity of the predicted phi-ladder thresholds. The proof is a one-line wrapper that invokes the Mathlib inverse-positivity lemma on the positivity of phi raised to k.
Claim. For every natural number $k$, $0 < phi^{-k}$, where $phi$ is the self-similar fixed point from the Recognition Science constants.
background
The module treats QEC code families whose thresholds decay as powers of phi, with five families corresponding to configDim D = 5. The upstream definition supplies the explicit formula codeThreshold k := (phi ^ k)^{-1}. This matches the module's stated prediction that adjacent family thresholds stand in the ratio 1/phi and that the surface-code threshold is approximately phi^{-9}. The local setting therefore uses the phi-ladder to organize repetition, surface, colour, topological and concatenated codes.
proof idea
The proof is a one-line wrapper that applies inv_pos.mpr to pow_pos phi_pos k. Here inv_pos.mpr converts the positivity of a positive real into the positivity of its reciprocal, while pow_pos phi_pos k supplies the required positivity of phi^k from the positivity of phi itself.
why it matters
The result supplies the threshold_pos field inside the downstream qecThresholdCert definition, which also records the five-family count and the phi-decay property. It thereby certifies the RS prediction of phi^{-k} decay for topological codes and closes the positivity requirement for the information-theoretic part of the framework. The construction sits downstream of the forcing chain (T5-T8) that fixes phi and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.