RCLCombiner_zero_separatelyAdditive
plain-language theorem explainer
The theorem shows that the RCL combiner at parameter zero is separately additive, decomposing as P(u,v)=2u+2v with linear witnesses p(u)=2u and q(v)=2v. Branch selection arguments cite it to identify the additive case before the coupling requirement excludes it. The proof is a direct term construction that exhibits the witnesses and confirms the identity by unfolding the combiner and applying ring simplification.
Claim. The combiner defined by $P(u,v)=2u+2v$ is separately additive: there exist functions $p,q:ℝ→ℝ$ such that $P(u,v)=p(u)+q(v)$ for all real $u,v$. This holds with the explicit choice $p(u)=2u$ and $q(v)=2v$.
background
The Branch Selection module starts from the Recognition Composition Law family $F(xy)+F(x/y)=2F(x)+2F(y)+c F(x)F(y)$, which produces the polynomial combiner $P(u,v)=2u+2v+c·u·v$. SeparatelyAdditive is the property that $P$ factors as independent single-argument maps, the structural form excluded from genuine composition consistency. RCLCombiner at $c=0$ collapses exactly to the additive case $2u+2v$ (see its definition in the same module).
proof idea
The proof is a term-mode construction. It refines the existential in SeparatelyAdditive by supplying the concrete witnesses $p(u)=2u$ and $q(v)=2v$. After introducing $u$ and $v$, it unfolds RCLCombiner and applies the ring tactic to obtain the required equality.
why it matters
This lemma isolates the additive branch ($c=0$) of the RCL combiner, which the module contrasts with the bilinear branch to enforce the coupling-combiner condition in the strengthened (L4*). It directly supports the characterization RCLCombiner_isCoupling_iff and the overall branch_selection result that forces the $J$ representative. In the Recognition framework it closes the $c=0$ case before the forcing chain selects $D=3$ and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.