double_counting_not_allowed
plain-language theorem explainer
Continuous non-counted composition fails to force the RCL family because the quartic-log combiner introduces a square-root interaction term that cannot be absorbed into a bilinear form. Researchers deriving the Recognition Composition Law from counted-once comparisons cite this to exclude alternative continuous combiners. The argument is a direct application of the upstream non-bilinearity result for the quartic combiner.
Claim. There does not exist a real number $c$ such that for all positive reals $a,b$, the quartic-log combiner satisfies $2a + 2b + 12√(ab) = 2a + 2b + c ab$.
background
The module formalises the requirement that each constituent comparison is counted once. Algebraically this means the combiner is affine in each variable separately, taking the form $a + b u + c v + d u v$. Identity and symmetry then force the RCL-family form, per the module documentation. The quartic-log combiner is the continuous function $f(a,b) = 2a + 2b + 12 √(ab)$. An upstream result establishes that this function lies outside the RCL bilinear family because its square-root interaction term cannot be expressed as a constant multiple of $ab$.
proof idea
The proof is a one-line wrapper that applies the upstream theorem establishing the quartic combiner is not in the RCL family. That result assumes such a $c$ exists and derives a contradiction by isolating the square-root term.
why it matters
This result shows that continuous non-counted composition does not suffice to force the RCL family. It supports the parent claim that only counted-once combiners yield the Recognition Composition Law. In the Recognition Science framework it reinforces the derivation of the functional equation from J-uniqueness and the self-similar fixed point. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.