CountedOnceComposition
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any comparison operator satisfying the property.
- Does not fix the numerical values of the affine coefficients.
- Does not extend to compositions of more than two comparisons.
- Does not incorporate the full set of Aristotelian constraints on the operator.
formal statement (Lean)
41def CountedOnceComposition (C : ComparisonOperator) : Prop :=
proof body
Definition body.
42 ∃ P : ℝ → ℝ → ℝ,
43 CountedOnceCombiner P ∧
44 SymmetricCombiner P ∧
45 (∀ x y : ℝ, 0 < x → 0 < y →
46 derivedCost C (x * y) + derivedCost C (x / y) =
47 P (derivedCost C x) (derivedCost C y))
48
49/-- Counted-once composition is a special case of finite pairwise polynomial
50closure. -/