quarticLogComparison
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish that the quartic-log operator satisfies the full set of Aristotelian constraints.
- Does not derive the continuous symmetric combiner Φ(a,b) = 2a + 2b + 12 sqrt(a b).
- Does not prove the absence of a constant c that would make the combiner bilinear.
- Does not connect to the eight-tick octave or spatial dimensions in the Recognition Science chain.
formal statement (Lean)
28noncomputable def quarticLogComparison : ComparisonOperator :=
proof body
Definition body.
29 fun x y => (Real.log (x / y)) ^ (4 : Nat)
30
31/-- The continuous non-polynomial combiner associated to the quartic-log
32comparison on the nonnegative range. -/