logical_error_positive
plain-language theorem explainer
The theorem establishes that Jcost(r) is strictly positive for any r > 0 with r ≠ 1. Researchers on quantum error correction thresholds in Recognition Science cite this to confirm physical errors produce positive cost. The proof is a direct one-line application of the upstream positivity lemma for Jcost.
Claim. If $r > 0$ and $r ≠ 1$, then $Jcost(r) > 0$.
background
The module Quantum Error Correction from J-Cost implements RS patent 015 on phi-harmonic QEC scheduling. Error correction is effective when the error rate produces J(r) below the band around J(φ) ∈ (0.11, 0.13); above that band the error is uncorrectable. Jcost is the cost function whose positivity for r ≠ 1 is the key property used here. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x ≠ 1 and x > 0, proved by rewriting Jcost as a square over a positive denominator and invoking sq_pos_of_ne_zero.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module directly to the hypotheses hr and hne.
why it matters
This supplies the error_positive field of the QECCert definition in the same module, which also records the five code families, below-threshold correctness, and DFT-8 mode count. It closes the logical-error half of the J-cost threshold argument in RS_PAT_015, separating correctable errors (J < J(φ)) from uncorrectable ones (J > J(φ)). The result sits inside the broader Recognition Science derivation of QEC from the single J functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.