J_at_one
plain-language theorem explainer
The J-cost function evaluates to zero at the multiplicative identity 1. Researchers building canonical cost algebras or deriving mass ladders in Recognition Science cite this normalization to anchor the zero-cost reference. The proof is a one-line term application of the upstream Jcost_unit0 lemma that simplifies the squared-ratio definition of Jcost at unity.
Claim. $J(1) = 0$, where $J(x) = ½(x + x^{-1}) - 1$ is the unique cost function on positive reals satisfying the Recognition Composition Law.
background
In the CostAlgebra module the J-cost is the unique function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). It is realized explicitly by the formula J(x) = ½(x + x^{-1}) - 1, equivalently (x-1)^2/(2x). The local setting is the construction of CostAlgebraData, which packages cost, RCL satisfaction, normalization, symmetry and non-negativity into a single algebraic structure.
proof idea
The declaration is a term-mode one-line wrapper. It directly invokes the upstream lemma Jcost_unit0 (from both Cost.JcostCore and Cost) whose proof is simp [Jcost] on the squared-ratio definition.
why it matters
J_at_one supplies the normalization clause inside the cost_algebra_certificate and is required by canonicalCostAlgebra to assemble the canonical CostAlgebraData. It is invoked by canonicalRecognitionCostSystem_cost_one, defectDist_self, H_at_one and the mass derivations in BaselineDerivation. The result closes the normalization step of the J-uniqueness property (T5) in the forcing chain and supplies the zero-cost origin for the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.