quarticCombiner_symmetric
plain-language theorem explainer
The quartic combiner satisfies symmetry under argument interchange for all real inputs. Researchers examining functional equations for continuous compositionality cite this to establish that the proposed non-polynomial combiner meets the symmetry requirement before testing bilinearity. The proof proceeds by direct unfolding of the definition followed by commutativity of multiplication and ring simplification.
Claim. For all real numbers $a,b$, the quartic combiner satisfies $2a + 2b + 12 sqrt(a b) = 2b + 2a + 12 sqrt(b a)$.
background
The module constructs an algebraic counterexample to show that the quartic-log function $C(x,y) = (log(x/y))^4$ admits a continuous symmetric combiner on the nonnegative reals, yet that combiner cannot be made bilinear. The upstream definition supplies the explicit form of the combiner: noncomputable def quarticCombiner (a b : ℝ) : ℝ := 2 * a + 2 * b + 12 * Real.sqrt (a * b). This combiner is continuous and symmetric but the square-root term fails to factor as a constant times a b for all positive a,b, separating mere continuity from the Recognition Composition Law family.
proof idea
The proof is a one-line wrapper that unfolds the definition of quarticCombiner, rewrites using commutativity of multiplication on the product inside the square root, and closes with the ring tactic.
why it matters
This symmetry lemma is an immediate prerequisite inside the quartic-log counterexample module. The module itself demonstrates that continuous symmetric compositionality on the nonnegative range does not force the RCL family without finite pairwise polynomial closure. It therefore isolates the necessity of the polynomial condition that appears in the Recognition Composition Law derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.