canonicalRecognitionCostSystem_cost_one
plain-language theorem explainer
The canonical recognition cost system assigns zero cost to the multiplicative identity. Researchers formalizing the Recognition Science cost algebra cite this to confirm normalization of the J-cost function. The proof is a direct one-line application of the J_at_one normalization lemma.
Claim. Let $n,W$ be natural numbers with $W>0$. For the canonical recognition cost system $C_{n,W}$ whose cost function is the $J$-cost, one has $C_{n,W}(1)=0$.
background
The canonical recognition cost system is the quadruple $(ℝ₊,J,σ,W)$ with cost function given by $J$. The $J$-cost satisfies the normalization $J(1)=0$ by the upstream J_at_one result, which encodes that the multiplicative identity carries zero cost. This theorem simply transfers that property to the full system definition, which also carries the RCL_holds instance and the canonical sigma.
proof idea
One-line wrapper that applies the J_at_one theorem.
why it matters
The result locks in the zero-cost normalization for the identity inside the canonical system, which is required for the balance property and reciprocal symmetry of the Recognition Science cost algebra. It sits directly under the definition of canonicalRecognitionCostSystem and supports the J-uniqueness and RCL landmarks in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.