quartic_sqrt_term_not_bilinear
plain-language theorem explainer
No real constant c satisfies 12 sqrt(a b) = c a b for all positive reals a and b. Recognition Science researchers cite this fact when separating the quartic-log combiner from the RCL bilinear family. The tactic proof assumes such a c exists, fixes its value at 12 by evaluation at (1,1), and derives a numerical contradiction at (4,4).
Claim. There does not exist a real number $c$ such that for all positive real numbers $a$ and $b$, $12 sqrt(a b) = c a b$.
background
The module formalizes the algebraic core of a counterexample from the Logic Functional Equation paper. The quartic combiner is the symmetric function Φ(a,b) = 2a + 2b + 12 sqrt(a b) that arises from C(x,y) = (log(x/y))^4 on nonnegative arguments. The Recognition Composition Law (RCL) requires that any admissible combiner belong to a bilinear family of the form 2a + 2b + c a b for some fixed c. Upstream results on collision-free empirical programs and simplicial edge lengths supply the surrounding foundation in which this algebraic separation is needed.
proof idea
The tactic proof begins by introducing the existential witness c and the universal hypothesis. It specializes the hypothesis at a=1, b=1 and uses norm_num together with linarith to conclude c=12. It then specializes at a=4, b=4, rewrites the square root of 16 as 4, substitutes the value of c, and obtains the false equality 48=192 by norm_num.
why it matters
The result is invoked directly by quarticCombiner_not_rcl_family to establish that the full quartic combiner lies outside the RCL bilinear family. It supplies the concrete algebraic step required by the paper's counterexample, showing that continuous symmetric compositionality alone does not force the RCL identity. The declaration therefore underscores why finite pairwise polynomial closure must be imposed separately in the Recognition Science foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.