FormationBounds

Abstract

Qubit entropy, convex concurrence cost and selective finite-ensemble formation bounds.

Scalar quotients are real unless a complex cast is displayed. Fin indices are zero based. Matrix, rankOneDensity, partialTraceRight and partialTransposeB denote the actual Lean operations. All entropy values are in bits.

Theorem 1.1 (Determinant bounds for a qubit density matrix).

$$\forall (\tau :\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{PosSemidef}(\tau ))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}(\tau )=1)\Rightarrow ((0\le \mathrm{Complex}.\mathrm{re}(\mathrm{Matrix}.\det (\tau )))\wedge (\mathrm{Complex}.\mathrm{re}(\mathrm{Matrix}.\det (\tau ))\le \frac{1}{4})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.qubit_det_bounds (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

A positive semidefinite two-by-two complex matrix with trace one has real determinant between zero and one quarter. Its two nonnegative eigenvalues sum to one, and their product is the determinant.

Theorem 1.2 (Direct.pure_det).

$$\forall (\psi :((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)))\to \mathbb{C}),\mathrm{Complex}.\mathrm{re}(\mathrm{Matrix}.\det (D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}(D5.S3.\mathrm{Quantum}.\mathrm{PureState}.\mathrm{PureStateHandshake}.\mathrm{rankOneDensity}(\psi ))))={\Vert \mathrm{Matrix}.\det (\mathrm{Matrix}.\mathrm{of}(\mathrm{Function}.\mathrm{curry}(\psi )))\Vert }^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.pure_det (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

For any two-qubit amplitude vector, the real determinant of the left marginal of its rank-one density matrix equals the squared norm of the determinant of the amplitude matrix. The identity holds for arbitrary complex amplitudes.

Definition 1.3 (Ensemble).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\mathrm{Ensemble}\left(\rho \right)=\{N:\mathbb{N};weight:\mathrm{Fin}\left(N\right)\to \mathbb{R};\mathrm{nonneg}:\forall (i:\mathrm{Fin}\left(N\right)),0\le weight(i);{\mathrm{le}}_{one}:\forall (i:\mathrm{Fin}\left(N\right)),weight(i)\le 1;\mathrm{total}:\sum _{i\in \mathrm{Fin}\left(N\right)}(weight(i))=1;\psi :\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C};\mathrm{unit}:\forall (i:\mathrm{Fin}\left(N\right)),\sum _{x\in (\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))}(\Vert \psi (i)(x){\Vert }^2)=1;\mathrm{average}:\sum _{i\in \mathrm{Fin}\left(N\right)}((weight(i):\mathbb{C})\cdot \mathrm{rankOneDensity}\left(\psi (i)\right))=\rho \}$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.Ensemble (✓ std3).

Citation. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

The dependent record has fields N, weight, nonneg, le_one, total, psi, unit and average. Page 18: “Let ρAB be a density matrix acting on CᵖA ⊗ CᑫB, where pq = n. Let Sρ = {{pi, |ψi⟩ : i = 1, 2, …, N} : ρAB = ∑ⁿᵢ₌₁ pi|ψi⟩AB⟨ψi|, where |ψi⟩AB ∈ CᵖA ⊗ CᑫB, 0 ≤ pi ≤ 1 and ∑ᴺᵢ₌₁ pi = 1}.” The reconstruction is read over N ensemble terms and uses Euclidean unit vectors.

Definition 1.4 (S).

$$\forall (p:\mathbb{N}),\forall (\tau :\mathrm{Matrix}\left(\mathrm{Fin}\left(p\right),\mathrm{Fin}\left(p\right),\mathbb{C}\right)),S\left(\tau \right)=\{\begin{array}{ll}\frac{{\sum }_{i\in \mathrm{Fin}\left(p\right)}(\mathrm{Real}.\mathrm{negMulLog}(h.\mathrm{eigenvalues}(i)))}{\mathrm{Real}.\log (2)}& \mathrm{if}h:\tau .\mathrm{IsHermitian}\\ 0& \mathrm{otherwise}\end{array}$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.S (✓ std3).

Citation. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Page 4: “The von Neumann entropy of an n × n density matrix ρ is S(ρ) = −∑ⁿᵢ₌₁ λi(ρ) log₂ λi(ρ).” Real.negMulLog handles zero eigenvalues; division by Real.log 2 converts natural logs to bits. The non-Hermitian branch is zero and is not used for density matrices.

Definition 1.5 (ensembleCost).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\forall (e:\mathrm{Ensemble}\left(\rho \right)),\mathrm{ensembleCost}\left(e\right)=\sum _{i\in \mathrm{Fin}\left(e.N\right)}(e.\mathrm{weight}(i)\cdot S\left(\mathrm{partialTraceRight}\left(\mathrm{rankOneDensity}\left(e.\mathrm{psi}(i)\right)\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.ensembleCost (✓ std3).

Citation. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

The finite weighted entropy of the literal second-factor partial traces.

Definition 1.6 (E_F).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),E_F(\rho )=\mathrm{sInf}\left(\{t:\mathbb{R}\mid \exists e:\mathrm{Ensemble}\left(\rho \right),t=\mathrm{ensembleCost}\left(e\right)\}\right)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.E_F (✓ std3).

Citation. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Page 18: “The entanglement of formation of ρAB is denoted and defined by EF(ρAB) = inf{pi,|ψi⟩:i=1,2,…,N}∈Sρ ∑ᴺᵢ₌₁ piS(trX(|ψi⟩AB⟨ψi|)), where X = A or X = B.” The real infimum uses the finite Euclidean-unit ensembles above and X = B. For a pure state the two marginals have the same nonzero spectrum, so X = A gives the same value in bits: zero eigenvalues contribute zero. The repository’s frozen D5/S3/Quantum/Information/InputInformationBalance.pure_complementary_entropy states this equality; it is not on this module’s dependency path. Spectral ensemble nonemptiness is proved below.

Theorem 1.7 (cost_set_nonempty_iff).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\{t:\mathbb{R}\mid \exists e:\mathrm{Ensemble}\left(\rho \right),t=\mathrm{ensembleCost}\left(e\right)\}.\mathrm{Nonempty}⟺\mathrm{Nonempty}\left(\mathrm{Ensemble}\left(\rho \right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.cost_set_nonempty_iff (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Definition 1.8 (Analytic.f).

$$\forall (c:\mathbb{R}),\mathrm{Analytic}.f(c)=\mathrm{CloningMachine}.\mathrm{binaryEntropyBits}(\frac{1-\mathrm{Real}.\mathrm{sqrt}(1-(c{)}^2)}{2})$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.f (✓ std3).

Citation. William K. Wootters (1998). Entanglement of Formation of an Arbitrary State of Two Qubits. DOI: 10.1103/PhysRevLett.80.2245. URL: https://arxiv.org/abs/quant-ph/9709029v2.

Commentary.

Wootters equations (6)–(8) write h(x) = Real.binEntropy(x) / Real.log(2). The frozen CloningMachine.binaryEntropyBits supplies this bit entropy.

Theorem 1.9 (Analytic.star_root_upper).

$$\forall (c:\mathbb{R}),((0\le c)\wedge ((c{)}^2\le \frac{1}{64}))⟶\mathrm{Analytic}.f(c)<\frac{1}{25}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.star_root_upper (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.10 (Analytic.lower_rational).

$$\forall (k:\mathbb{N}),(32\le k)⟶\frac{499751}{16646144}<\frac{7\cdot ((k:\mathbb{R})-1)}{8\cdot (k:\mathbb{R})-2}\cdot \mathrm{Analytic}.f(\frac{8}{63})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.lower_rational (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.11 (Analytic.upper_rational).

$$\forall (q:\mathbb{N}),(64\le q)⟶\frac{\frac{(q:\mathbb{R})}{25}+1}{2\cdot (q:\mathbb{R})-1}\le \frac{89}{3175}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.upper_rational (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.12 (qubit_entropy_det).

$$\forall (\tau :\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),((\tau .\mathrm{PosSemidef})\wedge (\tau .\mathrm{trace}=1))⟶S\left(\tau \right)=\mathrm{CloningMachine}.\mathrm{binaryEntropyBits}(\frac{1-\mathrm{Real}.\mathrm{sqrt}(1-4\cdot \tau .\det .\mathrm{re})}{2})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.qubit_entropy_det (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.13 (trace_outer).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\psi :(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),\mathrm{rankOneDensity}\left(\psi \right).\mathrm{trace}=(\sum _{x\in (\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))}(\Vert \psi (x){\Vert }^2):\mathbb{C})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.trace_outer (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.14 (marginal_trace).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\psi :(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),\mathrm{partialTraceRight}\left(\mathrm{rankOneDensity}\left(\psi \right)\right).\mathrm{trace}=(\sum _{x\in (\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))}(\Vert \psi (x){\Vert }^2):\mathbb{C})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.marginal_trace (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.15 (pure_qubit_nonneg).

$$\forall (q:\mathbb{N}),\forall (\psi :(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),(\sum _{x\in (\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))}(\Vert \psi (x){\Vert }^2)=1)⟶0\le S\left(\mathrm{partialTraceRight}\left(\mathrm{rankOneDensity}\left(\psi \right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.pure_qubit_nonneg (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.16 (pure_qubit_le_one).

$$\forall (q:\mathbb{N}),\forall (\psi :(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),(\sum _{x\in (\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))}(\Vert \psi (x){\Vert }^2)=1)⟶S\left(\mathrm{partialTraceRight}\left(\mathrm{rankOneDensity}\left(\psi \right)\right)\right)\le 1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.pure_qubit_le_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.17 (qubit_entropy_concave).

$$\mathrm{ConcaveOn}\left(\mathbb{R},\{\tau :\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)\mid \mathrm{IsDensity}\left(\tau \right)\},S\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.qubit_entropy_concave (✓ std3). ∎

Citation. Guifré Vidal (2000). Entanglement monotones. DOI: 10.1080/09500340008244048. URL: https://arxiv.org/abs/quant-ph/9807077v2.

Commentary.

Concavity of the marginal entropy on positive trace-one qubit matrices. The proof reduces eigenvalue entropy to the reused Bloch geometry.

Theorem 1.18 (Analytic.f_convex).

$$\mathrm{ConvexOn}\left(\mathbb{R},\mathrm{Set}.\mathrm{Icc}(0,1),\mathrm{Analytic}.f\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.f_convex (✓ std3). ∎

Citation. William K. Wootters (1998). Entanglement of Formation of an Arbitrary State of Two Qubits. DOI: 10.1103/PhysRevLett.80.2245. URL: https://arxiv.org/abs/quant-ph/9709029v2.

Commentary.

Convexity on the full closed concurrence interval, including both endpoints; Wootters equations (6)–(8).

Theorem 1.19 (spectral_ensemble_nonempty).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),((\rho .\mathrm{PosSemidef})\wedge (\rho .\mathrm{trace}=1))⟶\mathrm{Nonempty}\left(\mathrm{Ensemble}\left(\rho \right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.spectral_ensemble_nonempty (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.20 (formation_nonneg).

$$\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),(\mathrm{Nonempty}\left(\mathrm{Ensemble}\left(\rho \right)\right))⟶0\le E_F(\rho )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.formation_nonneg (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Theorem 1.21 (formation_le_cost).

$$\forall (q:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\forall (e:\mathrm{Ensemble}\left(\rho \right)),E_F(\rho )\le \mathrm{ensembleCost}\left(e\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.formation_le_cost (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean theorem; every displayed parameter is quantified.

Definition 1.22 (Witness.expectation).

$$\forall (w:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right))\to \mathbb{C}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),\mathbb{C}\right)),\mathrm{Witness}.\mathrm{expectation}(w,\rho )=\mathrm{dotProduct}\left(\mathrm{star}\left(w\right),\mathrm{partialTransposeB}\left(\rho \right).\mathrm{mulVec}(w)\right).\mathrm{re}$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.expectation (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

The real quadratic readout of the frozen partial transpose.

Definition 1.23 (Witness.W).

$$\forall (w:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right))\to \mathbb{C}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),\mathbb{C}\right)),\mathrm{Witness}.W(w,\rho )=\max \left(0,-\mathrm{Witness}.\mathrm{expectation}(w,\rho )\right)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.W (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

The positive part of the negative expectation.

Definition 1.24 (Selective.restrictVec).

$$\forall (q:\mathbb{N}),\forall (k:\mathbb{N}),\forall (part:\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(k\right)),\forall (j:\mathrm{Fin}\left(k\right)),\forall (\psi :(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),\forall (x:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))),\mathrm{Selective}.\mathrm{restrictVec}(part,j,\psi )(x)=\mathrm{ite}\left(part(x.2)=j,\psi (x),0\right)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.restrictVec (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean definition; every displayed parameter is quantified.

Definition 1.25 (Selective.branchMass).

$$\forall (q:\mathbb{N}),\forall (k:\mathbb{N}),\forall (part:\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(k\right)),\forall (j:\mathrm{Fin}\left(k\right)),\forall (\psi :(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),\mathrm{Selective}.\mathrm{branchMass}(part,j,\psi )=\sum _{x\in (\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))}(\Vert \mathrm{Selective}.\mathrm{restrictVec}(part,j,\psi )(x){\Vert }^2)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.branchMass (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean definition; every displayed parameter is quantified.

Definition 1.26 (Selective.branchVec).

$$\forall (q:\mathbb{N}),\forall (k:\mathbb{N}),\forall (part:\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(k\right)),\forall (j:\mathrm{Fin}\left(k\right)),\forall (\psi :(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))\to \mathbb{C}),\mathrm{Selective}.\mathrm{branchVec}(part,j,\psi )=\mathrm{ite}\left(\mathrm{Selective}.\mathrm{branchMass}(part,j,\psi )=0,\psi ,(\frac{1}{\mathrm{Real}.\mathrm{sqrt}(\mathrm{Selective}.\mathrm{branchMass}(part,j,\psi ))}:\mathbb{C})\cdot \mathrm{Selective}.\mathrm{restrictVec}(part,j,\psi )\right)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.branchVec (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean definition; every displayed parameter is quantified.

Definition 1.27 (Selective.projectBlock).

$$\forall (q:\mathbb{N}),\forall (k:\mathbb{N}),\forall (part:\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(k\right)),\forall (j:\mathrm{Fin}\left(k\right)),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\forall (x:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))),\forall (y:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right))),\mathrm{Selective}.\mathrm{projectBlock}(part,j,\rho )(x,y)=\mathrm{ite}\left((part(x.2)=j)\wedge (part(y.2)=j),\rho (x,y),0\right)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.projectBlock (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

Literal Lean definition; every displayed parameter is quantified.

Definition 1.28 (Selective.conditionalEnsemble).

$$\forall (q:\mathbb{N}),\forall (k:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\forall (e:\mathrm{Ensemble}\left(\rho \right)),\forall (part:\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(k\right)),\forall (j:\mathrm{Fin}\left(k\right)),\forall (p:\mathbb{R}),\forall (hp:0<p),\forall (r:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\forall (ht:r.\mathrm{trace}=1),\forall (ha:\mathrm{Selective}.\mathrm{projectBlock}(part,j,\rho )=(p:\mathbb{C})\cdot r),(\mathrm{Selective}.\mathrm{conditionalEnsemble}(e,part,j,p,hp,r,ht,ha).N=e.N)\wedge (\forall (i:\mathrm{Fin}\left(e.N\right)),\mathrm{Selective}.\mathrm{conditionalEnsemble}(e,part,j,p,hp,r,ht,ha).\mathrm{weight}(i)=\frac{e.\mathrm{weight}(i)\cdot \mathrm{Selective}.\mathrm{branchMass}(part,j,e.\mathrm{psi}(i))}{p})\wedge (\forall (i:\mathrm{Fin}\left(e.N\right)),\mathrm{Selective}.\mathrm{conditionalEnsemble}(e,part,j,p,hp,r,ht,ha).\mathrm{psi}(i)=\mathrm{Selective}.\mathrm{branchVec}(part,j,e.\mathrm{psi}(i)))$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.conditionalEnsemble (✓ std3).

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

The returned record has type Ensemble r. Its N, weight and psi fields are exactly the displayed expressions. Its nonneg, le_one, total, unit and average proof fields certify the constraints of Ensemble. The positive branch has normalized weights e.weight i · branchMass(part,j,e.psi i) / p and supplies an ensemble for each positive-probability branch.

Theorem 1.29 (Selective.selective_formation).

$$\forall (q:\mathbb{N}),\forall (k:\mathbb{N}),\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),\forall (part:\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(k\right)),\forall (p:\mathrm{Fin}\left(k\right)\to \mathbb{R}),\forall (r:\mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(q\right)),\mathbb{C}\right)),((\mathrm{Nonempty}\left(\mathrm{Ensemble}\left(\rho \right)\right))\wedge (\forall (j:\mathrm{Fin}\left(k\right)),0\le p(j))\wedge (\forall (j:\mathrm{Fin}\left(k\right)),r(j).\mathrm{trace}=1)\wedge (\forall (j:\mathrm{Fin}\left(k\right)),\mathrm{Selective}.\mathrm{projectBlock}(part,j,\rho )=(p(j):\mathbb{C})\cdot r(j)))⟶\sum _{j\in \mathrm{Fin}\left(k\right)}(p(j)\cdot E_F(r(j)))\le E_F(\rho )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.selective_formation (✓ std3). ∎

Citation. Guifré Vidal (2000). Entanglement monotones. DOI: 10.1080/09500340008244048. URL: https://arxiv.org/abs/quant-ph/9807077v2.

Commentary.

Finite projective partitions on the second factor cannot increase formation on average. Zero-probability branches are allowed. This is the coordinate-partition instance of Vidal Theorem 2.

Theorem 1.30 (Witness.witness_lower).

$$\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),\mathbb{C}\right)),\forall (w:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right))\to \mathbb{C}),((\mathrm{Nonempty}\left(\mathrm{Ensemble}\left(\rho \right)\right))\wedge (\sum _{x\in (\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right))}(\Vert w(x){\Vert }^2)=1))⟶\mathrm{Analytic}.f(2\cdot \mathrm{Witness}.W(w,\rho ))\le E_F(\rho )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.witness_lower (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Samuel L. Braunstein; Sibasish Ghosh; Simone Severini (2006). The Laplacian of a graph as a density matrix: a basic combinatorial approach to separability of mixed states. DOI: 10.1007/s00026-006-0289-3. URL: https://arxiv.org/abs/quant-ph/0406165v2.

Commentary.

The new formation lower bound combines the determinant readout estimate with the convex concurrence function.

References

• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.E_F
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.Ensemble
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.S
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.W
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.branchMass
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.branchVec
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.conditionalEnsemble
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.cost_set_nonempty_iff
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.ensembleCost
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.expectation
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.f
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.f_convex
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.formation_le_cost
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.formation_nonneg
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.lower_rational
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.marginal_trace
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.projectBlock
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.pure_det
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.pure_qubit_le_one
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.pure_qubit_nonneg
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.qubit_det_bounds
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.qubit_entropy_concave
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.qubit_entropy_det
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.restrictVec
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.selective_formation
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.spectral_ensemble_nonempty
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.star_root_upper
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.trace_outer
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.upper_rational
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds.witness_lower
• Dependency: D5/S3/Quantum/CloningMachine
• Dependency: D5/S3/Quantum/Divergence/ConditionalHockeyStickOrthogonalReduction
• Dependency: D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation
• Dependency: D5/S3/Quantum/Fibers/PhysicalFiber
• Dependency: D5/S3/Quantum/Information/ActualPureQubitGeometry
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
• Dependency: D5/S3/Quantum/Information/QubitNormalFormState
• Dependency: D5/S3/Quantum/Information/SeparableStateLocalUnitaryStabilizerObstruction
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake
• Dependency: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation