J_reciprocal
plain-language theorem explainer
The recognition cost J satisfies J(x) equals J of its reciprocal for every nonzero real x. Domain certificate authors and cost algebra constructions cite this invariance under inversion to close the symmetry clause. The proof is a one-line wrapper that unfolds the definition of J and applies algebraic simplification.
Claim. For every real number $x$ with $x$ nonzero, the canonical recognition cost satisfies $J(x) = J(1/x)$, where $J(y) = (y + y^{-1})/2 - 1$.
background
The Canonical J-Cost Band module supplies reusable identities for the six-clause J-cost template used in master certificates and domain openings. J is defined as J(x) = (x + x inverse)/2 minus 1, which measures recognition cost on ratios. This theorem supplies the reciprocal symmetry clause of that template. It rests on the algebraic reciprocal result from Cost Algebra, which encodes double-entry invariance for positive ratios.
proof idea
The proof is a one-line wrapper. It unfolds the definition of J, then applies field simplification followed by the ring tactic to verify the equality.
why it matters
This result supplies the symmetric property required by canonicalCostAlgebra and is invoked in defectDist_symm, canonicalRecognitionCostSystem_cost_inv, and mechanical_thermal_symmetric. It completes the reciprocal clause in the module's six-clause template. Within Recognition Science it realizes the double-entry invariance that underpins the cost algebra and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.