H_of
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish existence or uniqueness of the combiner P.
- Does not derive the RCL form of P from interaction.
- Does not assume differentiability or smoothness of F.
- Does not connect to specific constants such as G or the fine-structure interval.
formal statement (Lean)
50noncomputable def H_of (F : ℝ → ℝ) (t : ℝ) : ℝ := G_of F t + 1
proof body
Definition body.
51
52/-! ## Consistency in Log-Coordinates -/
53
54/-- If F has multiplicative consistency, then G has additive consistency. -/