BraunsteinGhoshSeveriniStarRefutation

Abstract

Refutation of the Braunstein–Ghosh–Severini star maximum conjecture.

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.

Definition 1.1 (degreeSum).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))\right)),\mathrm{degreeSum}\left(G\right)=\sum _{v\in (\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))}(G.\mathrm{degree}(v))$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.degreeSum (✓ 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 2 defines dG = ∑ᵢ₌₁ⁿ dG(vi). The sum is over Fin p × Fin q.

Definition 1.2 (sigma).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))\right)),\mathrm{sigma}\left(G\right)=(\frac{1}{\mathrm{degreeSum}\left(G\right):\mathbb{R}}:\mathbb{C})\cdot G.\mathrm{lapMatrix}(\mathbb{C})$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.sigma (✓ 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.

Definition 2.2, p. 3: “The density matrix of a graph G is the matrix” σ(G) = (1/dG)L(G). The source expression is the complex SimpleGraph.lapMatrix divided by degreeSum. A nonempty edge set ensures a positive denominator.

Definition 1.3 (root).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (x:(\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))),\mathrm{root}\left(x\right)⟺(\mathrm{val}\left(x.1\right)=0)\wedge (\mathrm{val}\left(x.2\right)=0)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.root (✓ 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 source labels i = sq + s′. Its vertex v₁ is zero-based (0,0).

Definition 1.4 (starGraph).

$$\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\mathrm{starGraph}\left(p,q\right)=\{\begin{array}{ll}\mathrm{SimpleGraph}.\mathrm{starGraph}((⟨0,h.1⟩,⟨0,h.2⟩))& \mathrm{if}h:(0<p)\wedge (0<q)\\ \mathrm{Bot}.\mathrm{bot}& \mathrm{otherwise}\end{array}$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.starGraph (✓ 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 source star K₁,ₙ₋₁ is rooted at v₁. The positive dimensions use Mathlib SimpleGraph.starGraph directly at the two Fin zero coordinates. The total extension is the empty graph when a dimension is zero; the conjecture domain excludes those cases because the edge set must be nonempty.

Definition 1.5 (center).

$$\forall (k:\mathbb{N}),\forall (x:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\cdot k\right))),\mathrm{center}\left(x\right)⟺(\mathrm{val}\left(x.1\right)=0)\wedge (\mathrm{Nat}.\mathrm{mod}(\mathrm{val}\left(x.2\right),2)=0)$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.center (✓ 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 block center has first coordinate zero and an even second coordinate. Nat.mod is natural-number remainder.

Definition 1.6 (Gk).

$$\forall (k:\mathbb{N}),\forall (x:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\cdot k\right))),\forall (y:(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\cdot k\right))),\mathrm{Gk}\left(k\right).\mathrm{Adj}(x,y)⟺(x\ne y)\wedge (((\mathrm{Nat}.\mathrm{div}(\mathrm{val}\left(x.2\right),2)=\mathrm{Nat}.\mathrm{div}(\mathrm{val}\left(y.2\right),2))\wedge (\mathrm{center}\left(x\right)\vee \mathrm{center}\left(y\right)))\vee ((\mathrm{center}\left(x\right))\wedge (\mathrm{center}\left(y\right))\wedge (\mathrm{root}\left(x\right)\vee \mathrm{root}\left(y\right))))$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.Gk (✓ 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.

Each four-vertex block is a star. Block centers are joined to the global root. Nat.div means natural-number integer division; the displayed divisions are not real fractions.

Definition 1.7 (claim).

$$\mathrm{claim}⟺\forall (p:\mathbb{N}),\forall (q:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left((\mathrm{Fin}\left(p\right))\times (\mathrm{Fin}\left(q\right))\right)),((G.\mathrm{Connected})\wedge (G.\mathrm{edgeSet}.\mathrm{Nonempty}))⟶E_F(\mathrm{sigma}\left(G\right))\le E_F(\mathrm{sigma}\left(\mathrm{starGraph}\left(p,q\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.claim (✓ 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.

Conjecture 6.7, p. 18, verbatim: “Let 𝒢⁽ᶜ⁾ₙ be the set of all connected graphs on n vertices. Let G ∈ 𝒢⁽ᶜ⁾ₙ (|V| = pq). Then max𝒢⁽ᶜ⁾ₙ EF(σ(G)) = EF(σ(K₁,ₙ₋₁)).” Encoding: every p,q and connected simple graph on Fin p × Fin q with nonempty edge set. The maximum assertion means that every such graph has formation at most the rooted star.

Theorem 1.8 (family).

$$\forall (k:\mathbb{N}),(32\le k)⟶(\frac{499751}{16646144}<E_F(\mathrm{sigma}\left(\mathrm{Gk}\left(k\right)\right)))\wedge (E_F(\mathrm{sigma}\left(\mathrm{starGraph}\left(2,2\cdot k\right)\right))<\frac{89}{3175})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.family (✓ 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 every k ≥ 32 the family density has a strict lower bound exceeding the strict star upper bound. The difference between the rational bounds is positive.

Theorem 1.9 (result).

$$\neg \mathrm{claim}$$

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

Resolves. Problems/braunstein-ghosh-severini-2006-star-formation-maximum (refuted) by D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.result.

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.

Refutation of BGS Conjecture 6.7: the instance k = 32 has 128 vertices with tensor dimensions 2 × 64. The graph is connected and has nonempty edge set, and its formation exceeds the rooted star.

References

• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.Gk
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.center
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.claim
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.degreeSum
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.family
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.result
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.root
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.sigma
• Truth anchor: D5/S3/Quantum/Entanglement/GraphDensity/BraunsteinGhoshSeveriniStarRefutation.starGraph
• Dependency: D5/S3/Quantum/Divergence/ConditionalHockeyStickOrthogonalReduction
• Dependency: D5/S3/Quantum/Entanglement/GraphDensity/SelectiveFormationBounds
• Dependency: D5/S3/Weil/Probability/FiniteGaussianSchoenberg