quarticLogComparison
plain-language theorem explainer
The quartic-log comparison operator supplies the function C(x, y) = [log(x/y)]^4 as a concrete counterexample in the study of functional equations for comparison costs. Workers on the Logic Functional Equation paper would cite it to demonstrate that a continuous symmetric combiner exists without forcing membership in the RCL family. The definition proceeds by direct assignment of the fourth power of the logarithm of the ratio to the ComparisonOperator type.
Claim. The quartic-log comparison operator is the function $C(x,y) = (log(x/y))^4$ on positive reals.
background
A ComparisonOperator is an abbreviation for a map from positive reals to reals that returns the cost of comparing two quantities, subject to four Aristotelian constraints that ensure the operation is well-posed under scale invariance. This module formalizes the algebraic heart of the counterexample from the Logic Functional Equation paper, where C(x,y) = (log (x/y))^4 admits a continuous symmetric combiner Φ(a,b) = 2a + 2b + 12 sqrt(a b) on the nonnegative range, yet no constant c makes the square-root term equal to c a b for all positive a,b. The upstream ComparisonOperator definition establishes the structural requirements for such cost functions.
proof idea
The definition is a one-line assignment that maps the pair (x, y) to the fourth power of the real logarithm of their ratio.
why it matters
This definition supplies the central counterexample showing that arbitrary continuous compositionality does not force the Recognition Composition Law family, as the quartic-log operator possesses a continuous symmetric combiner yet lacks a constant c making the square-root term bilinear. It fills the algebraic heart of the counterexample in the Logic Functional Equation paper, emphasizing that finite pairwise polynomial closure is essential. The result touches the open question of what minimal closure conditions suffice to recover the RCL from continuous combiners.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.