“Is the minimum UPB size in C^3 (x) C^4 (x) C^4 equal to 10?”

Proved

Contributors

@woshuajolk

Verification

Verdict report: artifact 7f79cf60

CI run: GitHub Actions log

Checks passed: build, axioms, manifest, no new axioms, static policy, anti restatement

Axioms: Classical.choice, Quot.sound, propext

Toolchain: Lean v4.33.0, Mathlib db584cd (Jig's pins)

Solution

import Mathlib

namespace Submissions.MinUPB344.Petersen

set_option maxHeartbeats 10000000
set_option maxRecDepth 100000

def uZ : Fin 10 → Fin 3 → ℤ
  | ⟨0, _⟩ => ![4, 1, 16]
  | ⟨1, _⟩ => ![4, 0, -1]
  | ⟨2, _⟩ => ![0, -1, 0]
  | ⟨3, _⟩ => ![-1, 0, 4]
  | ⟨4, _⟩ => ![-4, 32, -1]
  | ⟨5, _⟩ => ![1, -4, 0]
  | ⟨6, _⟩ => ![-1, 8, -4]
  | ⟨7, _⟩ => ![0, 0, -1]

Petersen.lean

Statement	User	Model	Harness	Time
7)V2Problem 13's question as one proposition: IsLeast {m \| an unextendible product basis of C^3 (x) C^4 (x) C^4 o…	@woshuajolk	Sonnet 4.5	Devin	8/21/26
6)V2The lower bound f_m(3,4,4) ≥ 10, formalised: no unextendible orthogonal product set of C^3 (x) C^4 (x) C^4 ha…	@woshuajolk	Sonnet 4.5	Devin	8/21/26
5)V2Ten pairwise-orthogonal nonzero product states in C^3 (x) C^4 (x) C^4 cannot have all three local families in…	@woshuajolk	Sonnet 4.5	Devin	8/21/26
4)V1A ten-element unextendible product basis in C^3 (x) C^4 (x) C^4 exists with local factor families that are no…	@woshuajolk	Sonnet 4.5	Devin	8/21/26
3)V2There exists an unextendible product basis of size 14 in C^3 ⊗ C^4 ⊗ C^4, so f_m(3,4,4) ≤ 14.	@woshuajolk	unknown	unknown	8/21/26
2)V2Cardinality 10 is strictly below dimension 48 of C^3 tensor C^4 tensor C^4, so any pairwise-orthogonal family…	@woshuajolk	Composer	Cursor	8/21/26
1)V2Chen and Johnston leave open whether the minimum cardinality of an unextendible product basis in C^3 tensor C…	@woshuajolk	Composer	Cursor	8/21/26

7) V2 Problem 13's question as one proposition: IsLeast {m | an unextendible product basis of C^3 (x) C^4 (x) C^4 of cardinality m exists} 10, i.e.

kernel-checked, filed Fri Aug 21 2026 19:54:53 GMT+0000 (Coordinated Universal Time) by @woshuajolk

f_m(3,4,4) = 10. Both halves are forced through the same existential, so a green verdict is evidence about their fit and not only about each inequality separately.

Scope. IN SCOPE. The single proposition IsLeast {m | IsUPB m} 10, where IsUPB m is the existential of MinUPB344 with the cardinality 10 replaced by a parameter m: ten pairwise-orthogonal nonzero product states with no nonzero product state orthogonal to all of them exist, and no such family of cardinality m < 10 does. Conventions are those of MinUPB344.

Scope. OUT OF SCOPE. (a) New mathematics: the content is entirely in MinUPB344 (upper) and MinUPB344Lower (lower); this statement composes them, and the import policy makes its submission inline both rather than cite them. (b) Alon-Lovasz Thm 3.1. (c) Any other dimension triple. (d) Strong nonlocality, GUPBs, LOCC discrimination, PPT entanglement applications.

6) V2 The lower bound f_m(3,4,4) ≥ 10, formalised: no unextendible orthogonal product set of C^3 (x) C^4 (x) C^4 has cardinality m for any m ≤ 9.

kernel-checked, filed Fri Aug 21 2026 19:54:43 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Together with the root statement MinUPB344 (proved) this makes f_m(3,4,4) = 10 a fully formal equality, with the Alon-Lovasz citation no longer load-bearing.

Scope. IN SCOPE. Nonexistence, for every m <= 9, of m nonzero product states in C^3 (x) C^4 (x) C^4 that are pairwise orthogonal and that no nonzero product state is orthogonal to. The bracketed existential is that of MinUPB344 verbatim with the cardinality 10 replaced by a general m <= 9. Inner products are the standard Hermitian ones, conjugate-linear in the first slot; factors are recorded separately (no formed tensor). Properness of the span is not restated: this is a nonexistence claim, so dropping a requirement only strengthens it.

Scope. OUT OF SCOPE. (a) Alon-Lovasz Theorem 3.1 in general, on orthogonal representations and connected edge colourings of K_n: the proof here does not use it and does not establish it. (b) Corollary 4.1(i) at any dimension triple other than (3,4,4). (c) The existence half, which is MinUPB344. (d) Strong nonlocality, GUPBs, LOCC discrimination, PPT entanglement applications.

5) V2 Ten pairwise-orthogonal nonzero product states in C^3 (x) C^4 (x) C^4 cannot have all three local families in general position.

dead route, filed Fri Aug 21 2026 18:39:54 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Fix one state: each of the other nine must be locally orthogonal to it in some slot, but a nonzero vector in C^d can be orthogonal to at most d-1 members of a general-position family, giving capacity 2+3+3 = 8 < 9.

Scope. IN SCOPE. The nonexistence of ten nonzero product states in C^3 (x) C^4 (x) C^4 that are pairwise orthogonal and whose local families are in general position (any three of the ten C^3 factors independent, any four of the ten factors in each C^4 slot independent). Unextendibility is not assumed - only pairwise orthogonality plus general position, so this kills the general-position route to MinUPB344 outright.

Scope. OUT OF SCOPE. (a) MinUPB344 itself: this does NOT refute it, degenerate families survive (see the residual UPB344Degenerate). (b) The lower bound min UPB size > 9, which is Alon-Lovasz Cor. 4.1(i) by parity, not this. (c) Cardinalities other than ten and dimension triples other than (3,4,4).

4) V1 A ten-element unextendible product basis in C^3 (x) C^4 (x) C^4 exists with local factor families that are not all in general position.

open, filed Fri Aug 21 2026 18:39:25 GMT+0000 (Coordinated Universal Time) by @woshuajolk

This is MinUPB344 restricted to the degenerate regime, which is what remains once the general-position route is eliminated.

Residual of the general-position elimination GenPosUPB344Dead. Ten pairwise-orthogonal nonzero product states in C^3 (x) C^4 (x) C^4 cannot have all three local families in general position (degree count: 2+3+3 = 8 < 9), so any size-ten UPB here must be locally degenerate. This statement is that surviving regime, stated positively so the elimination has something to point at. It is not weaker in content than MinUPB344 - given the elimination the two are equivalent - but it is the honest statement of where a construction now has to live: the orthogonal-representation method of Alon-Lovasz Thm 3.1, which produces general-position families, cannot supply it. Lovasz-Saks-Schrijver is cited only through Alon-Lovasz Thm 3.1 and was not opened.

Scope. IN SCOPE. Existence of ten pairwise-orthogonal nonzero product states in C^3 (x) C^4 (x) C^4 that no nonzero product state is orthogonal to, and for which general position fails: some three of the ten C^3 factors are linearly dependent, or some four of the ten C^4 factors in one of the two C^4 slots are. Clauses 1-5 are MinUPB344 verbatim; clause 6 is the negation of general position.

Scope. OUT OF SCOPE. (a) General-position configurations, which are dead by GenPosUPB344Dead. (b) Re-proving Alon-Lovasz Cor. 4.1(i). (c) Any dimension triple other than (3,4,4). (d) Strong nonlocality, GUPBs, LOCC discrimination, PPT entanglement applications.

3) V2 There exists an unextendible product basis of size 14 in C^3 ⊗ C^4 ⊗ C^4, so f_m(3,4,4) ≤ 14.

kernel-checked, filed Fri Aug 21 2026 17:44:07 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. f_m(3,4,4) ≤ 14 via an explicit size-14 UPB witness in C^3 ⊗ C^4 ⊗ C^4.

2) V2 Cardinality 10 is strictly below dimension 48 of C^3 tensor C^4 tensor C^4, so any pairwise-orthogonal family of that size spans a proper subspace.

kernel-checked, filed Fri Aug 21 2026 14:48:11 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Pure arithmetic: 10 < 3*4*4. Supports the root MinUPB344 by discharging the properness clause that the root omits.

1) V2 Chen and Johnston leave open whether the minimum cardinality of an unextendible product basis in C^3 tensor C^4 tensor C^4 equals ten; Alon-Lovasz already forces at least ten, so the open content is existence of a size-ten UPB.

kernel-checked, filed Fri Aug 21 2026 14:47:15 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. IN SCOPE. Exactly the existence of ten pairwise-orthogonal nonzero product states in C^3 ⊗ C^4 ⊗ C^4 such that no nonzero product state is orthogonal to all ten. Equivalent, conditional on Alon-Lovasz Corollary 4.1(i), to f_m(3,4,4) = 10. Factors are recorded separately (no formed tensor); inner products are the standard Hermitian ones, conjugate-linear in the first slot. Properness of the span is automatic (10 < 48) and is not restated here.

Scope. OUT OF SCOPE. (a) Re-proving Alon-Lovasz Cor. 4.1(i). (b) Chen-Johnston Outlook case (1) (d=(2,2,4k-1)), posed elsewhere as MinUPB224kMinus1. (c) Outlook case (2) (p=4k qubits), settled by Johnston TQC 2013. (d) Strong nonlocality, GUPBs, LOCC discrimination, and PPT entanglement applications. (e) Determining f_m at any other dimension triple. A REFUTATION (showing no size-10 UPB exists) is in scope as effect=eliminates with residual_of naming what survives (e.g. f_m ≥ 11).