H_dAlembert
plain-language theorem explainer
H satisfies the multiplicative d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) for positive reals x and y. Researchers assembling cost algebras or solving functional equations in Recognition Science cite this identity. The argument unfolds H in terms of J, invokes the RCL theorem, and closes via ring identities after adding a constant shift.
Claim. For all positive real numbers $x,y$, the shifted cost $H(z) := J(z) + 1$ obeys $H(xy) + H(x/y) = 2 H(x) H(y)$, where $J$ satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.
background
H is the shifted cost defined by $H(x) = J(x) + 1$, equivalently half of $(x + x^{-1})$. This reparametrization turns the Recognition Composition Law into the canonical d'Alembert form. The CostAlgebra module collects algebraic consequences of the cost functional equation under positive reals. RCL_holds supplies the base identity for the underlying $J$ function.
proof idea
Unfold H and J to reach Jcost terms. Apply RCL_holds to obtain the raw composition identity. Form hsum by adding 2 to both sides and simplifying with add_assoc, add_left_comm, add_comm. Obtain hmul by direct ring expansion of the product form. The calc block equates the shifted sum to the RCL side via hsum then matches the product via hmul.symm.
why it matters
The result supplies a required algebraic identity inside cost_algebra_certificate, which verifies the complete cost algebra package including RCL satisfaction and normalization. It realizes the passage from the primitive Recognition Composition Law to the d'Alembert equation whose continuous solutions are hyperbolic cosines, consistent with J-uniqueness in the forcing chain. The step supports the single-functional-equation derivation of physics constants and dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.