H_at_one
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the full d'Alembert equation.
- Does not address continuity or uniqueness of solutions.
- Does not connect to physical constants or spatial dimensions.
formal statement (Lean)
191theorem H_at_one : H 1 = 1 := by
proof body
Term-mode proof.
192 unfold H; rw [J_at_one]; ring
193
194/-- **THEOREM: H satisfies the standard d'Alembert equation.**
195 H(xy) + H(x/y) = 2·H(x)·H(y)
196
197 This is the canonical form of the multiplicative d'Alembert
198 functional equation, whose unique continuous solution is cosh. -/