Encyclopedia Foundation Foundation Dalembert Entanglement Gate No Interaction Implies Additive

ARTICLE 3 claims 3 theorems

Foundation Dalembert Entanglement Gate No Interaction Implies Additive

If observing a pair of objects is just the sum of observing each alone, the framework proves the combiner must be plain addition.

Verify this page

When combination is only addition

In the Recognition Science framework, a ledger, a discrete record of events, assigns a cost to each observation. The framework asks how the cost of observing a composite system relates to the costs of observing its parts. The answer it proves is stark: if the composite cost is exactly the sum of the part costs, with no extra coupling term, then the combiner is forced to be the additive rule P(u, v) = 2u + 2v. This is the content of the theorem no_interaction_implies_additive, a machine-checked result in the framework's library of formal theorems.

The theorem works from a functional equation, the same one that governs the framework's cost function. For positive x and y, the equation F(xy) + F(x/y) = P(F x)(F y) links the cost of a product and a quotient to a combiner P applied to the individual costs. The theorem assumes F is normalized so F(1) = 0 and that F has no interaction, meaning its mixed second difference vanishes. Under those conditions, whenever u and v are actual costs of some observations, the combiner must equal 2u + 2v. The proof is a short algebraic argument: separability, the property that P splits as a sum of a function of u and a function of v, together with the boundary conditions P(u, 0) = 2u and P(0, v) = 2v, pins down the additive form exactly.

The theorem is a classification result. It shows that the additive combiner is the unique option in the no-interaction regime. Its counterpart, interaction_implies_entangling, shows that if F does have interaction, then P must be entangling, meaning its mixed second difference is nonzero somewhere. The two results together draw a clean line: no interaction forces additivity; interaction forces entanglement. The framework's own cost function, J(x) = (x + 1/x)/2 - 1, falls on the interaction side, with the combiner P(u, v) = 2uv + 2u + 2v whose cross term 2uv is the signature of coupling.

What the theorem does not claim is broader. It does not say that every additive combiner describes a physical system, nor that the no-interaction regime is the one nature uses. It is a conditional statement about the framework's own definitions, not an empirical law. The theorem also requires that u and v lie in the range of F, so it does not apply to arbitrary real inputs. And it does not assert that the additive combiner is the only separable one; it proves that under the boundary conditions, the additive form is the only one that survives.

THEOREM no_interaction_implies_additive · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean
no_interaction_implies_additive · IndisputableMonolith/Foundation/DAlembert/EntanglementGate.lean:153 
/-- If F has no interaction and P satisfies boundary conditions,
    then P is the additive combiner. -/
theorem no_interaction_implies_additive (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
    (hNorm : F 1 = 0)
    (hNoInt : ¬ NecessityGates.HasInteraction F) :
    ∀ u v : ℝ, (∃ x y, 0 < x ∧ 0 < y ∧ F x = u ∧ F y = v) →
      P u v = 2 * u + 2 * v := by
  intro u v ⟨x, y, hx, hy, hFx, hFy⟩
  -- hNoInt says: ∀ x y, 0 < x → 0 < y → F(xy) + F(x/y) = 2 F x + 2 F y
  simp only [NecessityGates.HasInteraction, not_exists, not_and, not_not] at hNoInt
  have hAdd := hNoInt x y hx hy
  rw [hCons x y hx hy] at hAdd
  -- hAdd : P (F x) (F y) = 2 * F x + 2 * F y
  rw [← hFx, ← hFy]
  exact hAdd
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
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

What this page does not claim

The theorem does not assert that the additive combiner is the one nature uses. The theorem does not apply to arbitrary real inputs u and v, only to values that lie in the range of F. The theorem does not prove that the additive combiner is the only separable one without the boundary conditions.

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