no_interaction_implies_additive
plain-language theorem explainer
If a cost function F obeys the consistency equation F(xy) + F(x/y) = P(F(x), F(y)) for positive x, y together with F(1) = 0, but satisfies the no-interaction condition that F(xy) + F(x/y) always equals 2F(x) + 2F(y), then the combiner P must act additively on the image of F. Researchers separating the additive case from the Recognition Composition Law would cite this result. The proof is a one-line term-mode substitution that unfolds the negation of HasInteraction and replaces the left-hand side via the consistency hypothesis.
Claim. Let $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$ satisfy $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$ with $F(1) = 0$. If $F$ has no interaction, i.e., $F(xy) + F(x/y) = 2F(x) + 2F(y)$ holds identically for $x,y > 0$, then for any $u,v$ in the image of $F$ we have $P(u,v) = 2u + 2v$.
background
The module formalizes the Entanglement Gate as the requirement that the combiner P has nonzero cross-derivative ∂²P/∂u∂v. The additive combiner is defined by P(u,v) = 2u + 2v (zero cross term) while the RCL combiner is P(u,v) = 2uv + 2u + 2v (cross term equal to 2). HasInteraction F is the predicate that there exist x,y > 0 such that F(xy) + F(x/y) ≠ 2F(x) + 2F(y); its negation is therefore the statement that the equality with 2F(x) + 2F(y) holds for every positive pair. The local setting is the cross-derivative characterization of entanglement: observing a composite system xy is not merely the sum of observing x and y separately.
proof idea
The term proof proceeds by introducing u and v together with witnesses x,y > 0 such that F(x) = u and F(y) = v. It then rewrites the hypothesis ¬HasInteraction F into the universal statement that F(xy) + F(x/y) = 2F(x) + 2F(y) for all positive arguments. Substituting the consistency hypothesis replaces the left-hand side by P(F(x), F(y)), yielding P(u,v) = 2u + 2v after the final rewrites.
why it matters
This theorem supplies the contrapositive half of the claim that entanglement is necessary for the Recognition Composition Law: the additive combiner is forced precisely when interaction is absent. It sits immediately before the main result that any consistent combiner must be entangling once HasInteraction holds. The result closes the additive branch of the gate and thereby isolates the 2uv term required by the RCL in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.