Encyclopedia Foundation Foundation Dalembert Entanglement Gate

ARTICLE 5 claims 5 theorems

Foundation Dalembert Entanglement Gate

A formal criterion that separates composite observations that merely add up from those that genuinely interact.

Verify this page

The entanglement gate

The entanglement gate is a formal test for whether observing a composite system is more than the sum of observing its parts. In mathematics, a function P(u, v) that combines two observations is called separable when it can be written as α(u) + β(v), meaning the two inputs contribute independently. The gate checks the opposite: whether P has a nonzero mixed second difference, a discrete analogue of the cross-derivative ∂²P/∂u∂v. When that mixed difference is nonzero, the function is said to entangle its inputs, because the effect of changing u depends on the value of v.

The classical example comes from the framework's own cost function. The additive combiner P(u, v) = 2u + 2v is separable: its mixed difference is identically zero, and the theorem Padd_separable proves this in the machine-checked library. The RCL combiner P(u, v) = 2uv + 2u + 2v is not separable: its mixed difference equals 2(u₁ − u₀)(v₁ − v₀), which is nonzero whenever both inputs change. The theorem Prcl_entangling proves this directly. The two combiners sit at opposite ends of the gate, and the theorem entanglement_gate_theorem packages the full result: the framework's cost function has the interaction property, the RCL combiner entangles, and the additive combiner does not.

The gate earns its name because it connects two apparently separate ideas. On one side, a function F that satisfies the framework's composition law, normalization F(1) = 0, and symmetry F(x) = F(x⁻¹). On the other side, the combiner P that appears in that law. The theorem interaction_implies_entangling shows that if F has the interaction property, then P must entangle. The converse, no_interaction_implies_additive, shows that without interaction, P must be the additive form 2u + 2v. A further theorem, separable_with_boundary_is_additive, pins down the additive combiner uniquely once boundary conditions P(u, 0) = 2u and P(0, v) = 2v are imposed.

In plain language, the gate says this: if the universe's ledger of recognition events is forced to interact, then the combiner that joins two observations cannot be a simple sum. It must carry the cross term 2uv. That cross term is precisely the signature of entanglement in this framework, and it is what makes the RCL combiner the unique interactive choice. The gate does not prove that interaction must occur; it proves that if interaction occurs, the combiner's form is forced.

THEOREM Padd_separable · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
Padd_separable · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean:53 
/-- 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
THEOREM Prcl_entangling · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
Prcl_entangling · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean:84 
/-- 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
THEOREM entanglement_gate_theorem · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
entanglement_gate_theorem · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean:230 
/-- **Entanglement Gate Theorem**: J has interaction, hence any consistent combiner
    for J must be entangling (not separable). The RCL combiner satisfies this. -/
theorem entanglement_gate_theorem :
    NecessityGates.HasInteraction Cost.Jcost ∧
    IsEntangling Prcl ∧
    ¬ IsEntangling Padd := by
  refine ⟨NecessityGates.Jcost_hasInteraction, Prcl_entangling, Padd_not_entangling⟩
THEOREM interaction_implies_entangling · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
interaction_implies_entangling · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean:172 
/-- If F has interaction and symmetry, then ANY consistent combiner P must be entangling. -/
theorem interaction_implies_entangling (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
    (hNorm : F 1 = 0)
    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
    (hInt : NecessityGates.HasInteraction F) :
    IsEntangling P := by
  -- Proof by contradiction: suppose P is not entangling
  by_contra hNotEnt
  simp only [IsEntangling, not_exists, not_not] at hNotEnt
  -- Then P has zero mixed difference everywhere
  obtain ⟨x, y, hx, hy, hNeq⟩ := hInt
  have hcons := hCons x y hx hy
  -- Mixed difference = 0 implies P decomposes additively
  have hMixed : ∀ u₀ v₀ u₁ v₁, P u₁ v₁ - P u₁ v₀ - P u₀ v₁ + P u₀ v₀ = 0 :=
    fun u₀ v₀ u₁ v₁ => hNotEnt u₀ v₀ u₁ v₁
  have hDecomp : ∀ u v, P u v = P u 0 + P 0 v - P 0 0 := by
    intro u v
    have := hMixed 0 0 u v
    linarith
  -- P(u, 0) = 2u from normalization
  have hBdryU : ∀ u, (∃ x', 0 < x' ∧ F x' = u) → P u 0 = 2 * u := by
    intro u ⟨x', hxpos, hFx'⟩
    have hc := hCons x' 1 hxpos one_pos
    simp only [mul_one, div_one, hNorm] at hc
    rw [← hFx']
    linarith
  -- P(0, v) = 2v from symmetry: F(1·y) + F(1/y) = P(0, F y), and F(1/y) = F(y)
  have hBdryV : ∀ v, (∃ y', 0 < y' ∧ F y' = v) → P 0 v = 2 * v := by
    intro v ⟨y', hypos, hFy'⟩
    have hc := hCons 1 y' one_pos hypos
    simp only [one_mul, one_div, hNorm] at hc
    -- hc : F y' + F y'⁻¹ = P 0 (F y')
    have hsym := hSymm y' hypos
    -- hsym : F y' = F y'⁻¹, so F y' + F y'⁻¹ = F y' + F y' = 2 * F y'
    rw [← hsym] at hc
    -- hc : F y' + F y' = P 0 (F y')
    rw [← hFy']
    linarith
  -- P(0, 0) = 0
  have hP00 : P 0 0 = 0 := by
    have := hCons 1 1 one_pos one_pos
    simp only [mul_one, div_one, hNorm] at this
    linarith
  -- On the range of F, P(u, v) = 2u + 2v
  have hPadd : P (F x) (F y) = 2 * F x + 2 * F y := by
    rw [hDecomp]
    rw [hBdryU (F x) ⟨x, hx, rfl⟩]
    rw [hBdryV (F y) ⟨y, hy, rfl⟩]
    rw [hP00]
    ring
  -- But F has interaction: F(xy) + F(x/y) ≠ 2 F x + 2 F y
  -- And consistency: F(xy) + F(x/y) = P(F x, F y) = 2 F x + 2 F y
  rw [hcons] at hNeq
  exact hNeq hPadd
THEOREM separable_with_boundary_is_additive · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
separable_with_boundary_is_additive · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean:120 
/-- 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

What this page does not claim

This page does not claim that interaction must occur in the framework, only that if it does, the combiner is forced. This page does not claim that the entanglement gate is a physical entanglement measure in the quantum information sense. This page does not claim that the RCL combiner is the only entangling combiner satisfying the composition law.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND