surfaceCodeThreshold_pos
plain-language theorem explainer
Recognition Science predicts the surface-code fault-tolerance threshold as J(phi) divided by ten. Quantum information researchers comparing theoretical bands to experimental thresholds near one percent would cite this positivity result. The proof is a one-line term that unfolds the definition and applies division positivity to the already-established positivity of the numerator together with a numeric check on the denominator.
Claim. $0 < J(φ)/10$
background
The module derives a quantum error-correction threshold directly from the J-cost of a multiplicative recognizer. The cost function is the derived cost of the comparator on positive ratios; for any recognition event it equals the J-cost of the state. The surface-code threshold is defined as recognitionQuantum divided by ten, where recognitionQuantum is the RS prediction J(φ) shown positive by the upstream lemma that invokes phi greater than 1.5.
proof idea
One-line term proof. It unfolds the definition of surfaceCodeThreshold to recognitionQuantum / 10, then applies the lemma div_pos to the already-proved positivity of recognitionQuantum and the numeric fact that ten is positive.
why it matters
The result supplies the threshold_pos field of the ErrorCorrectionCert that packages positivity, cost at threshold, and cost non-negativity. It completes the structural theorem for the RS prediction that the surface-code threshold lies in the band (0.5, 2) percent, consistent with the empirical value near one percent. The construction rests on J-uniqueness (T5) and the phi fixed point (T6) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.