quarticCombiner_nonneg_on_nonneg
plain-language theorem explainer
The quartic combiner 2a + 2b + 12 sqrt(ab) is nonnegative for all nonnegative real inputs a and b. Researchers examining continuous symmetric combiners in functional equations would cite this result to anchor the nonnegative cone property of the quartic-log counterexample. The proof is a short tactic sequence that unfolds the definition and applies positivity followed by linear arithmetic on the three terms.
Claim. For all real numbers $a,b$ with $a≥0$ and $b≥0$, the expression $2a + 2b + 12√(ab)$ is nonnegative.
background
The module formalises the algebraic core of the quartic-log counterexample: the function C(x,y)=(log(x/y))^4 admits the continuous symmetric combiner Φ(a,b)=2a+2b+12√(ab) on the nonnegative reals, yet the square-root term cannot be replaced by any fixed multiple c·ab for all positive a,b. This shows that arbitrary continuous compositionality fails to force the Recognition Composition Law family; finite pairwise polynomial closure is required instead. The local definition quarticCombiner supplies exactly this Φ, and the present theorem records its nonnegativity on the domain of interest.
proof idea
The tactic proof introduces a and b together with the two nonnegativity hypotheses, unfolds the definition of quarticCombiner, generates three separate nonnegativity facts for 2a, 2b and 12√(ab) via the positivity tactic, and closes the goal with linarith.
why it matters
This lemma supplies the nonnegativity anchor for the quartic-log counterexample that demonstrates why continuous symmetric combiners alone do not imply the Recognition Composition Law. It sits inside the LogicAsFunctionalEquation development and directly supports the claim that polynomial closure is essential. The surrounding module contrasts the quartic case with the RCL family derived from the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.