Padd
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.