quarticCombiner
plain-language theorem explainer
quarticCombiner defines the continuous symmetric combiner Φ(a, b) = 2a + 2b + 12√(ab) on the nonnegative reals that arises directly from the quartic-log counterexample C(x, y) = (log(x/y))^4. Researchers studying the boundary between arbitrary continuous composition and the Recognition Composition Law would cite this explicit form. The definition is introduced as a direct algebraic expression without lemmas or computation.
Claim. Define the combiner function Φ(a, b) := 2a + 2b + 12√(ab) for real numbers a, b.
background
This module formalises the algebraic heart of the counterexample from the Logic Functional Equation paper: C(x,y) = (log (x/y))^4 has a continuous symmetric combiner on the nonnegative range, Φ(a,b) = 2a + 2b + 12 sqrt(a b), but no constant c can make the square-root term equal to c a b for all positive a,b. Thus arbitrary continuous compositionality does not force the RCL family; finite pairwise polynomial closure is essential.
proof idea
The definition is supplied directly by the algebraic expression 2 * a + 2 * b + 12 * Real.sqrt (a * b). It is a one-line definition encoding the continuous non-polynomial combiner with no lemmas applied.
why it matters
This definition supplies the explicit combiner used by quarticCombiner_not_rcl_family to prove that no c makes it bilinear and by continuous_composition_not_enough to establish that arbitrary continuous composition is not enough to force the RCL family. It illustrates why the Recognition Composition Law requires finite pairwise polynomial closure rather than mere continuity, consistent with the forcing chain landmarks T5 J-uniqueness and T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.