no_interaction_implies_additive
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume differentiability of P or F.
- Does not address the case in which F has interaction.
- Does not derive the explicit form of the RCL combiner.
- Does not quantify over all possible images of F.
formal statement (Lean)
155theorem no_interaction_implies_additive (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
156 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
157 (hNorm : F 1 = 0)
158 (hNoInt : ¬ NecessityGates.HasInteraction F) :
159 ∀ u v : ℝ, (∃ x y, 0 < x ∧ 0 < y ∧ F x = u ∧ F y = v) →
160 P u v = 2 * u + 2 * v := by
proof body
Term-mode proof.
161 intro u v ⟨x, y, hx, hy, hFx, hFy⟩
162 -- hNoInt says: ∀ x y, 0 < x → 0 < y → F(xy) + F(x/y) = 2 F x + 2 F y
163 simp only [NecessityGates.HasInteraction, not_exists, not_and, not_not] at hNoInt
164 have hAdd := hNoInt x y hx hy
165 rw [hCons x y hx hy] at hAdd
166 -- hAdd : P (F x) (F y) = 2 * F x + 2 * F y
167 rw [← hFx, ← hFy]
168 exact hAdd
169
170/-! ## Main Theorem: Entanglement is Necessary for RCL -/
171
172/-- If F has interaction and symmetry, then ANY consistent combiner P must be entangling. -/