continuous_composition_not_enough
plain-language theorem explainer
Continuous composition fails to force the RCL bilinear family, as shown by the existence of a quartic-log combiner that satisfies a continuous comparison on positive ratios yet deviates from any form 2a + 2b + c a b. Researchers sharpening the finite logical comparison theorem in Recognition Science cite this boundary result to establish why the finite algebraic condition cannot be dropped. The argument reduces directly to the prior lemma that places the quartic combiner outside the RCL family.
Claim. There does not exist a real number $c$ such that for all positive real numbers $a$ and $b$, the quartic-log combiner satisfies quarticCombiner$(a,b) = 2a + 2b + c a b$.
background
The module packages the sharpened claim that finite logical comparison on positive ratios forces the RCL family, with counterexamples demonstrating the necessity of the finite algebraic content. The quarticCombiner is the continuous non-polynomial combiner associated to the quartic-log comparison on the nonnegative range, given explicitly by $2a + 2b + 12 sqrt(a b)$. The upstream theorem quarticCombiner_not_rcl_family establishes that this combiner lies outside the RCL bilinear family.
proof idea
The proof is a one-line wrapper that applies the quarticCombiner_not_rcl_family lemma.
why it matters
This boundary theorem shows that arbitrary continuous composition is not enough to force the RCL family, thereby supporting the module's central claim that finite logical comparison is required. It directly illustrates the Recognition Composition Law by exhibiting a continuous function that violates the bilinear form while still arising from a quartic-log comparison. No downstream uses are recorded yet; the result closes a potential loophole in the forcing chain from finite comparison to RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.