H_of
plain-language theorem explainer
H_of defines the shifted log-lift H_F(t) = G_F(t) + 1 with G_F(t) = F(exp t). Researchers deriving the d'Alembert equation from multiplicative consistency and interaction axioms would cite this shift. The definition is a direct abbreviation that aligns the log-reparametrized cost function with the homogeneous form required by the RCL combiner.
Claim. Let $H_F(t) := G_F(t) + 1$, where $G_F(t) = F(e^t)$.
background
The Analytic Bridge module proves that structural axioms on a cost function F together with an interaction combiner force the d'Alembert functional equation on its log-lift. The log-lift G_of reparametrizes F via t = log x so that G(t) = F(e^t). Adding the constant 1 produces the shifted version H that converts the multiplicative consistency equation into the additive d'Alembert relation H(t+u) + H(t-u) = 2 H(t) H(u).
proof idea
This is a one-line definition that applies G_of and adds the constant 1. No lemmas or tactics are used beyond the definition of G_of itself.
why it matters
H_of supplies the precise form required by the Analytic Bridge Theorem (analytic_bridge) and its full version (analytic_bridge_full). These theorems show that multiplicative consistency plus structural axioms and interaction imply the d'Alembert equation for H_of when the combiner takes the RCL form P(u,v) = 2uv + 2u + 2v. The shift therefore closes the step from the Recognition Composition Law to the d'Alembert structure that appears in the forcing chain after J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.