Q_boundary_u
plain-language theorem explainer
The theorem shows that if F satisfies F(1)=0, inversion symmetry for positive arguments, and the multiplicative consistency relation with combiner P, then P(0,b)=2b for every b in the image of the log-lift G_of F. Researchers deriving the d'Alembert structure from Recognition Science interaction axioms cite this boundary constraint when closing the additive case. The tactic proof applies the log-consistency lemma at zero, establishes evenness of G via symmetry, substitutes the zero value of G, and finishes with linear arithmetic.
Claim. Let $F:ℝ→ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for $x>0$, and $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$. Let $G(t)=F(e^t)$. Then $P(0,b)=2b$ whenever $b$ lies in the range of $G$.
background
The Analytic Bridge module proves that structural axioms on a cost function force the combiner to obey the d'Alembert functional equation. G_of is the log-lift defined by G_of F t := F(exp t), which converts the multiplicative consistency hypothesis into an additive equation on the real line. The hypothesis hCons is precisely the Recognition Composition Law re-expressed in these coordinates, with P encoding the interaction between two costs.
proof idea
The proof is a short tactic sequence. It introduces b together with a witness u such that G_of F u = b. It applies the sibling lemma log_consistency F P hCons at arguments 0 and u, then simplifies with zero_add and zero_sub. Evenness of G_of F follows from the symmetry hypothesis applied at exp u. Substitution of G_zero F hNorm (which gives G_of F 0 = 0) reduces the equation to 2b = P(0,b), which linarith resolves.
why it matters
This boundary result supplies one of the two endpoint conditions required by the Analytic Bridge theorem, which shows that interaction forces the combiner into d'Alembert form rather than a purely additive rule. It directly supports the step from J-uniqueness (T5) and the self-similar fixed point phi (T6) to the Recognition Composition Law. The lemma closes the additive side of the boundary before the module differentiates to obtain the full cross-term structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.