recognitionQuantum_eq_Jph
plain-language theorem explainer
The equality recognitionQuantum = Jcost phi holds by direct substitution of the shared closed-form value phi - 3/2. Quantum information theorists modeling surface-code thresholds in Recognition Science would cite this link to anchor the predicted 1.18% fault-tolerance band. The proof is a one-line rewrite that applies the definition of recognitionQuantum together with the precomputed lemma Jcost_phi_val.
Claim. The recognition quantum equals the J-cost evaluated at the golden ratio: $recognitionQuantum = Jcost(phi)$, where $Jcost$ is the Recognition Science cost function and $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
The module Quantum Error Correction Threshold from J-Cost develops the RS prediction that the surface-code fault-tolerance threshold lies near J(phi)/10. The sibling definition recognitionQuantum : ℝ := phi - 3/2 supplies the left-hand side. The upstream lemma Jcost_phi_val states that Cost.Jcost phi = phi - 3/2 exactly, using the identity phi² = phi + 1 together with algebraic simplification and positivity of phi.
proof idea
The proof is a one-line wrapper that applies the rewrite tactic to the two identifiers in the goal. It first unfolds the definition of recognitionQuantum, then replaces the resulting expression with the closed form supplied by Jcost_phi_val.
why it matters
This equality confirms that the recognition quantum coincides with the J-cost at phi, which directly supports the module's structural claim that the surface-code threshold approximates J(phi)/10 ≈ 1.18% and lies inside the empirical band 0.5-2%. It closes the identification step inside the QuantumComputing.ErrorCorrectionThresholdFromJCost development and feeds the downstream constants used for error-rate bounds. The module falsifier remains any engineered surface code whose measured threshold falls outside [0.1%, 2%].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.