H
plain-language theorem explainer
The shifted cost H(x) = J(x) + 1 reparametrizes the J-cost to convert the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Researchers deriving energy conservation or Hamilton's equations from the cost algebra would cite this reparametrization. It is a direct definition that adds one to the J-cost function.
Claim. Define the shifted cost by $H(x) := J(x) + 1 = {1/2}(x + x^{-1})$. Under this shift the Recognition Composition Law becomes the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$.
background
J is the unique cost satisfying the Recognition Composition Law, given explicitly by J(x) = ½(x + x⁻¹) − 1 with J(1) = 0. The CostAlgebra module assembles algebraic consequences of this law, including reciprocal symmetry and non-negativity on the positive reals. Upstream, the FunctionalEquation module introduces an analogous reparametrization H_F t = G_F t + 1 that yields the cosh-type functional identity.
proof idea
Direct definition: H x := J x + 1. It inherits the algebraic properties of J and the reparametrization pattern from the upstream FunctionalEquation.H.
why it matters
This definition feeds the energy conservation certificate and the Hamiltonian derivations in the Action module. The doc-comment notes that it converts the Recognition Composition Law into standard d'Alembert form. In the framework it supports the transition from J-uniqueness (T5) toward the eight-tick octave (T7) and D = 3, appearing inside the cost algebra certificate that verifies RCL, normalization, and symmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.