qecThresholdAt_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the specific rung assignments for surface or colour codes.
- Does not derive the phi-ladder placement from the unified forcing chain.
- Does not quantify exponential suppression of logical errors.
- Does not address thresholds outside the phi-ladder model.
Lean usage
example (k : ℕ) : 0 < qecThresholdAt k := qecThresholdAt_pos kformal statement (Lean)
35theorem qecThresholdAt_pos (k : ℕ) : 0 < qecThresholdAt k := by
proof body
Term-mode proof.
36 unfold qecThresholdAt
37 exact div_pos (zpow_pos Constants.phi_pos _) (by norm_num)
38