CountedOnceComposition
plain-language theorem explainer
The definition requires that a comparison operator's cost function composes under multiplication and division via a symmetric affine combiner that counts each input once. Researchers deriving the Recognition Composition Law from resource-use constraints cite this when linking no-hidden-state assumptions to the functional equation. It is introduced directly as an existential claim over an affine symmetric P that reproduces the composition identity on derived costs.
Claim. Let $C$ be a comparison operator. Then $C$ satisfies counted-once composition if there exists a map $P:ℝ→ℝ→ℝ$ that is affine in each argument separately, symmetric under argument exchange, and obeys cost$_C(xy)+$cost$_C(x/y)=P($cost$_C(x),$cost$_C(y))$ for all positive reals $x,y$, where cost$_C(r):=C(r,1)$.
background
The module formalizes the requirement that each constituent comparison is counted once. For component costs $u$ and $v$ the combiner must therefore be affine in each variable: $a + b u + c v + d u v$. The module documentation states that identity and symmetry then force the RCL-family form, and that this algebra arises from using each comparison resource once with no hidden route memory.
proof idea
This is a definition. It directly packages the three conjuncts: existence of an affine combiner (from the sibling CountedOnceCombiner), symmetry of that combiner, and exact reproduction of the multiplicative composition identity on the cost function obtained by fixing the second argument at one.
why it matters
The definition is invoked by the theorem that counted-once composition forces the RCL family under operative comparison, by the result that finite logical comparison carries counted-once composition, and by the bridge from no-hidden-state composition. It supplies the algebraic step that converts the resource-counting constraint into the Recognition Composition Law inside the LogicAsFunctionalEquation development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.