The missing GHZ graph — a visual guide to the Krenn

00 The whole story

The result in ninety seconds

The problem began as a question about whether quantum interference could erase every unwanted six-photon outcome while preserving three desired ones. The proof says: within the exact graph model, no finite complex tuning can do it.

∅

What was proved

No six-vertex, three-color weighted bi-colored multigraph satisfies all 729 inherited-coloring equations over ℂ. Equivalently, the relevant polynomial fiber is empty.

What it means physically

The pair-source/linear-optics graph architecture cannot make an exact six-party qutrit GHZ state at finite amplitudes without stepping outside the modeled resources.

✓

How it was proved

Continuous complex algebra was reduced to eight symmetry classes of Boolean support patterns, cut by exact Laurent identities, refuted by SAT certificates, and checked end to end in Lean.

135complex edge amplitudes

729cubic output equations

15³target matching triples

8symmetry branches

8,421Lean build jobs passed

The central distinction: this is an exact, unrestricted result inside the stated model. “Unrestricted” means arbitrary complex weights, bi-colored edges, and parallel edges are all allowed. It does not mean every conceivable physical apparatus is represented by that model.

01 Build the object

From photon-pair sources to colored lines

No graph theory is assumed. A graph is only a set of points joined by lines. Here the points and lines are a bookkeeping language for indistinguishable ways an optical experiment can produce one photon in every output path.

Quantum-optics picture

○Output path and detector. We postselect events with one detected photon in every path.

↝Probabilistic pair source. A source creates two photons, one into each of two paths.

aInternal mode. Each photon can occupy one of three local modes—our qutrit levels 0, 1, 2.

ℂComplex amplitude. Magnitude and phase determine how indistinguishable alternatives interfere.

Graph picture

●Vertex. Six output paths become six labeled vertices.

—Edge. A possible photon pair becomes an edge joining its two output paths.

◐Endpoint colors. An edge may have different colors at its two ends because the paired photons may have different modes.

wEdge weight. The source amplitude becomes a complex edge weight.

A perfect matching chooses disjoint edges so that every vertex is touched exactly once. With six vertices, that means three pair sources fire and collectively deliver one photon to each of the six outputs. There are 5 × 3 × 1 = 15 such pairings.

Interactive: walk through all 15 perfect matchings

Move the slider to change the pairing. Click a vertex-color button to cycle its local mode; the symbolic cubic contribution updates below.

Try it

Pairing

1 / 15

Inherited vertex colors — click to cycle

This matching contributes one cubic monomial

Each factor is the amplitude for one selected pair source with the endpoint modes shown at its two vertices. The product appears because all three sources must fire in the same sixfold event.

Why sums—not probabilities—matter

Different perfect matchings can lead to the same observed six-mode outcome. Quantum mechanics adds their complex amplitudes first and takes a magnitude squared only afterward. Consequently, two individually possible alternatives can cancel. Complex weights are not a technical embellishment; their phases are the mechanism.

Interactive: rotate one contribution in the complex plane

The red contribution is 1. The blue contribution is e^iφ. Their vector sum is the observable amplitude for one inherited coloring.

Drag phase

Relative phase φ

128°

Complex sum—

Magnitude—

At 180°, the alternatives are both nonzero but sum to zero. The theorem allows cancellations of exactly this kind—across every one of the 726 unwanted outputs—and still proves that no global choice of weights can make them all happen at once.

02 The mathematical target

A sparse target in a 729-dimensional output space

Label the six vertices 0,…,5. For each pair i<j and endpoint colors a,b ∈ {0,1,2}, let W_ij^ab ∈ ℂ be the aggregate complex amplitude. There are 15 × 9 = 135 such numbers.

Why parallel edges are already included. If several physical sources have the same two endpoints and the same endpoint colors, replace them by one edge whose weight is their complex sum. Distributivity makes this aggregation exact, so the 135 variables lose no multigraph generality.

A_c(W) = ∑_{M ∈ PM(K₆)} ∏_{{i,j} ∈ M} W_ij^cᵢcⱼ 15 cubic matching terms for each coloring c ∈ {0,1,2}⁶

A coloring c = (c₀,…,c₅) records the mode detected at every output. The desired six-qutrit GHZ state has amplitude 1 for the three constant colorings 000000, 111111, and 222222, and amplitude 0 for all other 726 colorings.

Interactive: the complete output atlas

Every square is one of the 3⁶ = 729 colorings. Hover or tap to decode a square. Only the three bright diagonal targets should survive.

729 outputs

Desired nonzero3

Required zero726

Visually, the task is extreme sparsification: tune a nonlinear interference network so that almost every output coordinate vanishes while three prescribed coordinates remain exactly one.

Vector-calculus view

A polynomial inverse problem

Package the 729 amplitudes into a cubic map F: ℂ¹³⁵ → ℂ⁷²⁹. Let t be the three-spike GHZ vector. The existence question is simply whether F(W) = t.

F⁻¹(t) = ?

The theorem says the fiber is empty. It does not merely report that an optimizer failed; it proves that the target point is absent from the image.

03 Meaning of the result

The first unrestricted frontier is closed

“Unrestricted” is mathematically substantial here: zero or nonzero complex weights, arbitrary phases, bi-colored endpoints, every vertex pair, and arbitrarily many parallel sources after aggregation are all covered.

Formally verified statement

There does not exist W : WeightsN(6,3,ℂ) satisfying EqSystemN(6,3,W).

In ordinary language: no assignment of complex amplitudes to the 135 endpoint-colored edge types can make the 15-term matching sum equal 1 on all three monochromatic colorings and 0 on every non-monochromatic coloring.

Read the exact Lean theorem ↗

Why (6,3) is the first genuine boundary

(n,d) = (4,3)possible

The six edges of K₄ split into three perfect matchings. Give each matching its own color: this exactly creates the three target terms.

(n,d) = (6,2)possible

An alternating even cycle supplies two monochromatic perfect matchings and no unwanted alternatives. The qubit GHZ construction survives.

(n,d) = (6,3)impossible

This proof shows that adding a third local level creates unavoidable global obstruction—even with arbitrary destructive interference.

Immediate mathematical corollary. Although the packaged Lean theorem names d = 3, a solution with d > 3 would restrict to any three colors and give a forbidden d = 3 solution. Thus the result settles the six-vertex slice of the Krenn–Gu conjecture: its maximum dimension is 2. This restriction corollary is elementary but is not a separately exported theorem in the release.

Proved directly

Exact nonexistence over all complex weights
All bi-colored edge types and multigraphs
The official n = 6, d = 3 equation system
Every finite weight assignment

Follows or is strongly suggested

No n = 6 graph of dimension d ≥ 3
Exact searches in this model can stop
Extra resources are necessary for this route
Support geometry is a useful proof invariant

Not implied

No six-qutrit GHZ state by any physical method
No arbitrarily high-fidelity approximation
The full conjecture for n = 8, 10,…
A quantitative noise or rate bound

04 The geometric surprise

The target can be approached forever and never reached

The no-go theorem coexists with an explicit family whose error tends to zero. This is why numerical optimization looked tantalizing: the obstruction is at finite parameter values, while near-solutions escape toward infinity.

The Erhard border family

Nine nonzero edge types support three target matchings and one unwanted “rainbow” matching. Move x and watch the extra amplitude shrink while the weight scale diverges.

Exact formulas

Scale parameter x

x = —

Target amplitudes1, 1, 1

Unwanted amplitude—

Conditional fidelity—

Largest raw weight—

six edges: x —

three: x⁻² —

If all source amplitudes are uniformly rescaled to keep the largest at 1, each desired three-edge amplitude scales as x⁻³; the corresponding coincidence-rate scale falls like x⁻⁶. The normalized state improves while the usable event rate tends to zero.

The geometry in one sentence

The target t lies in the ordinary closure of the polynomial image F(ℂ¹³⁵), but not in the image itself. In inverse-problem language, increasingly good fits exist only along an unbounded parameter sequence.

This is a global, non-properness phenomenon: bounded output does not force bounded inputs. It is exactly the situation in which “the residual keeps falling” is not evidence of a finite solution.

Relation to Jacobian-style geometry. Both themes warn that local algebraic behavior need not settle a global inverse problem. But this proof does not use a Jacobian-conjecture counterexample: F is rectangular (135 → 729), no local invertibility is asserted, and the precise issue here is escape to infinity plus a non-closed image. The final algebraic tools are Laurent identities and finite support stratification.

05 Significance beyond pure mathematics

A resource boundary for one quantum-optical architecture

The graph equations encode amplitudes, not a loose analogy. Under the stated pair-source correspondence, an exact graph solution would compile into an experiment producing the high-dimensional GHZ state below.

|GHZ_6,3⟩ = 1/√3 ( |000000⟩ + |111111⟩ + |222222⟩ )

Each of the six parties has a three-dimensional local state—a qutrit. GHZ states are maximally correlated multipartite states: measuring one party in the displayed basis fixes what every other party will see, while the three global alternatives remain in coherent superposition.

Direct consequence

Stop exact searches inside this model for six-party dimension three. No denser six-output graph, larger collection of parallel pair sources, clever phase choice, or bi-colored edge can produce a finite exact solution, because all reduce to the 135 aggregate amplitudes already ruled out.

Operational reading

Additional resources are necessary. An experimenter seeking an exact six-qutrit GHZ state must relax some modeled assumption—for example by adding heralding/ancillary structure, a different source primitive, additional measurement resources, or another architecture.

Expected value

Search budgets can move from impossible exact synthesis to useful tradeoffs. The border family suggests studying fidelity versus count rate, bounded source strengths, robustness, and which added resource closes the gap most economically.

Methodological promise

The proof architecture may transfer. Support stratification + exact algebraic no-goods + SAT proof traces + formal semantic replay is a plausible template for other finite quantum experiment-design no-go questions. This is a research prospect, not a theorem exported by this result.

Inside the theorem

Six postselected output paths
Pair-source graph amplitudes
Three endpoint modes
Arbitrary finite complex weights
Exact GHZ amplitudes

All of quantum physics

Ancillary/heralding photons
Higher-order or deterministic sources
Adaptive measurements and feed-forward
Approximate states and noisy protocols
Other encodings and architectures

Do not overread the applications. High-dimensional GHZ states have uses in foundational tests, quantum networks, communication, and cryptography. This theorem does not prove that any such task is impossible or insecure. It constrains one state-generation resource model at one particle count, and its broader value is guidance about which resources must change.

06 Method of proof

Turn a continuous impossibility into eight finite contradictions

A direct assault on 729 cubic equations in 135 complex variables is too large and too unstructured. The proof keeps exact algebra where phases matter, but projects first to the zero/nonzero pattern—the combinatorial shadow on which exhaustive reasoning becomes possible.

Begin by assuming the impossible object exists

Suppose some complex weight tensor W satisfies the official equation system. Every following object—the support bits, selected matching triple, symmetry branch, semantic clauses, and final contradiction—is constructed from that hypothetical W.

135 complex coordinates

Step 1 · Keep only the zero/nonzero shadow

Replace each complex edge weight by one Boolean bit: present if nonzero, absent if zero. A matching term is supported precisely when all three of its edge bits are present. This forgets magnitudes and phases, but two necessary facts survive:

A target sum equal to 1 must contain at least one nonzero matching term.
A nontarget sum equal to 0 cannot contain exactly one nonzero term; a lone nonzero complex number cannot cancel itself.

Interactive: the Boolean shadow of one 15-term equation

Click terms to mark them nonzero. The support test is necessary, not sufficient: two or more terms might cancel, but need not.

Support only

—

Step 2 · Choose one target matching in each color

Each of the three monochromatic equations equals 1, so each supplies at least one supported perfect matching. Choose one red, one blue, and one gold matching. There are 15³ = 3,375 ordered triples—but most differ only by relabeling.

Here is the only group theory needed: S₆ means “all 720 ways to rename six vertices,” and S₃ means “all 6 ways to rename three colors.” Applying either renaming cannot change whether a solution exists. An orbit is simply a bucket of drawings that become identical after such renaming.

Interactive: 3,375 labeled triples collapse to eight shapes

Select an orbit. The diagram overlays its three monochromatic matchings; curved offsets keep coincident colored edges visible.

S₆ × S₃

Orbit 0

—

Underlying edges—

Stabilizer—

Labeled triples—

Share of 3,375—

Orbit size = 4,320 / stabilizer size. The eight sizes add exactly to 3,375.

Step 3 · Use linear algebra to force structure in every support

Fix a root vertex r. For each of its five neighbors v, the nine values W_rv^ab form a 3 × 3 matrix: rows are colors at r, columns are colors at v. The equation system is a tensor identity. Contracting that identity against carefully chosen vectors in ℂ³ turns missing support patterns into kernel vectors that would annihilate every perfect matching while leaving the GHZ tensor nonzero—a contradiction.

Three universal consequences are encoded in every SAT branch. They are best read as geometric restrictions on the five incident matrices, not as arbitrary Boolean clauses.

Interactive: the three universal matrix patterns

Five small matrices represent the five neighbors of a fixed root. One highlighted neighbor must exhibit the selected support pattern.

Linear algebra

Star anchor

Step 4 · Restore exact algebra locally

Support logic alone cannot decide whether two or more nonzero terms cancel. For stubborn local patterns, the proof selects a small set of amplitude equations and treats every supported edge weight as an invertible variable. Negative exponents are then legal, so the natural setting is a Laurent polynomial ring.

A checked certificate supplies rational Laurent polynomials h_i and reconstructed amplitude relations E_i satisfying the exact identity below. If a proposed support realized every E_i = 0, evaluation would turn the identity into 0 = 1.

Hypothetical local realization

E₁(W)=0
E₂(W)=0
⋮
Eₖ(W)=0

Exact checked identity

h₁E₁ + h₂E₂ + ··· + hₖEₖ = 1

therefore 0 = 1

Algebraic-geometric reading. These are local Nullstellensatz-style emptiness certificates on support tori. The proof avoids one enormous global Gröbner-basis computation: it discovers many small exact obstructions and lets Boolean reasoning glue them into a global cover.

Step 5 · Let SAT glue all necessary facts together

Each of the eight orbit representatives fixes nine target-edge bits to true. The common Boolean model then encodes matching support, target nonemptiness, nontarget nonsingleton rules, the universal matrix constraints, and the exact algebraic “no-good” clauses. Every branch is unsatisfiable.

12,330Boolean variables per branch

59–60kCNF clauses per branch

8 / 8branches refuted

64 MBcompact CNF + LRAT data

A SAT solver saying “UNSAT” is not the proof. For each branch, CaDiCaL emitted an LRAT certificate: a checkable derivation of contradiction from the exact clause list. Lean parses the DIMACS formula, verifies the LRAT trace using its standard soundness theorem, and proves that the corresponding Boolean branch has no assignment.

Finally, Lean checks that every clause in the formula really follows from the original complex equation system or from a checked exact certificate. This semantic ledger is the bridge that prevents a perfectly valid SAT refutation of the wrong encoding from masquerading as a graph proof.

The contradiction closes. Any hypothetical complex solution supplies a target matching triple. Lean transports it by a checked vertex/color symmetry into one of the eight canonical branches. That branch is impossible. Therefore the hypothetical solution cannot exist.

07 Formal verification

What the computer checked—and what it was not asked to trust

The final theorem is more than a collection of successful computations. The generated artifacts are treated as untrusted data and connected to the mathematical statement by proved soundness lemmas.

✓Exact theorem typeMatches the official EqSystemN proposition

✓50 checksumsAll committed proof artifacts matched

✓8,421 jobsClean release build completed

✓No sorryAxNo unfinished proof placeholder in closure

Checked trust stack · outside to inside

Eight LRAT refutations + finite orbit data + rational Laurent identities Large generated objects; accepted only after their defining predicates are checked.

Semantic replay and symmetry transport Lean proves that the replayed clauses hold for every genuine solution and that all 3,375 target triples are covered.

Official Formal Conjectures definitions The theorem uses the official WeightsN, pmSumN, and EqSystemN types at a pinned revision.

Lean 4 kernel + native compiler/runtime The large finite decisions use native_decide, so the compiler is explicitly inside the trusted base.

Outside the trusted theorem: Python search programs, numerical optimizers, CaDiCaL as a solver, and external computer-algebra systems generated candidates. They may be buggy without making a false certificate pass Lean’s checked predicates.

The exact release check

The pinned release was verified from a clean checkout with Lean 4.27.0. It completed in 22 minutes 18 seconds on the reference 8-core/16-thread machine. The printed axiom closure contains ordinary Lean foundations plus Lean.ofReduceBool and Lean.trustCompiler, as expected from native_decide; it contains no sorryAx.

git clone https://github.com/algal/krenn-gu-6x3-certificate.git cd krenn-gu-6x3-certificate scripts/verify_release.sh

Why a proof trace is different from trusting the SAT solver

A solver is an optimized search engine and can contain implementation bugs. An LRAT trace records enough local justification for a much smaller checker to verify that the empty clause follows. Lean uses a proved theorem connecting successful verification to propositional unsatisfiability. The solver discovers; the checker certifies.

Why native_decide expands the trust boundary

Ordinary kernel reduction of these large finite tables and proof traces would be impractically slow. native_decide compiles the decision procedure and asks Lean to accept the returned Boolean result through a soundness bridge. That makes the Lean native compiler/runtime trusted for these computations. This is disclosed rather than hidden; it is still a far smaller and clearer boundary than trusting all producer scripts and solvers.

Does the theorem depend on the still-open placeholder in Formal Conjectures?

No. The proof imports the official definitions but proves the right-hand proposition independently. It does not invoke the official theorem whose body still contains the repository’s open-problem placeholder. A status pull request links the external proof and marks the conjecture solved once maintainers review and merge it.

08 Understanding after proof

What this result opens rather than closes

The six-vertex case is complete, but the unrestricted conjecture for larger even systems remains open. The new proof also leaves a conceptual compression problem: can its many exact local obstructions be organized into a shorter structural theorem?

Find the human-scale invariant

The eight finite contradictions may be shadows of a single structural obstruction. Mining the Laurent cuts and universal matrix rules for that invariant could turn the certificate into a reusable theorem.

Move to n = 8, d = 3

This is the next unrestricted slice of the conjecture. Naive scaling is severe: 105 perfect matchings and 6,561 output colorings. New compression, not mere brute force, will likely be needed.

Make the no-go quantitative

Under bounded physical amplitudes, how close can one get, and at what coincidence rate? A robust inequality would speak more directly to laboratories than exact nonexistence alone.

Price the missing resource

Which smallest extension—ancilla, heralding, different source arity, adaptive measurement—permits exact synthesis? The theorem turns “try harder” into a resource-separation question.

A broader methodological bet. Many design problems ask whether a sparse target lies in the image of a structured polynomial map. When solutions can escape to infinity and the full ideal is too large, the mix used here—support geometry, symmetry, small exact identities, proof-producing SAT, and formal replay—deserves testing well beyond this graph problem.

09 Reference

Glossary and primary sources

Graph: A collection of vertices (points) and edges (connections). No geometry or distance is implied.
Perfect matching: A set of disjoint edges touching every vertex exactly once. On six vertices it contains three edges.
Inherited vertex coloring: The color each vertex receives from the endpoint of its unique matching edge.
Support: The set of coordinates whose complex weights are nonzero. It forgets values while retaining combinatorial possibility.
Orbit: An equivalence class under allowed relabelings. Here vertex and color renamings reduce 3,375 cases to eight.
Laurent polynomial: A polynomial that also permits negative integer exponents, appropriate when selected variables are known nonzero.
CNF / SAT: A standard Boolean constraint format and the problem of deciding whether any truth assignment satisfies it.
LRAT: A line-by-line certificate that a CNF formula is unsatisfiable, designed for small trusted checkers.
Lean: A proof assistant whose kernel checks formal terms against precise types and previously proved theorems.
GHZ state: A coherent superposition of globally correlated basis states, central to multipartite quantum information.

Primary sources and audit trail

Pinned Lean proof release and verification instructions — source of the theorem, proof architecture, artifact counts, and trust boundary.
Final Lean theorem — the exact unrestricted (6,3) statement.
Formal Conjectures registration PR #4610 — links the pinned external proof to the official conjecture.
M. Krenn, X. Gu, A. Zeilinger, Quantum Experiments and Graphs: Multiparty States as Coherent Superpositions of Perfect Matchings — the graph/optics correspondence.
M. Krenn, X. Gu, D. Soltész, Questions on the Structure of Perfect Matchings inspired by Quantum Physics — inherited vertex coloring and the original question.
Original MathOverflow formulation — concise definitions of bi-colored weighted graphs and coloring weights.
L. S. Chandran, R. Gajjala, A. M. Illickan, Krenn–Gu conjecture for sparse graphs — physical motivation, resource interpretation, and earlier structural results.
Mario Krenn’s problem and status page — historical context and known special cases.