H
plain-language theorem explainer
Definition H reparametrizes the log-shifted cost G_F by adding unity. T5 uniqueness proofs in the Recognition Science forcing chain cite it to obtain the d'Alembert form of the composition law. The construction is a direct abbreviation with no additional lemmas.
Claim. Let $G_F(t) = F(e^t)$. Define $H_F(t) := G_F(t) + 1$.
background
This module supplies auxiliary definitions for the T5 cost uniqueness argument. G re-expresses an arbitrary cost function F on the positive reals in logarithmic coordinates via $G_F(t) = F(e^t)$. The shifted version H then supplies the additive form of the functional equation that appears in the algebra of J-costs.
proof idea
The declaration is a one-line wrapper that applies the definition of G and adds one.
why it matters
This definition supports the chain of lemmas that establish uniqueness of the J-cost in the T5 step of the forcing chain. It appears in downstream results on energy conservation and Hamiltonian mechanics derived from the cost algebra, as well as in the cost algebra certificate that verifies the Recognition Composition Law. The construction closes part of the scaffolding for the eight-tick octave by providing clean notation for the functional equation proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.