Q_boundary_v
plain-language theorem explainer
The theorem shows that any interaction function P compatible with multiplicative consistency on F must obey the boundary relation P(a, 0) = 2a for every a in the image of the log-lifted cost G. Workers deriving the d'Alembert structure from Recognition Science axioms would invoke this result to fix the zero-argument slice of Q before differentiating the functional equation. The argument is a direct substitution: lift the consistency relation to additive form, set the second argument to zero, replace G(0) by the normalization, and finish with a
Claim. Let $F : (0,1] → ℝ$ satisfy $F(1) = 0$ and let $P : ℝ → ℝ → ℝ$ satisfy the multiplicative consistency $F(xy) + F(x/y) = P(Fx, Fy)$ for all $x,y > 0$. Define the log-lift $G(t) := F(e^t)$. Then for every $a ∈ ℝ$ in the range of $G$, one has $P(a, 0) = 2a$.
background
G_of is the log-lift that converts the original multiplicative consistency on F into an additive consistency on G: G(t+u) + G(t-u) = P(G(t), G(u)). The normalization hypothesis F(1) = 0 immediately yields G(0) = 0. The upstream lemma log_consistency performs exactly this change of variables, replacing the product-and-ratio arguments by sums and differences of the new variable t. The module AnalyticBridge uses these boundary facts to constrain the unknown combiner P before the differentiation step that produces the d'Alembert equation.
proof idea
One-line wrapper that applies log_consistency at the second argument zero, rewrites the resulting sum G(t) + G(t) by the normalization G_zero, substitutes the hypothesis that G(t) equals the target a, and concludes by linear arithmetic.
why it matters
This boundary identity is the first concrete constraint on the interaction function P inside the bridge theorem that forces d'Alembert structure from multiplicative consistency alone. It supplies the zero-slice needed for the subsequent differentiation argument that yields Q(a,b) = 2ab + 2a + 2b. The result sits between the normalization G_zero and the full ODE uniqueness statements that close the analytic bridge; without it the cross-derivative step cannot be anchored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.