Prove2Me

Relative dimension of a lifted local subspace: R(liftS(Y))=dim⁡Y/2∣S∣\mathrm{R}(\mathrm{lift}_S(Y)) = \dim Y / 2^{|S|}

Proved
QLLL.QSAT.relDim_lift

by sattath · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-qsatlinear-algebraquantum-lll

Model the state space of nn qubits as Hn=C{0,1}n\mathcal{H}_n = \mathbb{C}^{\{0,1\}^n}, the functions from bit strings to C\mathbb{C}, and write R(X)=dim⁡X/2n\mathrm{R}(X) = \dim X / 2^n for the relative dimension of a subspace X⊆HnX \subseteq \mathcal{H}_n. For a set SS of qubits and a subspace YY of the local space C{0,1}S\mathbb{C}^{\{0,1\}^S}, let liftS(Y)⊆Hn\mathrm{lift}_S(Y) \subseteq \mathcal{H}_n be the space of states all of whose SS-slices (obtained by fixing the bits outside SS) lie in YY; in tensor language this is Y⊗C{0,1}ScY \otimes \mathbb{C}^{\{0,1\}^{S^c}}. Then

R(liftS(Y)) = dim⁡Y2∣S∣.\mathrm{R}\big(\mathrm{lift}_S(Y)\big) \ =\ \frac{\dim Y}{2^{|S|}}.

In words, extending a local constraint to all qubits does not change its relative dimension. This converts the local hypotheses of the kk-QSAT corollary (dimension of each local satisfying space) into the relative-dimension hypotheses of the quantum local lemma.

Formalization Note Qubits are modelled as functions on bit strings; the denominator is written as the number of bit strings on SS, which equals 2∣S∣2^{|S|}.

Preamble
import Definitions.Def_QLLL_LocalLemma_Basic
import Definitions.Def_QLLL_Quantum_KQSAT_Basic
import Mathlib

open QLLL
open QLLL.QSAT
open Finset Module
variable {n : ℕ}
Formal statement
theorem QLLL.QSAT.relDim_lift (S : Finset (Fin n)) (Y : Submodule ℂ (HIn S)) :
    relDim (lift S Y) = (Module.finrank ℂ Y : ℝ) / (Fintype.card (CfgIn S) : ℝ) := by sorry
Source
A. Ambainis, J. Kempe, O. Sattath, A Quantum Lovász Local Lemma, J. ACM 59(5):24 (2012), arXiv:0911.1696 (numbering of the arXiv version), Lemma 8 (relative dimension is preserved under tensoring with the full space), as used in Corollary 16

View graph