SymmetricCombiner
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not impose continuity, measurability or differentiability on P.
- Does not fix the explicit coefficients of the affine form.
- Does not extend the symmetry condition to three or more arguments.
- Does not derive the RCL identity; that requires the sibling CountedOnceCombiner.
Lean usage
example (P : ℝ → ℝ → ℝ) (h : SymmetricCombiner P) : P 1 2 = P 2 1 := h 1 2formal statement (Lean)
37def SymmetricCombiner (P : ℝ → ℝ → ℝ) : Prop :=
proof body
Definition body.
38 ∀ u v, P u v = P v u
39
40/-- Counted-once composition for a comparison operator. -/