Quantum local lemma for $k$-QSAT on $n$ qubits, subspace form (Corollary 16)

Let $\mathcal{Q} = \mathbb{C}^2$ be the single-qubit space and, for a finite set $T$ of qubits, let $\mathcal{Q}^{\otimes T} = \bigotimes_{j \in T} \mathcal{Q}$ be Mathlib's tensor power. For a set $S \subseteq \{1, \dots, n\}$ the $n$-qubit space splits as $\mathcal{Q}^{\otimes S} \otimes \mathcal{Q}^{\otimes S^c} \cong \mathcal{Q}^{\otimes n}$. Under this splitting a subspace $Y$ of the local space $\mathcal{Q}^{\otimes S}$ extends to $\mathrm{ext}_S(Y) = Y \otimes \mathcal{Q}^{\otimes S^c}$, and a local operator $P$ on $\mathcal{Q}^{\otimes S}$ extends to $P \otimes I$, where $I$ is the identity on the remaining qubits.

Let $S_1, \dots, S_m$ be sets of qubits and $Y_i \subseteq \mathcal{Q}^{\otimes S_i}$ local subspaces such that:

1. $|S_i| = k$ for every $i$;
2. $\dim Y_i / 2^k \ge 1 - p$ for every $i$;
3. every qubit belongs to at most $D' + 1$ of the sets $S_i$;
4. $p \cdot e \cdot (k D' + 1) \le 1$.

Then

This is Corollary 16 of Ambainis, Kempe and Sattath in its subspace form, stated with Mathlib's tensor product of qubits: local constraints that are large enough and do not overlap too much admit a common nonzero state. The platform has four versions of Corollary 16: on Mathlib's tensor product, the operator form QLLL.PiQSAT.inf_ker_extendOp_ne_bot and the subspace form QLLL.PiQSAT.inf_extend_ne_bot; in the function model, the subspace form QLLL.QSAT.inf_ne_bot_of_degree_le, from which the others are derived, and the orthogonal-projector form QLLL.QSAT.satisfiable_of_degree_le.

Formalization Note The qubit space is Mathlib's PiTensorProduct of Fin 2 → ℂ, and the extension to all qubits is built from Mathlib's PiTensorProduct.tmulEquiv and PiTensorProduct.reindex.