IndisputableMonolith.Quantum.PureTwoQubit.EntropyConcurrence
IndisputableMonolith/Quantum/PureTwoQubit/EntropyConcurrence.lean · 675 lines · 52 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Pure Two-Qubit Concurrence and Entanglement Entropy (Track 2.B)
5
6## Status: STRUCTURAL THEOREM (Track 2.B closed; no proof holes, no new RS assumptions).
7
8This module discharges Track 2.B of the master
9plan: the chain from the Wootters concurrence of a pure two-qubit
10amplitude matrix to strict positivity of the von Neumann entanglement
11entropy. The full reduction
12`E_VN(ρ₁) = h((1 + √(1 − C²)) / 2)` is proved by combining:
13
14(i) the **algebraic core**: for `C ∈ (0, 1]`, the value
15 `(1 + √(1 − C²)) / 2` lies in the open unit interval `(1/2, 1]`
16 (strictly less than `1` when `C > 0`), and the binary entropy
17 `h(p) = -p log p - (1-p) log(1-p)` is strictly positive on
18 `(0, 1)` and zero at the endpoints `0, 1`.
19
20(ii) the **reduced-density-matrix step**: for a
21 pure two-qubit state `|ψ⟩ = Σᵢⱼ Aᵢⱼ |ij⟩`, the reduced density
22 matrix `ρ₁ = tr_2 |ψ⟩⟨ψ|` has eigenvalues
23 `(1 ± √(1 − 4|det A|²)) / 2 = (1 ± √(1 − C²)) / 2`, hence
24 `E_VN(ρ₁) = h((1 − √(1 − C²)) / 2)
25 = h((1 + √(1 − C²)) / 2)` (binary entropy is symmetric about
26 `p = 1/2`). This is captured as a Prop-shaped sub-target
27 `PureTwoQubitReducedEntropyTarget` and composed with the algebraic
28 core to give the full entropy-positivity theorem.
29
30## Concurrence convention
31
32For a pure two-qubit amplitude matrix `A : Fin 2 × Fin 2 → ℂ`
33representing a normalized state, the Wootters concurrence is
34`C(A) := 2 · |det A|`. (This is the standard pure-state simplification;
35the general mixed-state Wootters formula reduces to this in the pure
36case.) Strict positivity of `C` is equivalent to nonzero determinant,
37matching the algebraic entanglement witness already proved in
38`Gravity.QuantumChannel.BMVPositive.det_branchAmplitude_factored`.
39
40## What this module proves
41
42* `concurrence`: the Wootters concurrence of a `2×2` amplitude matrix.
43* `concurrence_nonneg`, `concurrence_eq_zero_iff_det_zero`.
44* `binaryEntropy`: `h(p) = -p · log p - (1-p) · log(1-p)`.
45* `binaryEntropy_zero_left`, `binaryEntropy_zero_right`: `h(0) = h(1) = 0`.
46* `binaryEntropy_pos_of_open_unit_interval`: `0 < p < 1 → 0 < h(p)`.
47* `inner_radius_pos_of_pos_concurrence`: for `0 < C ≤ 1`,
48 `(1 + √(1 − C²)) / 2 ∈ (1/2, 1)`.
49* `pureTwoQubitReducedEntropyTarget_holds`: the spectral reduced-entropy
50 target for `reducedDensityVonNeumannEntropy`.
51* `pure_two_qubit_entropy_positive_unconditional`: for normalized states
52 with `0 < C`,
53 `E_VN(ρ₁) > 0`.
54-/
55
56namespace IndisputableMonolith
57namespace Quantum
58namespace PureTwoQubit
59namespace EntropyConcurrence
60
61open Real Complex
62
63noncomputable section
64
65/-! ## §1. Concurrence of a pure two-qubit amplitude matrix -/
66
67/-- The Wootters concurrence of a pure two-qubit amplitude matrix:
68`C(A) = 2 · ‖det A‖`. (For pure two-qubit states, the general
69Wootters formula simplifies to twice the absolute value of the
70determinant of the amplitude matrix.) -/
71def concurrence (A : Matrix (Fin 2) (Fin 2) ℂ) : ℝ :=
72 2 * ‖Matrix.det A‖
73
74/-- Concurrence is non-negative. -/
75theorem concurrence_nonneg (A : Matrix (Fin 2) (Fin 2) ℂ) :
76 0 ≤ concurrence A := by
77 unfold concurrence
78 have h : 0 ≤ ‖Matrix.det A‖ := norm_nonneg _
79 linarith
80
81/-- Concurrence vanishes if and only if the amplitude matrix has
82zero determinant. -/
83theorem concurrence_eq_zero_iff_det_zero (A : Matrix (Fin 2) (Fin 2) ℂ) :
84 concurrence A = 0 ↔ Matrix.det A = 0 := by
85 unfold concurrence
86 constructor
87 · intro h
88 have : ‖Matrix.det A‖ = 0 := by linarith [norm_nonneg (Matrix.det A)]
89 exact norm_eq_zero.mp this
90 · intro h
91 rw [h]
92 simp
93
94/-- Concurrence is positive iff determinant is nonzero. -/
95theorem concurrence_pos_iff_det_ne_zero (A : Matrix (Fin 2) (Fin 2) ℂ) :
96 0 < concurrence A ↔ Matrix.det A ≠ 0 := by
97 rw [show (0 : ℝ) < concurrence A ↔ concurrence A ≠ 0 from
98 ⟨fun h => h.ne', fun h => lt_of_le_of_ne (concurrence_nonneg A) (Ne.symm h)⟩,
99 Ne, concurrence_eq_zero_iff_det_zero]
100
101/-! ## §1b. Reduced density matrix of a pure two-qubit amplitude matrix -/
102
103/-- Frobenius norm-squared of a pure two-qubit amplitude matrix:
104`Σᵢⱼ ‖Aᵢⱼ‖²`, written using `Complex.normSq` so the normalization
105condition is algebraic. -/
106def frobeniusNormSq (A : Matrix (Fin 2) (Fin 2) ℂ) : ℝ :=
107 ∑ i, ∑ j, Complex.normSq (A i j)
108
109/-- The first-qubit reduced density matrix of the pure two-qubit state
110with amplitude matrix `A`. This is the partial trace over the second
111qubit:
112
113`ρ₁(i,k) = Σⱼ Aᵢⱼ · conj(Aₖⱼ)`.
114
115Equivalently, it is `A · A†` in matrix notation. -/
116def reducedDensity (A : Matrix (Fin 2) (Fin 2) ℂ) :
117 Matrix (Fin 2) (Fin 2) ℂ :=
118 fun i k => ∑ j, A i j * (starRingEnd ℂ) (A k j)
119
120/-- The reduced-density trace equals the Frobenius normalization,
121as a complex number. -/
122theorem reducedDensity_trace_eq_frobenius
123 (A : Matrix (Fin 2) (Fin 2) ℂ) :
124 reducedDensity A 0 0 + reducedDensity A 1 1 =
125 (frobeniusNormSq A : ℂ) := by
126 unfold reducedDensity frobeniusNormSq
127 rw [Fin.sum_univ_two, Fin.sum_univ_two, Fin.sum_univ_two]
128 simp [Complex.mul_conj]
129
130/-- If the amplitude matrix is normalized, the reduced density matrix
131has trace one. -/
132theorem reducedDensity_trace_eq_one_of_normalized
133 (A : Matrix (Fin 2) (Fin 2) ℂ)
134 (hNorm : frobeniusNormSq A = 1) :
135 reducedDensity A 0 0 + reducedDensity A 1 1 = 1 := by
136 rw [reducedDensity_trace_eq_frobenius A, hNorm]
137 norm_num
138
139/-- Determinant of the first-qubit reduced density matrix:
140`det(ρ₁) = normSq(det A)`.
141
142This is the key pure-two-qubit algebraic identity behind Wootters'
143formula: the non-product witness `det A ≠ 0` is exactly the positive
144determinant of the reduced density matrix. -/
145theorem reducedDensity_det_eq_normSq_det
146 (A : Matrix (Fin 2) (Fin 2) ℂ) :
147 Matrix.det (reducedDensity A) = (Complex.normSq (Matrix.det A) : ℂ) := by
148 rw [Matrix.det_fin_two]
149 unfold reducedDensity
150 rw [Fin.sum_univ_two, Fin.sum_univ_two, Fin.sum_univ_two, Fin.sum_univ_two]
151 rw [Matrix.det_fin_two A]
152 change
153 (A 0 0 * (starRingEnd ℂ) (A 0 0) + A 0 1 * (starRingEnd ℂ) (A 0 1)) *
154 (A 1 0 * (starRingEnd ℂ) (A 1 0) + A 1 1 * (starRingEnd ℂ) (A 1 1)) -
155 (A 0 0 * (starRingEnd ℂ) (A 1 0) + A 0 1 * (starRingEnd ℂ) (A 1 1)) *
156 (A 1 0 * (starRingEnd ℂ) (A 0 0) + A 1 1 * (starRingEnd ℂ) (A 0 1)) =
157 ((Complex.normSq (A 0 0 * A 1 1 - A 0 1 * A 1 0) : ℝ) : ℂ)
158 rw [Complex.normSq_eq_conj_mul_self]
159 simp only [map_sub, map_mul]
160 ring
161
162/-- Determinant of the first-qubit reduced density matrix:
163`det(ρ₁) = ‖det A‖²`. -/
164theorem reducedDensity_det_eq_norm_det_sq
165 (A : Matrix (Fin 2) (Fin 2) ℂ) :
166 Matrix.det (reducedDensity A) = (‖Matrix.det A‖ ^ 2 : ℂ) := by
167 rw [reducedDensity_det_eq_normSq_det]
168 rw [Complex.normSq_eq_norm_sq]
169 norm_cast
170
171/-- Determinant of the reduced density matrix in concurrence form:
172`det(ρ₁) = C(A)^2 / 4`. -/
173theorem reducedDensity_det_eq_concurrence_sq_div_four
174 (A : Matrix (Fin 2) (Fin 2) ℂ) :
175 Matrix.det (reducedDensity A) = ((concurrence A) ^ 2 / 4 : ℝ) := by
176 rw [reducedDensity_det_eq_norm_det_sq]
177 unfold concurrence
178 norm_num
179 ring
180
181/-- If the pure two-qubit amplitude matrix has nonzero determinant, the
182first-qubit reduced density matrix has nonzero determinant. -/
183theorem reducedDensity_det_ne_zero_of_concurrence_pos
184 (A : Matrix (Fin 2) (Fin 2) ℂ)
185 (hC : 0 < concurrence A) :
186 Matrix.det (reducedDensity A) ≠ 0 := by
187 rw [reducedDensity_det_eq_concurrence_sq_div_four]
188 have hC_ne : concurrence A ≠ 0 := hC.ne'
189 have hsq_ne : (concurrence A) ^ 2 ≠ 0 := pow_ne_zero 2 hC_ne
190 exact_mod_cast div_ne_zero hsq_ne (by norm_num : (4 : ℝ) ≠ 0)
191
192/-- The trace-one characteristic discriminant of the reduced density
193matrix, written in terms of concurrence:
194`tr(ρ₁)^2 - 4 det(ρ₁) = 1 - C(A)^2`.
195
196This is the algebraic bridge from the partial trace to the standard
197eigenvalue expression `(1 ± √(1 - C²))/2`. -/
198theorem reducedDensity_discriminant_eq_one_sub_concurrence_sq
199 (A : Matrix (Fin 2) (Fin 2) ℂ)
200 (_hNorm : frobeniusNormSq A = 1) :
201 (1 : ℂ) - 4 * Matrix.det (reducedDensity A) =
202 ((1 - (concurrence A) ^ 2 : ℝ) : ℂ) := by
203 rw [reducedDensity_det_eq_concurrence_sq_div_four]
204 norm_num
205 ring
206
207/-! ## §1c. Spectral weights from concurrence -/
208
209/-- The upper reduced-density eigenvalue candidate:
210`λ₊(C) = (1 + √(1 - C²)) / 2`. -/
211def lambdaPlus (C : ℝ) : ℝ :=
212 (1 + Real.sqrt (1 - C ^ 2)) / 2
213
214/-- The lower reduced-density eigenvalue candidate:
215`λ₋(C) = (1 - √(1 - C²)) / 2`. -/
216def lambdaMinus (C : ℝ) : ℝ :=
217 (1 - Real.sqrt (1 - C ^ 2)) / 2
218
219/-- The two concurrence spectral weights sum to one. -/
220theorem lambdaPlus_add_lambdaMinus (C : ℝ) :
221 lambdaPlus C + lambdaMinus C = 1 := by
222 unfold lambdaPlus lambdaMinus
223 ring
224
225/-- If `0 ≤ 1 - C²`, the two concurrence spectral weights multiply to
226`C²/4`, matching the determinant of the reduced density matrix. -/
227theorem lambdaPlus_mul_lambdaMinus
228 {C : ℝ} (hdisc : 0 ≤ 1 - C ^ 2) :
229 lambdaPlus C * lambdaMinus C = C ^ 2 / 4 := by
230 unfold lambdaPlus lambdaMinus
231 have hs : (Real.sqrt (1 - C ^ 2)) ^ 2 = 1 - C ^ 2 := by
232 exact Real.sq_sqrt hdisc
233 nlinarith
234
235/-- For `0 ≤ C ≤ 1`, the concurrence spectral weights have the same
236trace and determinant invariants as a normalized reduced density matrix:
237sum `1`, product `C²/4`. -/
238theorem lambdaPair_sum_product_of_concurrence_unit_interval
239 {C : ℝ} (hC_nonneg : 0 ≤ C) (hC_le : C ≤ 1) :
240 lambdaPlus C + lambdaMinus C = 1 ∧
241 lambdaPlus C * lambdaMinus C = C ^ 2 / 4 := by
242 refine ⟨lambdaPlus_add_lambdaMinus C, ?_⟩
243 have hdisc : 0 ≤ 1 - C ^ 2 := by
244 nlinarith [sq_nonneg C, hC_nonneg, hC_le]
245 exact lambdaPlus_mul_lambdaMinus hdisc
246
247/-! ## §2. Binary entropy -/
248
249/-- The binary entropy function `h(p) = -p · log p - (1-p) · log(1-p)`,
250extended by continuity at the endpoints with `h(0) = h(1) = 0`
251(`Real.log 0 = 0` in Mathlib, so the formula evaluates correctly at
252the endpoints). -/
253def binaryEntropy (p : ℝ) : ℝ :=
254 -p * Real.log p - (1 - p) * Real.log (1 - p)
255
256/-- `h(0) = 0`. -/
257theorem binaryEntropy_zero_left : binaryEntropy 0 = 0 := by
258 unfold binaryEntropy
259 simp [Real.log_one]
260
261/-- `h(1) = 0`. -/
262theorem binaryEntropy_zero_right : binaryEntropy 1 = 0 := by
263 unfold binaryEntropy
264 simp [Real.log_one]
265
266/-- Binary entropy is symmetric about `p = 1/2`. -/
267theorem binaryEntropy_symm (p : ℝ) : binaryEntropy (1 - p) = binaryEntropy p := by
268 unfold binaryEntropy
269 ring_nf
270
271/-- Strict positivity of binary entropy on the open unit interval.
272
273For `0 < p < 1`, both `-p · log p` and `-(1-p) · log(1-p)` are
274non-negative (since `log` of a number in `(0, 1)` is negative), and at
275least one is strictly positive (since `p ≠ 0` and `1 - p ≠ 0`). -/
276theorem binaryEntropy_pos_of_open_unit_interval
277 {p : ℝ} (h0 : 0 < p) (h1 : p < 1) :
278 0 < binaryEntropy p := by
279 unfold binaryEntropy
280 -- Show that both terms `-p · log p` and `-(1-p) · log(1-p)` are ≥ 0,
281 -- with the first being > 0 (since 0 < p < 1).
282 have h1mp : 0 < 1 - p := by linarith
283 have hpt1 : p < 1 := h1
284 have hpt2 : 1 - p ≤ 1 := by linarith
285 have hp_log_neg : Real.log p < 0 := Real.log_neg h0 h1
286 have h_first_pos : 0 < -p * Real.log p := by
287 have : Real.log p < 0 := hp_log_neg
288 nlinarith [h0, this]
289 -- Second term `-(1-p) · log(1-p)`: with 0 < 1-p ≤ 1, log(1-p) ≤ 0.
290 -- Its negation times a positive scalar is ≥ 0.
291 have h1mp_log_le : Real.log (1 - p) ≤ 0 := by
292 by_cases h_eq : 1 - p = 1
293 · rw [h_eq]; simp [Real.log_one]
294 · have h1mp_lt : 1 - p < 1 := lt_of_le_of_ne hpt2 h_eq
295 exact (Real.log_neg h1mp h1mp_lt).le
296 have h_second_nonneg : 0 ≤ -(1 - p) * Real.log (1 - p) := by
297 nlinarith [h1mp, h1mp_log_le]
298 linarith [h_first_pos, h_second_nonneg]
299
300/-! ## §3. Inner radius from concurrence -/
301
302/-- For `0 < C ≤ 1`, the value `(1 + √(1 − C²)) / 2` lies strictly
303between `1/2` and `1`. The strict upper bound `< 1` is exactly the
304condition for binary entropy to be positive. -/
305theorem inner_radius_lt_one_of_pos_concurrence
306 {C : ℝ} (hC_pos : 0 < C) (hC_le : C ≤ 1) :
307 (1 + Real.sqrt (1 - C ^ 2)) / 2 < 1 := by
308 -- Need √(1 - C²) < 1, i.e., 1 - C² < 1, i.e., 0 < C².
309 have hC_sq_pos : 0 < C ^ 2 := by positivity
310 have h_arg_lt_one : 1 - C ^ 2 < 1 := by linarith
311 have h_arg_nonneg : 0 ≤ 1 - C ^ 2 := by
312 have : C ^ 2 ≤ 1 := by
313 have : C ^ 2 ≤ 1 ^ 2 := by
314 apply sq_le_sq'
315 · linarith
316 · exact hC_le
317 simpa using this
318 linarith
319 have h_sqrt_lt_one : Real.sqrt (1 - C ^ 2) < 1 := by
320 have h_sqrt_lt_sqrt : Real.sqrt (1 - C ^ 2) < Real.sqrt 1 :=
321 Real.sqrt_lt_sqrt h_arg_nonneg h_arg_lt_one
322 simpa [Real.sqrt_one] using h_sqrt_lt_sqrt
323 linarith
324
325/-- For `0 < C ≤ 1`, the inner radius `(1 + √(1 − C²)) / 2` lies in
326`[1/2, 1)` (lower bound non-strict — equality holds at `C = 1`; upper
327bound strict — the entropy positivity argument needs the upper bound to
328be strict). -/
329theorem inner_radius_in_unit_interval_of_pos_concurrence
330 {C : ℝ} (hC_pos : 0 < C) (hC_le : C ≤ 1) :
331 (1 : ℝ) / 2 ≤ (1 + Real.sqrt (1 - C ^ 2)) / 2 ∧
332 (1 + Real.sqrt (1 - C ^ 2)) / 2 < 1 := by
333 refine ⟨?_, inner_radius_lt_one_of_pos_concurrence hC_pos hC_le⟩
334 have h_arg_nonneg : 0 ≤ 1 - C ^ 2 := by
335 have hCsq_le_one : C ^ 2 ≤ 1 := by
336 have : C ^ 2 ≤ 1 ^ 2 := by
337 apply sq_le_sq'
338 · linarith
339 · exact hC_le
340 simpa using this
341 linarith
342 have h_sqrt_nonneg : 0 ≤ Real.sqrt (1 - C ^ 2) := Real.sqrt_nonneg _
343 linarith
344
345/-- Composing §2 and §3: for `0 < C ≤ 1`, the binary entropy of the
346inner radius is strictly positive. -/
347theorem binaryEntropy_inner_radius_pos_of_concurrence
348 {C : ℝ} (hC_pos : 0 < C) (hC_le : C ≤ 1) :
349 0 < binaryEntropy ((1 + Real.sqrt (1 - C ^ 2)) / 2) := by
350 obtain ⟨h_lo, h_hi⟩ := inner_radius_in_unit_interval_of_pos_concurrence hC_pos hC_le
351 apply binaryEntropy_pos_of_open_unit_interval
352 · linarith
353 · exact h_hi
354
355/-! ## §3b. Spectral closure of the reduced-density-matrix step -/
356
357/-- The manual partial-trace formula agrees with `A · A†`. -/
358theorem reducedDensity_eq_mul_conjTranspose
359 (A : Matrix (Fin 2) (Fin 2) ℂ) :
360 reducedDensity A = A * A.conjTranspose := by
361 ext i k
362 simp only [reducedDensity, Matrix.mul_apply, Matrix.conjTranspose_apply, starRingEnd_apply]
363
364/-- The reduced density matrix is Hermitian. -/
365theorem reducedDensity_isHermitian
366 (A : Matrix (Fin 2) (Fin 2) ℂ) :
367 (reducedDensity A).IsHermitian := by
368 rw [reducedDensity_eq_mul_conjTranspose]
369 exact Matrix.isHermitian_mul_conjTranspose_self A
370
371/-- Trace of the reduced density matrix equals the Frobenius normalization. -/
372theorem reducedDensity_trace_eq_frobenius_complex
373 (A : Matrix (Fin 2) (Fin 2) ℂ) :
374 (reducedDensity A).trace = (frobeniusNormSq A : ℂ) := by
375 rw [Matrix.trace_fin_two, reducedDensity_trace_eq_frobenius A]
376
377theorem reducedDensity_trace_eq_one_of_normalized_complex
378 (A : Matrix (Fin 2) (Fin 2) ℂ)
379 (hNorm : frobeniusNormSq A = 1) :
380 (reducedDensity A).trace = 1 := by
381 rw [reducedDensity_trace_eq_frobenius_complex A, hNorm]
382 norm_num
383
384private theorem lambdaPlus_sub_lambdaMinus (C : ℝ) :
385 lambdaPlus C - lambdaMinus C = Real.sqrt (1 - C ^ 2) := by
386 unfold lambdaPlus lambdaMinus
387 ring
388
389private theorem lambdaPlus_ge_lambdaMinus {C : ℝ} (_hdisc : 0 ≤ 1 - C ^ 2) :
390 lambdaMinus C ≤ lambdaPlus C := by
391 unfold lambdaPlus lambdaMinus
392 linarith [Real.sqrt_nonneg (1 - C ^ 2)]
393
394private theorem sum_product_implies_quadratic
395 {x y p : ℝ} (hsum : x + y = 1) (hprod : x * y = p) :
396 x ^ 2 - x + p = 0 := by
397 have hy : y = 1 - x := by linarith
398 rw [hy] at hprod
399 nlinarith
400
401private theorem eq_lambdaPlus_or_lambdaMinus_of_quadratic
402 {C x : ℝ} (hdisc : 0 ≤ 1 - C ^ 2)
403 (hx : x ^ 2 - x + C ^ 2 / 4 = 0) :
404 x = lambdaPlus C ∨ x = lambdaMinus C := by
405 unfold lambdaPlus lambdaMinus
406 have hs : Real.sqrt (1 - C ^ 2) ^ 2 = 1 - C ^ 2 := Real.sq_sqrt hdisc
407 have hfac :
408 (x - (1 + Real.sqrt (1 - C ^ 2)) / 2) *
409 (x - (1 - Real.sqrt (1 - C ^ 2)) / 2) = 0 := by
410 nlinarith [Real.sqrt_nonneg (1 - C ^ 2), hs]
411 rcases mul_eq_zero.mp hfac with h1 | h2
412 · exact Or.inl (by linarith)
413 · exact Or.inr (by linarith)
414
415private theorem eigenvalues_fin_two_sum_eq_of_complex_sum
416 {e0 e1 t : ℝ} (h : (e0 : ℂ) + (e1 : ℂ) = (t : ℂ)) :
417 e0 + e1 = t := by
418 rw [← Complex.ofReal_add] at h
419 exact Complex.ofReal_injective h
420
421private theorem eigenvalues_fin_two_prod_eq_of_complex_prod
422 {e0 e1 p : ℝ} (h : (e0 : ℂ) * (e1 : ℂ) = (p : ℂ)) :
423 e0 * e1 = p := by
424 rw [← Complex.ofReal_mul] at h
425 exact Complex.ofReal_injective h
426
427private theorem reducedDensity_eigenvalues_sum_eq_one
428 (A : Matrix (Fin 2) (Fin 2) ℂ)
429 (hNorm : frobeniusNormSq A = 1) :
430 let hρ := reducedDensity_isHermitian A
431 hρ.eigenvalues 0 + hρ.eigenvalues 1 = 1 := by
432 intro hρ
433 have htrace := hρ.trace_eq_sum_eigenvalues
434 rw [reducedDensity_trace_eq_one_of_normalized_complex A hNorm, Fin.sum_univ_two] at htrace
435 exact eigenvalues_fin_two_sum_eq_of_complex_sum htrace.symm
436
437private theorem reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four
438 (A : Matrix (Fin 2) (Fin 2) ℂ) :
439 let hρ := reducedDensity_isHermitian A
440 hρ.eigenvalues 0 * hρ.eigenvalues 1 = (concurrence A) ^ 2 / 4 := by
441 intro hρ
442 have hdet := hρ.det_eq_prod_eigenvalues
443 rw [reducedDensity_det_eq_concurrence_sq_div_four A, Fin.prod_univ_two] at hdet
444 exact eigenvalues_fin_two_prod_eq_of_complex_prod hdet.symm
445
446private theorem concurrence_sq_le_one_of_normalized
447 (A : Matrix (Fin 2) (Fin 2) ℂ)
448 (hNorm : frobeniusNormSq A = 1) :
449 (concurrence A) ^ 2 ≤ 1 := by
450 let hρ := reducedDensity_isHermitian A
451 have hsum := reducedDensity_eigenvalues_sum_eq_one A hNorm
452 have hprod := reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four A
453 nlinarith [sq_nonneg (hρ.eigenvalues 0 - hρ.eigenvalues 1), hsum, hprod]
454
455theorem concurrence_le_one_of_normalized
456 (A : Matrix (Fin 2) (Fin 2) ℂ)
457 (hNorm : frobeniusNormSq A = 1) :
458 concurrence A ≤ 1 := by
459 nlinarith [sq_nonneg (concurrence A), concurrence_nonneg A,
460 concurrence_sq_le_one_of_normalized A hNorm]
461
462private theorem reducedDensity_eigenvalues_eq_lambda_or_swap
463 (A : Matrix (Fin 2) (Fin 2) ℂ)
464 (hNorm : frobeniusNormSq A = 1) :
465 let hρ := reducedDensity_isHermitian A
466 let C := concurrence A
467 (hρ.eigenvalues 0 = lambdaPlus C ∧ hρ.eigenvalues 1 = lambdaMinus C) ∨
468 (hρ.eigenvalues 0 = lambdaMinus C ∧ hρ.eigenvalues 1 = lambdaPlus C) := by
469 intro hρ C
470 have hC := concurrence_le_one_of_normalized A hNorm
471 have hdisc : 0 ≤ 1 - C ^ 2 := by
472 nlinarith [sq_nonneg C, concurrence_nonneg A, hC]
473 have hsum := reducedDensity_eigenvalues_sum_eq_one A hNorm
474 have hprod := reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four A
475 have h0q :
476 hρ.eigenvalues 0 ^ 2 - hρ.eigenvalues 0 + C ^ 2 / 4 = 0 :=
477 sum_product_implies_quadratic hsum hprod
478 have h0 := eq_lambdaPlus_or_lambdaMinus_of_quadratic hdisc h0q
479 rcases h0 with h0plus | h0minus
480 · exact Or.inl ⟨h0plus, by linarith [hsum, lambdaPlus_add_lambdaMinus C]⟩
481 · exact Or.inr ⟨h0minus, by linarith [hsum, lambdaPlus_add_lambdaMinus C]⟩
482
483/-- Von Neumann entropy of the first-qubit reduced density matrix, defined
484from the spectral theorem as `-∑ᵢ λᵢ log λᵢ`. -/
485def reducedDensityVonNeumannEntropy
486 (A : Matrix (Fin 2) (Fin 2) ℂ) : ℝ :=
487 let hρ := reducedDensity_isHermitian A
488 (-∑ i : Fin 2, hρ.eigenvalues i * Real.log (hρ.eigenvalues i))
489
490private theorem binaryEntropy_eq_neg_sum_lambda
491 {C : ℝ} (_hC_nonneg : 0 ≤ C) (_hC_le : C ≤ 1) :
492 binaryEntropy (lambdaPlus C) =
493 -(lambdaPlus C * Real.log (lambdaPlus C) +
494 lambdaMinus C * Real.log (lambdaMinus C)) := by
495 have h1 : lambdaMinus C = 1 - lambdaPlus C := by
496 linarith [lambdaPlus_add_lambdaMinus C]
497 unfold binaryEntropy
498 rw [h1]
499 ring
500
501/-- Sub-target capturing the reduced-density-matrix step. It is discharged
502by `pureTwoQubitReducedEntropyTarget_holds` for the canonical spectral
503definition `reducedDensityVonNeumannEntropy`. -/
504def PureTwoQubitReducedEntropyTarget
505 (vonNeumannEntropy : Matrix (Fin 2) (Fin 2) ℂ → ℝ) : Prop :=
506 ∀ (A : Matrix (Fin 2) (Fin 2) ℂ),
507 (∑ i, ∑ j, Complex.normSq (A i j)) = 1 →
508 vonNeumannEntropy A =
509 binaryEntropy ((1 + Real.sqrt (1 - (concurrence A) ^ 2)) / 2)
510
511theorem pureTwoQubitReducedEntropyTarget_holds :
512 PureTwoQubitReducedEntropyTarget reducedDensityVonNeumannEntropy := by
513 intro A hNorm
514 have hNorm' : frobeniusNormSq A = 1 := by
515 simpa [frobeniusNormSq] using hNorm
516 have hC := concurrence_le_one_of_normalized A hNorm'
517 rcases reducedDensity_eigenvalues_eq_lambda_or_swap A hNorm' with h | h
518 · simp only [reducedDensityVonNeumannEntropy]
519 rw [Fin.sum_univ_two, h.1, h.2]
520 rw [← binaryEntropy_eq_neg_sum_lambda (concurrence_nonneg A) hC]
521 unfold lambdaPlus
522 rfl
523 · simp only [reducedDensityVonNeumannEntropy]
524 rw [Fin.sum_univ_two, h.1, h.2]
525 have hneg := binaryEntropy_eq_neg_sum_lambda (concurrence_nonneg A) hC
526 have hadd :
527 lambdaMinus (concurrence A) * Real.log (lambdaMinus (concurrence A)) +
528 lambdaPlus (concurrence A) * Real.log (lambdaPlus (concurrence A)) =
529 lambdaPlus (concurrence A) * Real.log (lambdaPlus (concurrence A)) +
530 lambdaMinus (concurrence A) * Real.log (lambdaMinus (concurrence A)) := by
531 ac_rfl
532 rw [hadd, ← hneg]
533 unfold lambdaPlus
534 rfl
535
536theorem pure_two_qubit_entropy_eq_binaryEntropy_inner_radius
537 (A : Matrix (Fin 2) (Fin 2) ℂ)
538 (hNorm : (∑ i, ∑ j, Complex.normSq (A i j)) = 1) :
539 reducedDensityVonNeumannEntropy A =
540 binaryEntropy ((1 + Real.sqrt (1 - (concurrence A) ^ 2)) / 2) :=
541 pureTwoQubitReducedEntropyTarget_holds A hNorm
542
543/-! ## §4. Reduced-density entropy target (reference) -/
544
545/-- Alias namespace anchor for the reduced-density-matrix sub-target,
546already defined and discharged in §3b. -/
547abbrev PureTwoQubitReducedEntropyTargetDef :=
548 PureTwoQubitReducedEntropyTarget
549
550/-! ## §5. Composite: pure two-qubit entropy positivity -/
551
552/-- **CONDITIONAL CLOSURE: pure two-qubit entropy positivity from
553concurrence positivity.** Given an abstract von Neumann-entropy
554functional satisfying the reduced-density-matrix sub-target, strict
555positivity of the Wootters concurrence implies strict positivity of
556the von Neumann entanglement entropy. -/
557theorem pure_two_qubit_entropy_positive_of_concurrence_positive
558 {vonNeumannEntropy : Matrix (Fin 2) (Fin 2) ℂ → ℝ}
559 (hVN : PureTwoQubitReducedEntropyTarget vonNeumannEntropy)
560 (A : Matrix (Fin 2) (Fin 2) ℂ)
561 (hNorm : (∑ i, ∑ j, Complex.normSq (A i j)) = 1)
562 (hC_pos : 0 < concurrence A)
563 (hC_le : concurrence A ≤ 1) :
564 0 < vonNeumannEntropy A := by
565 rw [hVN A hNorm]
566 exact binaryEntropy_inner_radius_pos_of_concurrence hC_pos hC_le
567
568/-- **UNCONDITIONAL CLOSURE: pure two-qubit entropy positivity from
569concurrence positivity.** Uses the discharged reduced-density-matrix
570sub-target at the canonical spectral definition. -/
571theorem pure_two_qubit_entropy_positive_unconditional
572 (A : Matrix (Fin 2) (Fin 2) ℂ)
573 (hNorm : (∑ i, ∑ j, Complex.normSq (A i j)) = 1)
574 (hC_pos : 0 < concurrence A) :
575 0 < reducedDensityVonNeumannEntropy A := by
576 have hNorm' : frobeniusNormSq A = 1 := by simpa [frobeniusNormSq] using hNorm
577 exact pure_two_qubit_entropy_positive_of_concurrence_positive
578 pureTwoQubitReducedEntropyTarget_holds A hNorm hC_pos
579 (concurrence_le_one_of_normalized A hNorm')
580
581/-! ## §6. Master certificate -/
582
583/-- **PURE TWO-QUBIT CONCURRENCE-ENTROPY CERTIFICATE.**
584
585Five clauses establishing the algebraic core of Track 2.B:
586
5871. `concurrence_nonneg`: the Wootters concurrence is non-negative.
5882. `concurrence_zero_iff_det_zero`: concurrence vanishes iff
589 determinant vanishes.
5903. `reduced_trace`: the reduced-density trace is the Frobenius norm.
5914. `reduced_det`: `det(ρ₁) = C(A)^2 / 4`.
5925. `lambda_pair_sum_product`: the concurrence spectral candidates
593 `λ±(C)` have sum `1` and product `C²/4`.
5946. `binary_entropy_pos`: binary entropy is strictly positive on
595 `(0, 1)`.
5967. `inner_radius_in_unit_interval`: for `0 < C ≤ 1`, the inner radius
597 lies in `[1/2, 1)`.
5988. `entropy_pos_unconditional`: strict concurrence positivity implies
599 strict entropy positivity at `reducedDensityVonNeumannEntropy`.
6009. `reduced_entropy_target`: the canonical spectral entropy functional
601 satisfies `PureTwoQubitReducedEntropyTarget`. -/
602structure PureTwoQubitConcurrenceEntropyCert where
603 /-- (1) Concurrence is non-negative. -/
604 concurrence_nonneg :
605 ∀ A : Matrix (Fin 2) (Fin 2) ℂ, 0 ≤ concurrence A
606 /-- (2) Concurrence zero iff det zero. -/
607 concurrence_zero_iff_det_zero :
608 ∀ A : Matrix (Fin 2) (Fin 2) ℂ,
609 concurrence A = 0 ↔ Matrix.det A = 0
610 /-- (3) Reduced-density trace equals the Frobenius normalization. -/
611 reduced_trace :
612 ∀ A : Matrix (Fin 2) (Fin 2) ℂ,
613 reducedDensity A 0 0 + reducedDensity A 1 1 =
614 (frobeniusNormSq A : ℂ)
615 /-- (4) Reduced-density determinant equals `C(A)^2 / 4`. -/
616 reduced_det :
617 ∀ A : Matrix (Fin 2) (Fin 2) ℂ,
618 Matrix.det (reducedDensity A) = ((concurrence A) ^ 2 / 4 : ℝ)
619 /-- (5) The concurrence spectral candidates have sum one and product `C²/4`. -/
620 lambda_pair_sum_product :
621 ∀ {C : ℝ}, 0 ≤ C → C ≤ 1 →
622 lambdaPlus C + lambdaMinus C = 1 ∧
623 lambdaPlus C * lambdaMinus C = C ^ 2 / 4
624 /-- (6) Binary entropy is positive on (0, 1). -/
625 binary_entropy_pos :
626 ∀ {p : ℝ}, 0 < p → p < 1 → 0 < binaryEntropy p
627 /-- (7) Inner radius lies in [1/2, 1) for 0 < C ≤ 1. -/
628 inner_radius_in_unit_interval :
629 ∀ {C : ℝ}, 0 < C → C ≤ 1 →
630 (1 : ℝ) / 2 ≤ (1 + Real.sqrt (1 - C ^ 2)) / 2 ∧
631 (1 + Real.sqrt (1 - C ^ 2)) / 2 < 1
632 /-- (8) Unconditional entropy positivity. -/
633 entropy_pos_unconditional :
634 ∀ (A : Matrix (Fin 2) (Fin 2) ℂ)
635 (_hNorm : (∑ i, ∑ j, Complex.normSq (A i j)) = 1)
636 (_hC_pos : 0 < concurrence A),
637 0 < reducedDensityVonNeumannEntropy A
638 /-- (9) Canonical spectral entropy satisfies the reduced target. -/
639 reduced_entropy_target :
640 PureTwoQubitReducedEntropyTarget reducedDensityVonNeumannEntropy
641 /-- (10) Conditional entropy positivity for abstract functionals. -/
642 entropy_pos_conditional :
643 ∀ {vonNeumannEntropy : Matrix (Fin 2) (Fin 2) ℂ → ℝ}
644 (_hVN : PureTwoQubitReducedEntropyTarget vonNeumannEntropy)
645 (A : Matrix (Fin 2) (Fin 2) ℂ)
646 (_hNorm : (∑ i, ∑ j, Complex.normSq (A i j)) = 1)
647 (_hC_pos : 0 < concurrence A) (_hC_le : concurrence A ≤ 1),
648 0 < vonNeumannEntropy A
649
650noncomputable def pureTwoQubitConcurrenceEntropyCert :
651 PureTwoQubitConcurrenceEntropyCert where
652 concurrence_nonneg := concurrence_nonneg
653 concurrence_zero_iff_det_zero := concurrence_eq_zero_iff_det_zero
654 reduced_trace := reducedDensity_trace_eq_frobenius
655 reduced_det := reducedDensity_det_eq_concurrence_sq_div_four
656 lambda_pair_sum_product := lambdaPair_sum_product_of_concurrence_unit_interval
657 binary_entropy_pos := binaryEntropy_pos_of_open_unit_interval
658 inner_radius_in_unit_interval :=
659 inner_radius_in_unit_interval_of_pos_concurrence
660 entropy_pos_unconditional := pure_two_qubit_entropy_positive_unconditional
661 reduced_entropy_target := pureTwoQubitReducedEntropyTarget_holds
662 entropy_pos_conditional :=
663 pure_two_qubit_entropy_positive_of_concurrence_positive
664
665theorem pureTwoQubitConcurrenceEntropyCert_inhabited :
666 Nonempty PureTwoQubitConcurrenceEntropyCert :=
667 ⟨pureTwoQubitConcurrenceEntropyCert⟩
668
669end
670
671end EntropyConcurrence
672end PureTwoQubit
673end Quantum
674end IndisputableMonolith
675