CountedOnceCombiner
plain-language theorem explainer
A combiner P from two real inputs is counted-once precisely when it takes the bi-affine form a + b u + c v + d u v for some fixed reals a,b,c,d. Workers on the Recognition Composition Law cite this definition to establish that single-use resource comparisons yield the required algebraic structure before symmetry is imposed. The definition is an immediate existential statement with no further proof obligations.
Claim. A function $P : ℝ → ℝ → ℝ$ is a counted-once combiner if there exist real numbers $a, b, c, d$ such that $P(u, v) = a + b u + c v + d u v$ for all real $u, v$.
background
This module formalises the phrase 'each constituent comparison is counted once.' Algebraically, for two component costs u and v, this means the combiner is affine in each variable separately: a + bu + cv + duv. Identity and symmetry then force the RCL-family form. The resource-syntax and no-hidden-state bridges in sibling modules show how this algebra arises from using each comparison resource once, with no hidden route memory.
proof idea
The definition is a direct encoding of the bi-affine property. It asserts the existence of coefficients a, b, c, d that reproduce P exactly as a linear combination plus the cross term.
why it matters
This definition supplies the algebraic starting point for CountedOnceComposition, which further requires symmetry to reach the RCL form. It appears in the LinearLogicBridge as the target of expr_induces_counted_once_combiner, confirming that resource expressions without repeated counting satisfy the counted-once condition. In the Recognition framework it anchors the step from single-use comparisons to the functional equation that forces J-uniqueness at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.