CountedOnceComposition
plain-language theorem explainer
Counted-once composition requires that the derived cost of a comparison operator admits a symmetric affine bilinear combiner P so the sum of costs for the product and quotient equals P applied to the separate costs. Researchers deriving the Recognition Composition Law from resource constraints cite this when connecting no-hidden-state comparisons to the RCL family. The definition directly packages an existential claim over the combiner coefficients and the functional equation with no separate proof steps.
Claim. Let $C$ be a comparison operator. Then $C$ satisfies counted-once composition if there exists $P : ℝ → ℝ → ℝ$ such that $P$ is a counted-once combiner ($P(u,v) = a + b u + c v + d u v$ for constants $a,b,c,d$), $P$ is symmetric ($P(u,v) = P(v,u)$), and for all positive reals $x,y$, derivedCost$_C(xy) +$ derivedCost$_C(x/y) = P($derivedCost$_C(x),$ derivedCost$_C(y))$.
background
The module formalizes the requirement that each constituent comparison is counted once. For two component costs $u$ and $v$ this means the combiner is affine in each variable separately, taking the form $a + b u + c v + d u v$. Identity and symmetry on this form then force the RCL-family expression. The derived cost is the specialization of the comparison operator obtained by fixing the second argument at the multiplicative identity 1, yielding a well-defined function on positive ratios under scale invariance.
proof idea
This is a definition that directly asserts the existence of a combiner $P$ satisfying the three conjuncts: it is a counted-once combiner (affine in each argument), it is symmetric, and it reproduces the composition equation for the derived cost under multiplication and division. No lemmas or tactics are invoked; the body is the existential packaging of the affine coefficients and the functional equation.
why it matters
The definition bridges no-hidden-state composition to the Recognition Composition Law. It is invoked by counted_once_combiner_forces_rcl to conclude that the derived cost lies in the RCL family, and by finite_logical_has_counted_once to equip finite logical comparisons with the property. In the Recognition Science chain it encodes the step where resource counting without hidden routes enforces the functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, feeding the phi-forcing and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.