SymmetricCombiner
plain-language theorem explainer
SymmetricCombiner encodes exchange invariance for a binary real-valued combiner P. Workers deriving the RCL family from counted-once axioms cite it to enforce that the operator treats its arguments identically under swap. The definition reduces to a single universal statement P u v = P v u with no auxiliary lemmas required.
Claim. A map $P : ℝ → ℝ → ℝ$ is symmetric when $P(u,v) = P(v,u)$ holds for every pair of real numbers $u,v$.
background
The module formalizes the counted-once rule for comparison operators: given component costs $u$ and $v$, the combiner must be affine in each argument separately, taking the shape $a + b u + c v + d u v$. The module doc states that identity together with symmetry then forces the RCL-family form. This algebraic constraint arises directly from the resource-syntax requirement that each comparison is used once with no hidden route memory.
proof idea
The declaration is a direct definition. It simply unfolds to the universal quantification ∀ u v, P u v = P v u. No upstream lemmas are invoked; the body is the property itself.
why it matters
SymmetricCombiner supplies one of the two conjuncts inside CountedOnceComposition, the definition that isolates the RCL form. It therefore sits on the path from the affine counted-once combiner to the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). In the broader forcing chain the symmetry step helps isolate the unique J-cost function at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.