continuous_composition_not_enough
plain-language theorem explainer
No real constant c exists making the quartic-log combiner equal 2a + 2b + c a b for all positive a, b. Researchers establishing the necessity of finite algebraic conditions for the RCL family cite this boundary result. The proof is a direct reference to the separate theorem that the quartic combiner lies outside the RCL bilinear family.
Claim. There does not exist a real constant $c$ such that for all positive reals $a,b$ the quartic-log combiner satisfies quarticCombiner$(a,b)=2a+2b+cab$.
background
The module shows that finite logical comparison on positive ratios forces the RCL family, with the finite-pairwise-polynomial condition named as its algebraic content. Counterexamples demonstrate why that finite condition cannot be dropped. The quarticCombiner is the continuous non-polynomial combiner associated to the quartic-log comparison on the nonnegative range. Its non-membership in the RCL bilinear family is recorded in the upstream theorem quarticCombiner_not_rcl_family.
proof idea
One-line wrapper that applies quarticCombiner_not_rcl_family.
why it matters
This boundary theorem shows continuity alone fails to force the Recognition Composition Law from logical comparison, supporting the module's sharpened claim that the finite algebraic condition is required. It sits inside the paper's finite logical comparison result and connects to the RCL identity used in the forcing chain (T5 J-uniqueness onward). No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.