interaction_implies_entangling
If F satisfies the d'Alembert consistency relation with a combiner P, plus F(1)=0 and inversion symmetry, and F exhibits interaction on some positive pair, then P cannot be separable. Researchers tracing the Recognition Science forcing chain cite this to rule out additive combiners before deriving the hyperbolic ODE for the cost function. The proof proceeds by contradiction: non-entangling forces an additive decomposition of P on the image of F, which collides with the interaction witness via the consistency equation.
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$ and $F(x) = F(x^{-1})$ for $x > 0$. Suppose $F$ has interaction, i.e., there exist $x,y > 0$ such that $F(xy) + F(x/y) ≠ 2F(x) + 2F(y)$. Then $P$ is entangling: there exist $u_0,v_0,u_1,v_1$ with $P(u_1,v_1) - P(u_1,v_0) - P(u_0,v_1) + P(u_0,v_0) ≠ 0$.
background
The Entanglement Gate module isolates the cross-derivative requirement on any combiner P that respects the functional equation for F. IsEntangling P means the mixed second difference is nonzero somewhere, equivalently (under smoothness) a nonzero ∂²P/∂u∂v. The module contrasts the separable case P(u,v) = 2u + 2v (zero cross term) with the RCL case P(u,v) = 2uv + 2u + 2v (cross term 2), noting that entanglement encodes the coupling between composite and separate observations.
proof idea
Proof by contradiction. Assume ¬IsEntangling P, so the mixed difference vanishes identically. This yields the additive decomposition P(u,v) = P(u,0) + P(0,v) - P(0,0). Boundary evaluations via the consistency relation at y=1 (using mul_one, one_mul) and symmetry give P(u,0) = 2u and P(0,v) = 2v on the image of F, with P(0,0)=0. Hence P(Fx,Fy) = 2Fx + 2Fy. The interaction witness then supplies x,y where the left side of consistency differs from 2Fx + 2Fy, a direct contradiction.
why it matters in Recognition Science
This result supplies the first link in the chain that forces F to Jcost: interaction implies entangling P (this theorem), entangling forces the hyperbolic ODE, and the ODE plus initial conditions recover J. It is invoked by F_forced_to_Jcost and Jcost_satisfies_dAlembert in AnalyticBridge, and by interaction_forces_entanglement in TriangulatedProof. Within the framework it closes the step from T5 (J-uniqueness) to the RCL combiner before the eight-tick octave and D=3 emerge.
scope and limits
- Does not prove uniqueness of the combiner P.
- Does not assume differentiability of F or P.
- Does not extend to arguments ≤0 or to multi-argument combiners.
- Does not derive the explicit 2uv form of P.
- Does not address stability under perturbations of the interaction witness.
Lean usage
example (F P hCons hNorm hSymm hInt) : IsEntangling P := interaction_implies_entangling F P hCons hNorm hSymm hIntformal statement (Lean)
173theorem interaction_implies_entangling (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
174 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
175 (hNorm : F 1 = 0)
176 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
177 (hInt : NecessityGates.HasInteraction F) :
178 IsEntangling P := by
proof body
Tactic-mode proof.
179 -- Proof by contradiction: suppose P is not entangling
180 by_contra hNotEnt
181 simp only [IsEntangling, not_exists, not_not] at hNotEnt
182 -- Then P has zero mixed difference everywhere
183 obtain ⟨x, y, hx, hy, hNeq⟩ := hInt
184 have hcons := hCons x y hx hy
185 -- Mixed difference = 0 implies P decomposes additively
186 have hMixed : ∀ u₀ v₀ u₁ v₁, P u₁ v₁ - P u₁ v₀ - P u₀ v₁ + P u₀ v₀ = 0 :=
187 fun u₀ v₀ u₁ v₁ => hNotEnt u₀ v₀ u₁ v₁
188 have hDecomp : ∀ u v, P u v = P u 0 + P 0 v - P 0 0 := by
189 intro u v
190 have := hMixed 0 0 u v
191 linarith
192 -- P(u, 0) = 2u from normalization
193 have hBdryU : ∀ u, (∃ x', 0 < x' ∧ F x' = u) → P u 0 = 2 * u := by
194 intro u ⟨x', hxpos, hFx'⟩
195 have hc := hCons x' 1 hxpos one_pos
196 simp only [mul_one, div_one, hNorm] at hc
197 rw [← hFx']
198 linarith
199 -- P(0, v) = 2v from symmetry: F(1·y) + F(1/y) = P(0, F y), and F(1/y) = F(y)
200 have hBdryV : ∀ v, (∃ y', 0 < y' ∧ F y' = v) → P 0 v = 2 * v := by
201 intro v ⟨y', hypos, hFy'⟩
202 have hc := hCons 1 y' one_pos hypos
203 simp only [one_mul, one_div, hNorm] at hc
204 -- hc : F y' + F y'⁻¹ = P 0 (F y')
205 have hsym := hSymm y' hypos
206 -- hsym : F y' = F y'⁻¹, so F y' + F y'⁻¹ = F y' + F y' = 2 * F y'
207 rw [← hsym] at hc
208 -- hc : F y' + F y' = P 0 (F y')
209 rw [← hFy']
210 linarith
211 -- P(0, 0) = 0
212 have hP00 : P 0 0 = 0 := by
213 have := hCons 1 1 one_pos one_pos
214 simp only [mul_one, div_one, hNorm] at this
215 linarith
216 -- On the range of F, P(u, v) = 2u + 2v
217 have hPadd : P (F x) (F y) = 2 * F x + 2 * F y := by
218 rw [hDecomp]
219 rw [hBdryU (F x) ⟨x, hx, rfl⟩]
220 rw [hBdryV (F y) ⟨y, hy, rfl⟩]
221 rw [hP00]
222 ring
223 -- But F has interaction: F(xy) + F(x/y) ≠ 2 F x + 2 F y
224 -- And consistency: F(xy) + F(x/y) = P(F x, F y) = 2 F x + 2 F y
225 rw [hcons] at hNeq
226 exact hNeq hPadd
227
228/-! ## The Gate Theorem -/
229
230/-- **Entanglement Gate Theorem**: J has interaction, hence any consistent combiner
231 for J must be entangling (not separable). The RCL combiner satisfies this. -/