CountedOnceComposition
plain-language theorem explainer
Counted-once composition for a comparison operator C requires existence of an affine symmetric combiner P such that derived costs satisfy the product-quotient identity. Researchers deriving the Recognition Composition Law from resource constraints cite this definition when linking no-hidden-state or finite-logical comparisons to the RCL family. The definition directly packages the bilinear form together with symmetry and the matching equation.
Claim. For a comparison operator $C$, counted-once composition holds when there exists $P : ℝ → ℝ → ℝ$ that is affine in each argument separately, symmetric under argument exchange, and satisfies derivedCost$(C)(xy) +$ derivedCost$(C)(x/y) = P($derivedCost$(C)(x),$ derivedCost$(C)(y))$ for all positive reals $x,y$.
background
ComparisonOperator is the abbreviation for maps ℝ → ℝ → ℝ that assign a real cost to comparing two positive quantities, subject to the four Aristotelian constraints. derivedCost extracts the unary cost function on positive ratios by fixing the second argument at 1. CountedOnceCombiner asserts that any such combiner P takes the explicit bilinear form a + b u + c v + d u v. SymmetricCombiner requires invariance under exchange of arguments. The module formalises the phrase 'each constituent comparison is counted once' so that identity and symmetry force the RCL-family form, as developed from the resource-syntax and no-hidden-state bridges in sibling modules.
proof idea
This is a definition. It directly asserts the existential claim over a counted-once combiner P that is also symmetric and satisfies the composition identity on derivedCost C.
why it matters
CountedOnceComposition supplies the algebraic interface used by counted_once_combiner_forces_rcl to derive RCLFamily(derivedCost C) from operative positive-ratio comparisons. It is invoked by finite_logical_has_counted_once and no_hidden_state_implies_counted_once. In the Recognition Science chain this isolates the step converting the counted-once resource rule into the functional equation J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.