Foundation Dalembert Entanglement Gate Separable Implies Not Entangling

The separability test

In mathematics, a function of two variables is called separable when it can be written as the sum of a function of the first variable alone plus a function of the second variable alone. For example, P(u,v) = 2u + 2v is separable because it equals α(u) + β(v) with α(u) = 2u and β(v) = 2v. A function that cannot be written this way, such as P(u,v) = 2uv + 2u + 2v, is called entangling. The name comes from the physical picture: a separable combiner merely adds what each part contributes on its own, while an entangling combiner includes a cross term, the 2uv, that couples the two inputs together.

The Recognition Science framework formalizes this distinction in its machine-checked library of formal theorems. The declaration separable_implies_not_entangling proves a basic fact: if a combiner is separable, then it cannot be entangling. The proof is algebraic. For a separable function, the mixed second difference P(u₁,v₁) − P(u₁,v₀) − P(u₀,v₁) + P(u₀,v₀) always equals zero. For an entangling function, by definition, this same expression is nonzero for some choice of points. A number cannot be both zero and nonzero, so the two properties are mutually exclusive.

The result matters because the framework's central cost function J(x) = (x + 1/x)/2 − 1 turns out to force an entangling combiner. When J satisfies its defining functional equation, the combiner P(u,v) = 2uv + 2u + 2v appears, and its cross-derivative is 2, not 0. In this account, the universe's ledger of recognition events cannot be a mere sum of separate observations; it must include the interaction term that couples them. The theorem separable_implies_not_entangling is the negative half of that picture: it rules out the additive alternative, showing that a separable combiner would contradict the framework's forced structure.

What the declaration does not claim is equally precise. It does not say that every non-separable function is physically meaningful, nor that separability is impossible in all contexts. It proves only the logical implication: separability excludes entangling, for any real-valued function of two real variables. It also does not assert that the additive combiner P(u,v) = 2u + 2v is the only separable option; the theorem applies to all separable functions, but the framework's boundary conditions later single out that specific additive form when interaction is absent.

/-- Separable implies not entangling (contrapositive of entangling implies not separable). -/
theorem separable_implies_not_entangling (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
    ¬ IsEntangling P := by
  intro ⟨u₀, v₀, u₁, v₁, h⟩
  exact h (separable_implies_zero_mixed_diff P hSep u₀ v₀ u₁ v₁)

/-- Separable implies zero mixed difference. -/
theorem separable_implies_zero_mixed_diff (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
    ∀ u₀ v₀ u₁ v₁, P u₁ v₁ - P u₁ v₀ - P u₀ v₁ + P u₀ v₀ = 0 := by
  obtain ⟨α, β, h⟩ := hSep
  intro u₀ v₀ u₁ v₁
  simp only [h]
  ring

/-- Padd is separable: P(u,v) = 2u + 2v = α(u) + β(v). -/
theorem Padd_separable : IsSeparable Padd := by
  use fun u => 2 * u, fun v => 2 * v
  intro u v
  rfl

/-- Padd is not entangling. -/
theorem Padd_not_entangling : ¬ IsEntangling Padd := by
  intro ⟨u₀, v₀, u₁, v₁, h⟩
  exact h (Padd_mixed_diff_zero u₀ v₀ u₁ v₁)

/-- Prcl is entangling. Witness: (0,0) and (1,1) give mixed diff = 2. -/
theorem Prcl_entangling : IsEntangling Prcl := by
  use 0, 0, 1, 1
  rw [Prcl_mixed_diff]
  norm_num

/-- 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 declaration does not claim that every non-separable function is physically meaningful. It does not claim that separability is impossible in all contexts, only that it excludes entangling. It does not claim that the additive combiner is the only separable function, only that it is one example.

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: