qecThresholdAt_pos
plain-language theorem explainer
Positivity of the QEC threshold at phi-ladder rung k holds for every natural number k. Quantum information researchers modeling fault-tolerant thresholds within Recognition Science cite this result to keep predicted error rates strictly positive. The proof is a one-line term that unfolds the definition and applies division positivity to the powered golden ratio.
Claim. For every natural number $k$, $0 < phi^{-k}/2$, where $phi$ denotes the golden ratio.
background
The module places the quantum error correction fault-tolerance threshold on the phi-ladder. Upstream, qecThresholdAt is defined as phi to the power of negative k divided by 2, with higher rungs producing lower thresholds below unity. Constants from LawOfExistence supplies the positivity of phi required for the argument.
proof idea
The term proof unfolds qecThresholdAt to expose the explicit form phi^{-k}/2. It then applies div_pos to zpow_pos of Constants.phi_pos together with a norm_num check that the denominator 2 is positive.
why it matters
This result supplies the positivity component for the QEC threshold certificate. It is invoked by qecThresholdAt_adjacent_ratio to obtain the phi inverse ratio between adjacent rungs and by qecThresholdCert to assemble the full certificate. In the Recognition Science framework it anchors the phi-ladder structure for QEC thresholds, consistent with the module's empirical bench for surface and colour codes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.