quarticCombiner_not_rcl_family
plain-language theorem explainer
The quartic combiner Φ(a, b) = 2a + 2b + 12√(ab) cannot be rewritten in the bilinear form 2a + 2b + c ab for any fixed real c and all positive a, b. Researchers examining functional equations for composition laws cite this to show that continuity of a symmetric combiner alone fails to force the bilinear structure required by the Recognition Composition Law. The proof is a direct reduction that assumes such a c, unfolds the combiner definition, and invokes the separate non-bilinearity of the isolated square-root term.
Claim. There does not exist a real number $c$ such that $2a + 2b + 12√(ab) = 2a + 2b + c ab$ for all positive real numbers $a, b$.
background
The quartic combiner is the continuous symmetric function Φ(a, b) := 2a + 2b + 12 √(a b) on the nonnegative reals, obtained from the quartic-log comparison C(x, y) = (log(x/y))^4. This module isolates the algebraic obstruction that prevents Φ from belonging to the bilinear family even though it is continuous and symmetric. The key upstream result is the theorem establishing that the isolated square-root term 12 √(a b) cannot equal c a b for any single c across all positive inputs.
proof idea
The proof assumes for contradiction that a witness c exists, extracts it via rcases, unfolds the definition of quarticCombiner, and applies the upstream theorem quartic_sqrt_term_not_bilinear. The final step uses linarith on the resulting equality after substitution.
why it matters
This supplies the algebraic core for the boundary theorems double_counting_not_allowed and continuous_composition_not_enough. Those results establish that arbitrary continuous composition is insufficient to force the RCL bilinear family, because the quartic-log combiner introduces a non-polynomial square-root interaction. In the Recognition Science framework the declaration closes the counterexample showing that finite pairwise polynomial closure, rather than mere continuity, is required to reach the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.