Foundation Dalembert Entanglement Gate Separable With Boundary Is Additive

The boundary forces the sum

In mathematics, a function of two variables is called separable when it can be written as a sum of two single-variable functions: P(u,v) = α(u) + β(v). The Recognition Science declaration separable_with_boundary_is_additive proves a sharp consequence: if such a separable function also satisfies two boundary conditions, P(u,0) = 2u and P(0,v) = 2v, then it must be exactly P(u,v) = 2u + 2v. The proof is a short algebraic identity: substitute the separable form into the boundary conditions, solve for α and β, and the sum falls out. No calculus, no continuity assumptions, just the structure of separability plus the boundary pins the whole function down.

The theorem lives in a module about the entanglement gate, a term the framework uses for a combiner that couples two inputs rather than merely adding them. The additive combiner Padd(u,v) = 2u + 2v has zero mixed second difference, meaning changes in u and v act independently. The rival combiner Prcl(u,v) = 2uv + 2u + 2v has a nonzero mixed difference, the 2uv term, which the framework interprets as interaction: observing a composite is not just the sum of observing its parts. The theorem's role is to show that if you demand separability and fix the boundary behavior, the additive form is the only option; the interaction term cannot sneak in under those constraints.

In Recognition Science, this is a load-bearing step in a larger argument. The framework derives its cost function J(x) = (x + 1/x)/2 - 1 from five forced conditions, and the combiner P appears when composing costs. The theorem separable_with_boundary_is_additive is what closes off the separable branch: given the boundary conditions that the framework's axioms impose, a separable combiner cannot be anything but additive. The entangling alternative, Prcl, is what the framework's actual cost function uses, and it is provably not separable. So the theorem does not say interaction is impossible; it says interaction requires giving up separability, which the framework's axioms do elsewhere.

What the theorem does not claim is broader than what it proves. It does not assert that every separable function with those boundaries is physically meaningful, nor that the additive combiner is the one the framework ultimately uses. It does not say anything about quantum entanglement, a different concept that shares the name. The theorem is purely about real-valued functions of two real variables: a conditional statement, if separable and boundary-matched, then additive. The framework's larger claims about why interaction is necessary come from other theorems, not from this one.

/-- If P is separable AND satisfies both boundary conditions,
    then P must be the additive combiner 2u + 2v. -/
theorem separable_with_boundary_is_additive (P : ℝ → ℝ → ℝ)
    (hSep : IsSeparable P)
    (hBdryU : ∀ u, P u 0 = 2 * u)
    (hBdryV : ∀ v, P 0 v = 2 * v) :
    ∀ u v, P u v = 2 * u + 2 * v := by
  obtain ⟨α, β, hαβ⟩ := hSep
  -- From hBdryU: α(u) + β(0) = 2u, so α(u) = 2u - β(0)
  have hα : ∀ u, α u = 2 * u - β 0 := by
    intro u
    have := hBdryU u
    rw [hαβ] at this
    linarith
  -- From hBdryV: α(0) + β(v) = 2v, so β(v) = 2v - α(0)
  have hβ : ∀ v, β v = 2 * v - α 0 := by
    intro v
    have := hBdryV v
    rw [hαβ] at this
    linarith
  -- From hα at u=0: α(0) = -β(0)
  have hα0 : α 0 = -β 0 := by
    have := hα 0
    simp at this
    exact this
  intro u v
  rw [hαβ]
  -- Goal: α u + β v = 2 * u + 2 * v
  have hαu := hα u
  have hβv := hβ v
  rw [hαu, hβv, hα0]
  ring

/-- The mixed second difference of Padd is zero. -/
theorem Padd_mixed_diff_zero : ∀ u₀ v₀ u₁ v₁ : ℝ,
    Padd u₁ v₁ - Padd u₁ v₀ - Padd u₀ v₁ + Padd u₀ v₀ = 0 := by
  intro u₀ v₀ u₁ v₁
  simp only [Padd]
  ring

/-- The mixed second difference of Prcl equals 2(u₁-u₀)(v₁-v₀).
    In particular, it's nonzero when u₁ ≠ u₀ and v₁ ≠ v₀. -/
theorem Prcl_mixed_diff : ∀ u₀ v₀ u₁ v₁ : ℝ,
    Prcl u₁ v₁ - Prcl u₁ v₀ - Prcl u₀ v₁ + Prcl u₀ v₀ = 2 * (u₁ - u₀) * (v₁ - v₀) := by
  intro u₀ v₀ u₁ v₁
  simp only [Prcl]
  ring

/-- Prcl is NOT separable. -/
theorem Prcl_not_separable : ¬ IsSeparable Prcl := by
  intro ⟨α, β, h⟩
  -- If Prcl(u,v) = α(u) + β(v), then the mixed second difference is 0
  have hsep : Prcl 1 1 - Prcl 1 0 - Prcl 0 1 + Prcl 0 0 = 0 := by
    calc Prcl 1 1 - Prcl 1 0 - Prcl 0 1 + Prcl 0 0
        = (α 1 + β 1) - (α 1 + β 0) - (α 0 + β 1) + (α 0 + β 0) := by
          simp only [h 1 1, h 1 0, h 0 1, h 0 0]
      _ = 0 := by ring
  rw [Prcl_mixed_diff] at hsep
  norm_num at hsep

What this page does not claim

The theorem says nothing about quantum entanglement, a physical phenomenon with a different definition. It does not assert that the additive combiner is the one the framework uses; the framework's actual combiner is the entangling Prcl. It does not prove that interaction is impossible, only that separability plus these boundaries rules it out.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: