SeparatelyAdditive
plain-language theorem explainer
A combiner P of two real arguments is separately additive when it decomposes exactly as the sum of a univariate function of the first argument and a univariate function of the second. Researchers formalizing the Recognition Science branch selection cite this definition to isolate the additive case (c = 0) inside the RCL polynomial family and thereby exclude it in favor of the bilinear branch. The definition is a direct existential quantification over the component functions p and q.
Claim. A combiner $P : ℝ → ℝ → ℝ$ is separately additive when there exist functions $p, q : ℝ → ℝ$ such that $P(u, v) = p(u) + q(v)$ for all real $u, v$.
background
The Branch Selection module works inside the family of combiners produced by the translation theorem of Logic_FE, namely the RCL family $P(u, v) = 2u + 2v + c·u·v$ for $c ∈ ℝ$. The additive branch of this family arises precisely when $c = 0$ and is represented by the quadratic form $½(ln x)²$; the bilinear branch arises when $c ≠ 0$ and is represented by $J(x) = ½(x + x^{-1}) - 1$. The module introduces the structural distinction that a genuine composition law must employ a coupling combiner, i.e., one that is not separately additive in its arguments.
proof idea
This is a direct definition. It encodes the additive decomposition by an existential quantifier over univariate functions p and q, with the equality $P u v = p u + q v$ required for every pair of arguments.
why it matters
The definition supplies the negative clause in the BranchSelectionCert structure, which states that a coupling combiner (¬SeparatelyAdditive P) forces the bilinear branch inside the RCL family. It is used to prove the equivalence SeparatelyAdditive P ↔ interactionDefect P ≡ 0 and to establish that the RCL combiner with c = 0 is separately additive while c ≠ 0 yields a coupling combiner. Together with the translation theorem this isolates the J-form modulo the residual α-coordinate freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.