theorem
proved
tactic proof
interaction_implies_entangling
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
204 -- hc : F y' + F y'⁻¹ = P 0 (F y')
205 have hsym := hSymm y' hypos
206 -- hsym : F y' = F y'⁻¹, so F y' + F y'⁻¹ = F y' + F y' = 2 * F y'
207 rw [← hsym] at hc
208 -- hc : F y' + F y' = P 0 (F y')
209 rw [← hFy']
210 linarith
211 -- P(0, 0) = 0
212 have hP00 : P 0 0 = 0 := by
213 have := hCons 1 1 one_pos one_pos
214 simp only [mul_one, div_one, hNorm] at this
215 linarith
216 -- On the range of F, P(u, v) = 2u + 2v
217 have hPadd : P (F x) (F y) = 2 * F x + 2 * F y := by
218 rw [hDecomp]
219 rw [hBdryU (F x) ⟨x, hx, rfl⟩]
220 rw [hBdryV (F y) ⟨y, hy, rfl⟩]
221 rw [hP00]
222 ring
223 -- But F has interaction: F(xy) + F(x/y) ≠ 2 F x + 2 F y
224 -- And consistency: F(xy) + F(x/y) = P(F x, F y) = 2 F x + 2 F y
225 rw [hcons] at hNeq
226 exact hNeq hPadd
227
228/-! ## The Gate Theorem -/
229
230/-- **Entanglement Gate Theorem**: J has interaction, hence any consistent combiner
231 for J must be entangling (not separable). The RCL combiner satisfies this. -/