counted_once_combiner_forces_rcl
plain-language theorem explainer
An operative positive-ratio comparison operator whose derived-cost composition counts each input once must belong to the RCL family. Researchers formalizing the functional-equation basis of Recognition Science cite this when bridging single-use resource constraints to the quadratic combiner form. The term-mode proof destructures the CountedOnceComposition hypothesis into an affine symmetric combiner and invokes rcl_direct_theorem to extract the required multiplicative consistency constant.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator satisfying the operative positive-ratio conditions (identity, non-contradiction, continuity, scale invariance, non-triviality). If the derived cost $F(r) = C(r,1)$ obeys counted-once composition, i.e., there exists a symmetric affine combiner $P(u,v) = a + bu + cv + duv$ such that $F(xy) + F(x/y) = P(F(x),F(y))$ for all positive $x,y$, then $F$ belongs to the RCL family: there exist a combiner $P'$ and constant $c$ with $P'(u,v) = 2u + 2v + c·uv$ and $F$ multiplicatively consistent with $P'$.
background
ComparisonOperator is the type of maps from pairs of positive reals to reals that assign a comparison cost. derivedCost extracts the one-variable function $F(r) = C(r,1)$ by fixing the second argument at the multiplicative identity, which is well-defined under scale invariance. OperativePositiveRatioComparison packages the four Aristotelian constraints together with continuity and non-triviality into a single structure hypothesis on $C$ (see DirectProof).
proof idea
The proof is a term-mode wrapper. rcases on the CountedOnceComposition hypothesis yields the combiner polynomial $P$, its four coefficients, symmetry, and the composition identity. rcl_direct_theorem is then applied to $C$, the operative hypothesis, and these extracted data, returning the RCL witness pair. The final exact packages the result into the RCLFamily constructor.
why it matters
This declaration supplies the direct link from the counted-once resource axiom to the RCL family, the algebraic core of the Recognition Composition Law. It is invoked by finite_logical_comparison_forces_rcl (which reduces finite logical comparison to the operative case) and by no_hidden_state_comparison_forces_rcl. In the broader framework it closes the step from T5 J-uniqueness and the eight-tick octave to the functional equation by enforcing single-use counting on comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.