theorem
proved
interaction_implies_entangling
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.DAlembert.EntanglementGate on GitHub at line 173.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
Gate -
consistent -
has -
mul_one -
one_mul -
IsEntangling -
of -
HasInteraction -
is -
of -
from -
is -
of -
for -
is -
of -
is -
and -
F -
F -
F
used by
formal source
170/-! ## Main Theorem: Entanglement is Necessary for RCL -/
171
172/-- If F has interaction and symmetry, then ANY consistent combiner P must be entangling. -/
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
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