H_at_one
plain-language theorem explainer
H(1) equals 1 for the shifted cost H(x) = J(x) + 1. Algebraists working on the Recognition Composition Law cite this normalization when converting the law into d'Alembert form. The proof is a one-line algebraic reduction that unfolds H, substitutes J(1) = 0, and simplifies.
Claim. Let $H(x) = J(x) + 1$. Then $H(1) = 1$.
background
In CostAlgebra the shifted cost is defined by H(x) := J(x) + 1, which equals (x + x^{-1})/2. This reparametrization turns the Recognition Composition Law into the standard d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The local setting is the algebra of the J-cost function on positive reals. The result rests on the upstream theorem J_at_one, which states that the base cost satisfies J(1) = 0.
proof idea
The proof is a one-line wrapper that unfolds the definition of H, rewrites with J_at_one, and closes by the ring tactic.
why it matters
This normalization is required before the d'Alembert equation for H can be stated and solved. It feeds the derivation of the canonical multiplicative form whose continuous solutions are cosh. In the Recognition framework it supports the step from J-uniqueness to the phi fixed point and the eight-tick octave. No open scaffolding is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.