Padd
Padd supplies the additive combiner P(u, v) = 2u + 2v that satisfies the functional equation for the quadratic log-cost F(x) = (log x)^2 / 2. Researchers studying why existence of a combiner fails to force d'Alembert structure on the log-lift cite this definition to motivate nondegeneracy axioms. It is introduced by direct assignment in the counterexamples module.
claimThe combiner function satisfies $P(u, v) = 2u + 2v$.
background
The Counterexamples module shows that existence of some combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert equation on the shifted log-lift. Here F is the quadratic log-cost F(x) = (log x)^2 / 2, which admits the additive combiner P(u, v) = 2u + 2v, yet H(t) = t^2/2 + 1 fails d'Alembert. The module concludes that any forcing theorem from weak existence of P requires at least one further nondegeneracy axiom. The same additive combiner appears upstream in EntanglementGate to establish separability.
proof idea
The definition is a direct one-line assignment of the expression 2 * u + 2 * v. No lemmas or tactics are applied.
why it matters in Recognition Science
Padd provides the separable, non-entangling combiner that serves as the counterexample to weak forcing of the Recognition Composition Law. It is invoked in entanglement_gate_theorem to show Jcost has interaction while Padd does not entangle, and in Fquad_consistency to verify the equation holds for the quadratic case. This fills the structural obstruction noted in the module doc and touches the question of minimal axioms needed beyond existence of P.
scope and limits
- Does not assert that Padd satisfies d'Alembert for arbitrary F.
- Does not claim uniqueness of the combiner.
- Does not apply to non-quadratic costs.
- Does not guarantee the log-lift satisfies d'Alembert.
formal statement (Lean)
43noncomputable def Padd (u v : ℝ) : ℝ := 2 * u + 2 * v
proof body
Definition body.
44