recognitionQuantum_pos
plain-language theorem explainer
recognitionQuantum_pos establishes that the recognition quantum J(φ) equals φ minus 3/2 and is strictly positive. Quantum error correction researchers cite it to fix the sign of the RS-predicted surface-code threshold near 1.18 percent. The proof is a one-line wrapper that unfolds the definition and applies linarith to the bound φ greater than 1.5.
Claim. $0 < J(φ)$ where $J(φ) = φ - 3/2$ and $φ = (1 + √5)/2$ is the golden ratio.
background
The module develops quantum error correction thresholds from J-cost. recognitionQuantum is defined as phi minus 3/2, which equals the recognition function J evaluated at the golden ratio φ. The local setting is a structural theorem giving the RS prediction that the surface-code fault-tolerance threshold is approximately J(φ)/10, or 1.18 percent, inside the empirical band 0.5 to 2 percent.
proof idea
The proof is a one-line wrapper. It unfolds recognitionQuantum to phi minus 3/2, then applies linarith to the upstream lemma phi_gt_onePointFive that establishes 1.5 less than phi.
why it matters
The result is invoked directly by surfaceCodeThreshold_pos to obtain positivity of the surface-code threshold. It completes the structural theorem of the module and anchors the RS prediction J(φ)/10 inside the observed consistency band. The step traces to J-uniqueness at forcing-chain step T5 and the self-similar fixed point at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.