IndisputableMonolith.Gravity.QuantumChannel.BMVPositive
IndisputableMonolith/Gravity/QuantumChannel/BMVPositive.lean · 366 lines · 13 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.LedgerSuperposition
3
4/-!
5# Gravity IV: BMV-Positive Sign (Theorem 3)
6
7This module formalizes the third load-bearing theorem of *Gravity from
8Recognition IV: The Quantum Channel*: in the BMV two-mass two-branch
9protocol, the linear cost-gradient channel of
10`Gravity.LedgerSuperposition` produces a branch-dependent gravitational
11phase whose entangling combination `Δφ` is generically nonzero, yielding
12a non-product joint state and (equivalently, for pure two-qubit states)
13strictly positive entanglement entropy outside a discrete set of revival
14times.
15
16We package the algebraic content of T3 explicitly. The two test masses
17each have a Left/Right branch index, giving four definite branch states
18`{LL, LR, RL, RR}`. After the gravitational interaction, the joint state
19acquires a per-branch phase `φ_ab`, and the joint state is a product
20state if and only if the entangling combination
21`Δφ = φ_LL + φ_RR - φ_LR - φ_RL` is congruent to `0 mod 2π` (equivalently,
22the `2×2` amplitude matrix has determinant zero). For non-degenerate BMV
23geometry, `Δφ ≠ 0 mod 2π` for every `T ∈ (0, T_rev)`, so the joint
24amplitude matrix has nonzero determinant and the joint state is
25entangled.
26
27## What is proved here
28
29* `branchAmplitudeMatrix`, `branchPhaseInvariant`: explicit definitions.
30* `det_branchAmplitude` : the `2×2` determinant of the branch amplitude
31 matrix is `(1/4) (e^{-i(φ_LL+φ_RR)} - e^{-i(φ_LR+φ_RL)})`.
32* `det_nonzero_iff_branchPhase_nonzero` : the determinant is zero if and
33 only if the entangling combination is `0 mod 2π`.
34* `entangled_of_branchPhaseNonzero` : the algebraic entanglement
35 witness — the joint state is non-product whenever `Δφ ≠ 0 mod 2π`.
36* `branchPhase_weakField` : in the weak-field regime the entangling
37 invariant is `(G m₁ m₂ T / ℏ) · (1/r_LL + 1/r_RR − 1/r_LR − 1/r_RL)`.
38-/
39
40namespace IndisputableMonolith
41namespace Gravity
42namespace QuantumChannel
43namespace BMVPositive
44
45open Complex
46
47noncomputable section
48
49/-! ## The BMV branch-amplitude matrix -/
50
51/-- The `2×2` complex amplitude matrix of the post-interaction joint
52state in the BMV protocol. The four entries are the per-branch
53phase factors `e^{-i φ_ab}` for `(a, b) ∈ {LL, LR, RL, RR}`,
54multiplied by the prefactor `1/2` from the initial product
55`((|L⟩ + |R⟩)/√2) ⊗ ((|L⟩ + |R⟩)/√2)`. -/
56def branchAmplitudeMatrix
57 (φ_LL φ_LR φ_RL φ_RR : ℝ) : Matrix (Fin 2) (Fin 2) ℂ :=
58 fun i j =>
59 (1 / 2 : ℂ) *
60 Complex.exp
61 (-Complex.I *
62 (match i, j with
63 | 0, 0 => (φ_LL : ℂ)
64 | 0, 1 => (φ_LR : ℂ)
65 | 1, 0 => (φ_RL : ℂ)
66 | 1, 1 => (φ_RR : ℂ)))
67
68/-- The entangling invariant `Δφ = φ_LL + φ_RR − φ_LR − φ_RL`. -/
69def branchPhaseInvariant (φ_LL φ_LR φ_RL φ_RR : ℝ) : ℝ :=
70 φ_LL + φ_RR - φ_LR - φ_RL
71
72/-! ## The determinant of the branch amplitude matrix -/
73
74/-- The determinant of the `2×2` BMV amplitude matrix is
75`(1/4)·(e^{-i(φ_LL+φ_RR)} − e^{-i(φ_LR+φ_RL)})`. -/
76theorem det_branchAmplitude (φ_LL φ_LR φ_RL φ_RR : ℝ) :
77 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR)
78 = (1 / 4 : ℂ) *
79 (Complex.exp (-Complex.I * ((φ_LL : ℂ) + (φ_RR : ℂ))) -
80 Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ)))) := by
81 unfold branchAmplitudeMatrix
82 rw [Matrix.det_fin_two]
83 simp only []
84 -- det = M(0,0) M(1,1) − M(0,1) M(1,0)
85 -- = (1/2 e^{-i φ_LL})(1/2 e^{-i φ_RR}) − (1/2 e^{-i φ_LR})(1/2 e^{-i φ_RL})
86 -- = (1/4) (e^{-i (φ_LL+φ_RR)} − e^{-i (φ_LR+φ_RL)})
87 have h00 : (-Complex.I) * (φ_LL : ℂ) + -Complex.I * (φ_RR : ℂ)
88 = -Complex.I * ((φ_LL : ℂ) + (φ_RR : ℂ)) := by ring
89 have h01 : (-Complex.I) * (φ_LR : ℂ) + -Complex.I * (φ_RL : ℂ)
90 = -Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ)) := by ring
91 rw [show (((1:ℂ) / 2) * Complex.exp (-Complex.I * (φ_LL : ℂ))) *
92 (((1:ℂ) / 2) * Complex.exp (-Complex.I * (φ_RR : ℂ)))
93 = ((1:ℂ) / 4) *
94 (Complex.exp (-Complex.I * (φ_LL : ℂ)) *
95 Complex.exp (-Complex.I * (φ_RR : ℂ))) by ring,
96 show (((1:ℂ) / 2) * Complex.exp (-Complex.I * (φ_LR : ℂ))) *
97 (((1:ℂ) / 2) * Complex.exp (-Complex.I * (φ_RL : ℂ)))
98 = ((1:ℂ) / 4) *
99 (Complex.exp (-Complex.I * (φ_LR : ℂ)) *
100 Complex.exp (-Complex.I * (φ_RL : ℂ))) by ring,
101 ← Complex.exp_add, ← Complex.exp_add, h00, h01]
102 ring
103
104/-! ## When is the determinant zero?
105
106The complex exponential `e^{-i x}` is invariant under translations of
107`x` by `2π`, so the BMV amplitude matrix has zero determinant iff
108`(φ_LL + φ_RR) − (φ_LR + φ_RL) ≡ 0 mod 2π`.
109
110We give the algebraic content directly: the determinant equals
111`(1/4) e^{-i (φ_LR+φ_RL)} (e^{-i Δφ} − 1)`, so it is zero iff
112`e^{-i Δφ} = 1`, iff `Δφ ∈ 2π ℤ`.
113-/
114
115/-- The branch determinant factored through the entangling invariant
116`Δφ`. -/
117theorem det_branchAmplitude_factored
118 (φ_LL φ_LR φ_RL φ_RR : ℝ) :
119 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR)
120 = (1 / 4 : ℂ) *
121 Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) *
122 (Complex.exp
123 (-Complex.I * (branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR : ℂ))
124 - 1) := by
125 rw [det_branchAmplitude]
126 unfold branchPhaseInvariant
127 -- e^{-i (φ_LL + φ_RR)} − e^{-i (φ_LR + φ_RL)}
128 -- = e^{-i (φ_LR + φ_RL)} · (e^{-i ((φ_LL + φ_RR) − (φ_LR + φ_RL))} − 1)
129 have hpush :
130 Complex.exp (-Complex.I * ((φ_LL : ℂ) + (φ_RR : ℂ)))
131 - Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ)))
132 = Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) *
133 (Complex.exp
134 (-Complex.I *
135 (((φ_LL : ℂ) + (φ_RR : ℂ)) -
136 ((φ_LR : ℂ) + (φ_RL : ℂ)))) - 1) := by
137 have hsum :
138 -Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))
139 + (-Complex.I *
140 (((φ_LL : ℂ) + (φ_RR : ℂ)) -
141 ((φ_LR : ℂ) + (φ_RL : ℂ))))
142 = -Complex.I * ((φ_LL : ℂ) + (φ_RR : ℂ)) := by ring
143 calc
144 Complex.exp (-Complex.I * ((φ_LL : ℂ) + (φ_RR : ℂ)))
145 - Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ)))
146 = Complex.exp
147 (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))
148 + (-Complex.I *
149 (((φ_LL : ℂ) + (φ_RR : ℂ)) -
150 ((φ_LR : ℂ) + (φ_RL : ℂ)))))
151 - Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) := by
152 rw [hsum]
153 _ = Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) *
154 Complex.exp
155 (-Complex.I *
156 (((φ_LL : ℂ) + (φ_RR : ℂ)) -
157 ((φ_LR : ℂ) + (φ_RL : ℂ))))
158 - Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) := by
159 rw [Complex.exp_add]
160 _ = Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) *
161 (Complex.exp
162 (-Complex.I *
163 (((φ_LL : ℂ) + (φ_RR : ℂ)) -
164 ((φ_LR : ℂ) + (φ_RL : ℂ)))) - 1) := by ring
165 have hcast :
166 ((φ_LL + φ_RR - φ_LR - φ_RL : ℝ) : ℂ)
167 = ((φ_LL : ℂ) + (φ_RR : ℂ)) - ((φ_LR : ℂ) + (φ_RL : ℂ)) := by
168 push_cast
169 ring
170 rw [hpush, hcast]
171 ring
172
173/-- The branch amplitude determinant is nonzero iff the entangling
174invariant `Δφ` is not in `2π ℤ`. -/
175theorem det_ne_zero_iff_branchPhase_ne_zero
176 (φ_LL φ_LR φ_RL φ_RR : ℝ) :
177 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR) ≠ 0
178 ↔ Complex.exp
179 (-Complex.I * (branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR : ℂ)) ≠ 1 := by
180 rw [det_branchAmplitude_factored]
181 have h14 : ((1 : ℂ) / 4) ≠ 0 := by norm_num
182 have hexp_pos : Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) ≠ 0 :=
183 Complex.exp_ne_zero _
184 constructor
185 · intro hdet hphase
186 apply hdet
187 rw [show
188 Complex.exp
189 (-Complex.I * (branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR : ℂ)) - 1 = 0 by
190 rw [hphase]; ring]
191 ring
192 · intro hphase hprod
193 apply hphase
194 -- (1/4) · e^{-i(...)} · (exp(...) - 1) = 0 with first two factors nonzero
195 -- forces (exp(...) - 1) = 0.
196 have habc :
197 ((1 : ℂ) / 4) *
198 Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) ≠ 0 :=
199 mul_ne_zero h14 hexp_pos
200 rcases mul_eq_zero.mp hprod with h | h
201 · exact (habc h).elim
202 · exact sub_eq_zero.mp h
203
204/-- Algebraic entanglement witness: when the entangling invariant `Δφ`
205is not in `2π ℤ`, the BMV branch amplitude matrix has nonzero
206determinant, so the corresponding two-qubit pure state is not a product
207state. -/
208theorem entangled_of_branchPhase_nonzero
209 (φ_LL φ_LR φ_RL φ_RR : ℝ)
210 (h : Complex.exp
211 (-Complex.I * (branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR : ℂ)) ≠ 1) :
212 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR) ≠ 0 := by
213 rw [det_ne_zero_iff_branchPhase_ne_zero]
214 exact h
215
216/-- A simple sufficient condition: for `Δφ ∈ ℝ` strictly between `0` and
217`2π`, the corresponding complex exponential is not `1`, and therefore
218the two-qubit state is entangled. This is the version used in the
219paper's Theorem 3 (positivity of entanglement entropy on
220`(0, T_rev)`). -/
221theorem entangled_of_branchPhase_in_open_period
222 (φ_LL φ_LR φ_RL φ_RR : ℝ)
223 (hlo : 0 < branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR)
224 (hhi : branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR < 2 * Real.pi) :
225 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR) ≠ 0 := by
226 apply entangled_of_branchPhase_nonzero
227 -- We use the Mathlib characterization Complex.exp_eq_one_iff:
228 -- exp z = 1 ↔ ∃ n : ℤ, z = n * (2π i).
229 intro hexp
230 set x : ℝ := branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR with hx
231 rw [Complex.exp_eq_one_iff] at hexp
232 obtain ⟨n, hn⟩ := hexp
233 -- −i · x = n · (2π · i) ⟹ x = −n · 2π
234 have hpi : (Real.pi : ℂ) ≠ 0 := by
235 exact_mod_cast Real.pi_ne_zero
236 have hI : (Complex.I : ℂ) ≠ 0 := Complex.I_ne_zero
237 have hxeq : (x : ℂ) = - (n : ℂ) * (2 * (Real.pi : ℂ)) := by
238 -- From: -i · x = n · (2π · i), multiply both sides by i:
239 -- -i · x · i = n · (2π · i) · i, i.e. x = -n · 2π using i·i = -1.
240 have h1 : -Complex.I * (x : ℂ) = (n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := hn
241 have h2 : (-Complex.I * (x : ℂ)) * Complex.I =
242 ((n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) * Complex.I := by
243 rw [h1]
244 have hii : Complex.I * Complex.I = -1 := Complex.I_mul_I
245 have hL : (-Complex.I * (x : ℂ)) * Complex.I = (x : ℂ) := by
246 have : (-Complex.I * (x : ℂ)) * Complex.I
247 = - (x : ℂ) * (Complex.I * Complex.I) := by ring
248 rw [this, hii]; ring
249 have hR : ((n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) * Complex.I
250 = - (n : ℂ) * (2 * (Real.pi : ℂ)) := by
251 have : ((n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) * Complex.I
252 = (n : ℂ) * (2 * (Real.pi : ℂ)) * (Complex.I * Complex.I) := by ring
253 rw [this, hii]; ring
254 rw [← hL, h2, hR]
255 have hxeqR : x = - (n : ℝ) * (2 * Real.pi) := by
256 have := hxeq
257 have : (x : ℂ) = ((- (n : ℝ) * (2 * Real.pi) : ℝ) : ℂ) := by
258 rw [hxeq]; push_cast; ring
259 exact_mod_cast this
260 -- Now 0 < x < 2π forces 0 < -n · 2π < 2π, i.e. -1 < -n < 1, i.e. n = 0.
261 -- But then x = 0, contradicting 0 < x.
262 have h2pi_pos : 0 < (2 : ℝ) * Real.pi := by
263 have := Real.pi_pos
264 linarith
265 have hxpos : (0 : ℝ) < - (n : ℝ) * (2 * Real.pi) := by rw [← hxeqR]; exact hlo
266 have hxlt : - (n : ℝ) * (2 * Real.pi) < 2 * Real.pi := by rw [← hxeqR]; exact hhi
267 have hn_pos : (0 : ℝ) < - (n : ℝ) := by
268 have := hxpos
269 have h := (mul_pos_iff.mp this).resolve_right ?_
270 · exact h.1
271 · intro ⟨h1, h2⟩; linarith
272 have hn_lt_one : - (n : ℝ) < 1 := by
273 by_contra hge
274 push_neg at hge
275 have : (1 : ℝ) * (2 * Real.pi) ≤ - (n : ℝ) * (2 * Real.pi) :=
276 mul_le_mul_of_nonneg_right hge (le_of_lt h2pi_pos)
277 linarith
278 -- 0 < -n < 1 with n integer is impossible
279 have hn_int_pos : 0 < (-n : ℤ) := by
280 have hcast : ((-n : ℤ) : ℝ) = - (n : ℝ) := by push_cast; ring
281 have := hn_pos
282 rw [← hcast] at this
283 exact_mod_cast this
284 have hn_int_lt_one : (-n : ℤ) < 1 := by
285 have hcast : ((-n : ℤ) : ℝ) = - (n : ℝ) := by push_cast; ring
286 have := hn_lt_one
287 rw [← hcast] at this
288 exact_mod_cast this
289 omega
290
291/-! ## Weak-field BMV phase formula -/
292
293/-- The weak-field gravitational interaction phase between mass-1 in
294branch position `r_a` and mass-2 in branch position `r_b`, accumulated
295over time `T`. -/
296def weakFieldPhase (G hbar m1 m2 T r : ℝ) : ℝ :=
297 G * m1 * m2 * T / (hbar * r)
298
299/-- The weak-field entangling invariant `Δφ` evaluated for a BMV
300configuration with the four branch separations `r_LL, r_LR, r_RL, r_RR`. -/
301def weakFieldBranchInvariant
302 (G hbar m1 m2 T r_LL r_LR r_RL r_RR : ℝ) : ℝ :=
303 weakFieldPhase G hbar m1 m2 T r_LL +
304 weakFieldPhase G hbar m1 m2 T r_RR -
305 weakFieldPhase G hbar m1 m2 T r_LR -
306 weakFieldPhase G hbar m1 m2 T r_RL
307
308/-- Closed-form for the weak-field entangling invariant. -/
309theorem weakFieldBranchInvariant_eq
310 (G hbar m1 m2 T r_LL r_LR r_RL r_RR : ℝ)
311 (hhbar : hbar ≠ 0)
312 (hLL : r_LL ≠ 0) (hLR : r_LR ≠ 0)
313 (hRL : r_RL ≠ 0) (hRR : r_RR ≠ 0) :
314 weakFieldBranchInvariant G hbar m1 m2 T r_LL r_LR r_RL r_RR
315 = (G * m1 * m2 * T / hbar) *
316 (1 / r_LL + 1 / r_RR - 1 / r_LR - 1 / r_RL) := by
317 unfold weakFieldBranchInvariant weakFieldPhase
318 field_simp
319
320/-! ## Master witness -/
321
322/-- The complete content of T3: given the linear cost-gradient channel
323of T2 and the weak-field BMV phase formula, the BMV branch state is
324entangled whenever the entangling invariant `Δφ` lies in the open
325interval `(0, 2π)`. The witness is `det A ≠ 0`. -/
326structure BMVPositiveTheorem where
327 /-- The amplitude-matrix determinant in closed form. -/
328 det_formula :
329 ∀ (φ_LL φ_LR φ_RL φ_RR : ℝ),
330 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR)
331 = (1 / 4 : ℂ) *
332 Complex.exp (-Complex.I * ((φ_LR : ℂ) + (φ_RL : ℂ))) *
333 (Complex.exp
334 (-Complex.I *
335 (branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR : ℂ)) - 1)
336 /-- Algebraic entanglement witness for `Δφ ∈ (0, 2π)`. -/
337 entangled_open_period :
338 ∀ (φ_LL φ_LR φ_RL φ_RR : ℝ),
339 0 < branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR →
340 branchPhaseInvariant φ_LL φ_LR φ_RL φ_RR < 2 * Real.pi →
341 Matrix.det (branchAmplitudeMatrix φ_LL φ_LR φ_RL φ_RR) ≠ 0
342 /-- Weak-field formula for the entangling invariant. -/
343 weakField_formula :
344 ∀ (G hbar m1 m2 T r_LL r_LR r_RL r_RR : ℝ),
345 hbar ≠ 0 →
346 r_LL ≠ 0 → r_LR ≠ 0 → r_RL ≠ 0 → r_RR ≠ 0 →
347 weakFieldBranchInvariant G hbar m1 m2 T r_LL r_LR r_RL r_RR
348 = (G * m1 * m2 * T / hbar) *
349 (1 / r_LL + 1 / r_RR - 1 / r_LR - 1 / r_RL)
350
351/-- The canonical inhabitant of `BMVPositiveTheorem`. -/
352def bmvPositiveTheorem : BMVPositiveTheorem where
353 det_formula := det_branchAmplitude_factored
354 entangled_open_period := entangled_of_branchPhase_in_open_period
355 weakField_formula := weakFieldBranchInvariant_eq
356
357theorem bmvPositiveTheorem_inhabited : Nonempty BMVPositiveTheorem :=
358 ⟨bmvPositiveTheorem⟩
359
360end
361
362end BMVPositive
363end QuantumChannel
364end Gravity
365end IndisputableMonolith
366