continuous_composition_not_enough
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not claim that no continuous functions can satisfy the RCL equation.
- Does not classify all possible continuous combiners on positive reals.
- Does not address discrete or finite-pairwise cases.
- Does not provide a general criterion for when continuity plus comparison forces RCL.
formal statement (Lean)
90theorem continuous_composition_not_enough :
91 ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
92 quarticCombiner a b = 2 * a + 2 * b + c * a * b :=
proof body
Term-mode proof.
93 quarticCombiner_not_rcl_family
94
95/-- Searchable boundary theorem: analytic composition is not enough to force
96degree-two RCL form. -/