canonicalRecognitionCostSystem_cost_inv
plain-language theorem explainer
The canonical recognition cost system inherits invariance of its cost function under inversion of positive arguments. Researchers modeling double-entry bookkeeping in recognition costs or symmetry properties of the J-cost would cite this result. The proof is a direct one-line application of the J_reciprocal lemma to the cost field of the canonical system.
Claim. Let $n, W$ be natural numbers with $W > 0$. For the canonical recognition cost system on positive reals, whose cost function is the $J$-cost, one has $J(x) = J(x^{-1})$ whenever $x > 0$.
background
The canonical recognition cost system is the structure $(ℝ₊, J, σ, W)$ whose cost component is exactly the function $J$. The upstream lemma J_reciprocal states that $J x = J x^{-1}$ for $x > 0$, which is the algebraic encoding of reciprocal symmetry. This symmetry is the concrete realization of the Recognition Composition Law (RCL) applied to the pair $(x, x^{-1})$. The definition of the system itself appears in the same module and simply packages $J$ together with the already-proved RCL_holds and a canonical sigma map.
proof idea
The proof is a one-line wrapper that applies the lemma J_reciprocal directly to the cost field of the canonicalRecognitionCostSystem instance.
why it matters
This theorem closes the inheritance step that lets the full RecognitionCostSystem carry the reciprocal symmetry already established for $J$. It sits inside the algebra layer that feeds the forcing chain (T5 J-uniqueness) and supplies the double-entry property required by downstream cost-composition results. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.