quarticCombiner
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not assert that the combiner satisfies the Recognition Composition Law for any c.
- Does not extend the domain to negative reals where the square root may fail to be real.
- Does not claim that this is the unique continuous combiner for the quartic-log comparison.
formal statement (Lean)
33noncomputable def quarticCombiner (a b : ℝ) : ℝ :=
proof body
Definition body.
34 2 * a + 2 * b + 12 * Real.sqrt (a * b)
35