Complexity of Quantum Logic Satisfiability in Fixed Dimension: Realification and Rank-One Encodings

Complexity of Quantum Logic Satisfiability in Fixed Dimension: Realification and Rank-One Encodings Joaquim Reizi Higuchi November 17, 2025 Abstract Quantum propositional logic, introduced by Birkhoff and von Neumann, formalizes reasoning about experimental propositions in quantum mechanics through closed subspaces of Hilbert spaces. We provide a comprehensive complexity analysis of the satisfiability problem for quantum logic formulas over the connectives conjunction, disjunction, and negation. Distinguishing between weak satisfiability (evaluation to a nonzero subspace) and strong satisfiability (evaluation to the full space), we establish that both notions coincide with Boolean satisfiability for dimension one, are classically NP-complete for dimension two, and become complete for the Blum–Shub–Smale class NPRwhen dimension d≥3is fixed. Our principal contribution is twofold. First, we present two alternative constructive reductions from quantum logic satisfiability to the Existential Theory of the Reals (ETR): a realification-based encoding that explicitly handles the complex-to-real translation through commutant characterizations, and a rank-one column encoding with orthogonal splitting gadgets. Both reductions yield polynomial-size systems of quadratic equations for fixed dimension, proving membership in the complexity class ∃Rand hence in PSPACE via Canny’s algorithm. Second, we provide detailed size bounds distinguishing weak and strong satisfiability: weak satisfiability encodes with O(nD2+N∨D)scalar variables where nis the number of atoms, Dthe real dimension, and N∨the number of disjunctions, while strong satisfiability requires O(nD2+N∨D2)variables due to basis-vector witnesses. When dimension is part of the input, strong satisfiability becomes polynomial-time equivalent to feasibility of non-commutative integer polynomial equations. These results position quantum logic satisfiability precisely between classical NP and ∃R, highlighting dimension as a fundamental complexity parameter. 1 Introduction Propositional quantum logic captures the logical structure of experimental propositions about quantum systems. For a finite-dimensional Hilbert space Hover Ror C, the lattice L(H)of closed subspaces is modular and orthocomplemented but generally non-distributive, distinguishing it fundamentally from classical Boolean algebras. A valuation vassigns to each propositional variable a closed subspace of H. Negation ¬pis interpreted as the orthogonal complement of v(p), conjunction p∧qas the intersection of subspaces, and disjunction p∨qas the closed linear span of v(p) and v(q). While various notions of implication have been studied in quantum logic, we restrict attention to the {∧,∨,¬}-fragment and its satisfiability problems. Two semantically distinct notions of satisfiability arise naturally in this setting. A formula ϕis weakly satisfied by valuation vif the subspace v(ϕ)is nonzero, denoted ϕ∈WL(H). A 1 formula is strongly satisfied if v(ϕ) = H, denoted ϕ∈QL(H). In the classical Boolean case where dim(H)=1, these notions coincide with propositional satisfiability. For higher dimensions they diverge: the formula pis weakly satisfiable in any dimension but never strongly satisfiable unless the valuation assigns the entire space to p. This distinction proves crucial for complexity classification. 1.1 Complexity landscape and main results Herrmann and Ziegler [1] established foundational complexity results for quantum logic satisfiability. They proved that for dim(H) = 2, both weak and strong satisfiability are NP-complete through reductions encoding Boolean formulas into one-dimensional subspaces of C2using orthogonality to simulate negation. For fixed dimension d≥3, they showed completeness for NPR, the class of problems decidable in nondeterministic polynomial time on a Blum–Shub–Smale machine over the reals. Furthermore, they proved that strong satisfiability in indefinite but finite dimension is polynomially equivalent to feasibility of non-commutative integer polynomial equations. These results firmly place quantum logic satisfiability between classical NP and the existential theory of the reals. Our work provides a self-contained and comprehensive treatment of these complexity results with three principal contributions. First, we develop two distinct constructive reductions from quantum logic satisfiability to ETR for fixed dimension. The realification-based approach explicitly manages the complex-to-real translation through detailed characterizations of the commutant of the canonical complex structure matrix, while the rank-one encoding employs orthogonal splitting gadgets to enforce lattice operations. Both constructions yield polynomial-size systems of quadratic equations, establishing membership in ∃Rand hence in PSPACE through Canny’s algorithm [4]. Second, we provide precise complexity bounds that distinguish weak and strong satisfiability through their witness structures: weak satisfiability requires O(N∨D)witness scalars while strong satisfiability demands O(N∨D2)due to the necessity of verifying the full-space condition across all basis vectors. Third, we present complete proofs of all typing and well-formedness lemmas, ensuring that all operations respect the subspace lattice structure and that encodings faithfully represent quantum logic semantics. The paper is structured as follows. Section 2 establishes preliminaries including the subspace semantics, orthogonal projectors, and the BSS computational model. Section 3 presents the main classification theorem. Section 4 develops the realification-based ETR reduction with detailed treatment of complex-to-real translation. Section 5 provides the alternative rank-one encoding approach. Section 6 synthesizes the complexity classification results. Section 7 discusses open problems and connections to broader questions in algebraic complexity theory. 2 Preliminaries Throughout we fix a finite-dimensional Hilbert space Hof dimension d≥1over Ror C. We denote by L(H)the set of closed subspaces of Hordered by inclusion. For subspaces U, V ∈ L(H), we write U≤Vwhen U⊆V,U⊥for the orthogonal complement, U∩Vfor the intersection, and U+Vfor the algebraic sum, which equals the closed linear span in finite dimension. Definition 2.1 (Subspace valuation and semantics).Avaluation is a map vassigning to each propositional variable pia subspace v(pi)∈ L(H). For a formula ϕbuilt from propositional 2 variables and connectives ∧,∨,¬, we define v(ϕ)∈ L(H)inductively by v(¬ψ) = v(ψ)⊥, v(ψ∧χ) = v(ψ)∩v(χ), v(ψ∨χ) = v(ψ) + v(χ). A valuation weakly satisfies ϕif v(ϕ)6={0}and strongly satisfies ϕif v(ϕ) = H. Lemma 2.2 (Well-formedness of operations).Let Hbe a real or complex inner product space and let U, V ≤Hbe linear subspaces. Then U⊥,U∩V, and U+Vare linear subspaces of H. Proof. We verify linearity in each case. First, U⊥is a linear subspace. Clearly 0∈U⊥because h0, ui= 0 for all u∈U. If x, y ∈U⊥ and α, β ∈F(where Fis Ror C), then for every u∈Uwe have hαx +βy, ui=αhx, ui+βhy, ui= 0, since hx, ui=hy, ui= 0. Thus αx +βy ∈U⊥. Next, U∩Vis a linear subspace. If x, y ∈U∩Vand α, β ∈F, then x, y ∈Uand x, y ∈V, hence αx +βy ∈Uand αx +βy ∈Vbecause Uand Vare linear subspaces. Therefore αx +βy ∈U∩V. Finally, U+V:= {u+v:u∈U, v ∈V}is a linear subspace. We have 0 = 0 + 0 ∈U+V. If x=u1+v1and y=u2+v2with ui∈Uand vi∈Vand if α, β ∈F, then αx +βy =α(u1+v1) + β(u2+v2) = (αu1+βu2)+(αv1+βv2), and αu1+βu2∈U,αv1+βv2∈Vbecause Uand Vare linear subspaces. Hence αx +βy ∈U+V. Thus all three sets U⊥,U∩V, and U+Vare linear subspaces of H. Lemma 2.3 (Orthogonal projectors in finite dimension).Let Hbe a finite-dimensional real or complex Hilbert space and U≤Ha subspace. (a) There exists a unique orthogonal projector PUonto U; moreover PU⊥= Id −PU. (b) A linear operator P:H→Hsatisfies P∗=Pand P2=Pif and only if Pis the orthogonal projector onto Ran(P); in particular Ker(P) = Ran(P)⊥. (c) For all x∈H, one has x∈Uif and only if PUx=x, and x∈U⊥if and only if PUx= 0. Proof. We fix the convention that the inner product is linear in its first argument and conjugatelinear in its second; in (b), P∗denotes the adjoint. (a) Existence, orthogonality, self-adjointness, idempotence, then uniqueness, and finally PU⊥= Id −PU.Choose a basis (u1, . . . , uk)of Uand apply Gram–Schmidt: e1=u1 ku1k, vi:= ui− i−1 X j=1 hui, ejiej, ei=vi kvik(2 ≤i≤k). Since span(e1, . . . , ei−1) = span(u1, . . . , ui−1)and (u1, . . . , ui)is linearly independent, each vi6= 0; hence (e1, . . . , ek)is an orthonormal basis of U. 3 Define PU:H→Hby the explicit rule PUx= k X i=1 hx, eiiei(x∈H). Then PUis linear, PUx∈Ufor all x, and for u=Pk i=1 αiei∈U, PUu= k X i=1 hu, eiiei= k X i=1 αiei=u, so Ran(PU) = U. For orthogonality, compute for each i: hx−PUx, eii=hx, eii − Dk X j=1 hx, ejiej, eiE=hx, eii − k X j=1 hx, ejihej, eii= 0. Hence for any u=Pk i=1 αiei∈U, hx−PUx, ui= k X i=1 αihx−PUx, eii= 0 (using conjugate-linearity in the second argument), and therefore x−PUx∈U⊥. Idempotence and self-adjointness are explicit: P2 Ux= k X i=1 hPUx, eiiei= k X i=1 hx, eiiei=PUx, hPUx, yi=Dk X i=1 hx, eiiei, yE= k X i=1 hx, eii hei, yi, hx, PUyi=Dx, k X i=1 hy, eiieiE= k X i=1 hy, eii hx, eii= k X i=1 hei, yi hx, eii, so hPUx, yi=hx, PUyiand PU=P∗ U. Moreover, ker(PU) = U⊥(both directions): (z∈U⊥⇒ hz, eii= 0 ∀i⇒PUz= 0, PUx= 0 ⇒x=x−PUx∈U⊥. Uniqueness. Let Q:H→Hbe any orthogonal projector onto U, i.e. Qx ∈Uand x−Qx ∈U⊥ for all x. Fix xand set u:= PUx∈U, v := x−PUx∈U⊥. First, u−Qu ∈U⊥and u−Qu ∈U, hence u−Qu = 0; thus Q(PUx) = PUx. Second, Qv ∈Uand v−Qv ∈U⊥by definition of Q, while v∈U⊥by construction; since U⊥is a linear subspace, Qv =v−(v−Qv)∈U⊥. 4 Therefore Qv ∈U∩U⊥={0}, so Q(x−PUx) = 0. Consequently, Qx =Q(PUx) + Q(x−PUx) = PUx, and Q=PU. Finally, set Q:= Id −PU. Then Q∗=Qand Q2=Q. For any x,Qx =x−PUx∈U⊥, so Ran(Q)⊆U⊥; conversely, if z∈U⊥, then PUz= 0 and Qz =z, hence Ran(Q) = U⊥. Moreover, ker(Q) = Ubecause Qu = 0 for u∈Uand Qx = 0 implies x=PUx∈U. Thus Qis the orthogonal projector onto U⊥; by the uniqueness just proved (applied to U⊥), Q=PU⊥, i.e. PU⊥= Id −PU. (b) Characterization of self-adjoint idempotents. (⇒) Assume P∗=Pand P2=P. If z∈ker(P)and y=Pw ∈Ran(P), then hz, yi=hz, P wi=hP∗z, wi=hP z, wi= 0, so ker(P)⊆Ran(P)⊥. Conversely, if x∈Ran(P)⊥, then P Px ∈Ran(P)and 0 = hx, P P xi=hP∗x, P xi=hPx, Pxi, whence Px = 0 and x∈ker(P). Therefore ker(P) = Ran(P)⊥. Now for any x, x=Px + (Id −P)x, P (Id −P) = 0 ⇒(Id −P)x∈ker(P) = Ran(P)⊥. Since Px ∈Ran(P), this is the orthogonal decomposition of xinto Ran(P)⊕Ran(P)⊥. As Pis the identity on Ran(P)and zero on Ran(P)⊥,Pis the orthogonal projector onto Ran(P). (⇐) If Pis the orthogonal projector onto W≤H, then for x=w+zand y=w0+z0with w, w0∈Wand z, z0∈W⊥we have Px =wand hence P2x=P(P x) = P w =w=P x; moreover hPx, yi=hw, w0+z0i=hw, w0i=hw+z, w0i=hx, P yi, so P∗=Pand ker(P) = W⊥= Ran(P)⊥. (c) Fixed points and zeros. From (a), Ran(PU) = Uand ker(PU) = U⊥. Hence PUx=x⇐⇒ x∈U, PUx= 0 ⇐⇒ x∈U⊥. This completes the proof. Lemma 2.4 (De Morgan rules and involution).For subspaces U, V ≤H, (U+V)⊥=U⊥∩V⊥,(U∩V)⊥=U⊥+V⊥. Moreover, (·)⊥is an order-reversing involution: (U⊥)⊥=Uand U⊆V⇒V⊥⊆U⊥. Proof. We work in finite dimension, so orthogonal complements yield direct sums and closures are unnecessary. (Order-reversing). If U⊆Vand x∈V⊥, then hx, ui= 0 for all u∈U, hence x∈U⊥; thus V⊥⊆U⊥. (First De Morgan identity). For any x, x∈(U+V)⊥⇐⇒ hx, u +vi= 0 ∀u∈U, v ∈V⇐⇒ hx, ui=hx, vi= 0 ⇐⇒ x∈U⊥∩V⊥. 5 (Involutivity). By Lemma 2.3, there is an orthogonal projector PUonto Uwith ker(PU) = U⊥ and Ran(PU) = U, hence H=U⊕U⊥. The inclusion U⊆(U⊥)⊥is immediate. Conversely, if x∈(U⊥)⊥, write x=u+zwith u∈U,z∈U⊥; then 0 = hx, zi=hu, zi+hz, zi=kzk2, so z= 0 and x=u∈U. Therefore (U⊥)⊥=U. (Second De Morgan identity). Apply the first identity to U⊥and V⊥: (U⊥+V⊥)⊥=U⊥⊥ ∩V⊥⊥ =U∩V. Taking orthogonal complements of both sides and using (·)⊥⊥ = Id in finite dimension yields (U∩V)⊥= (U⊥+V⊥)⊥⊥ =U⊥+V⊥. Lemma 2.5 (Negation normal form).Every formula ϕis equivalent under the subspace semantics to a formula φin negation normal form (NNF), where negations appear only on atomic propositions. The translation is linear in |ϕ|. Proof. Apply Lemma 2.4 recursively to push negations inward and use involutivity (U⊥)⊥=Uto eliminate double negations. 2.1 Blum–Shub–Smale computation Blum, Shub, and Smale [2] introduced a model of computation over the reals in which a machine can store and operate on real numbers exactly, with arithmetic operations and comparisons as unit-cost primitives. The class NPRconsists of decision problems solvable by a nondeterministic BSS machine in time polynomial in the input size. The existential theory of the reals, denoted ∃R, asks whether a given Boolean combination of polynomial equations and inequalities over real variables has a solution. This problem is complete for NPR. In the classical Turing model, Canny [4] showed that ∃Rlies in PSPACE, establishing a crucial bridge between algebraic and discrete complexity. Definition 2.6 (4-FEASIBILITY in the BSS model).Given a finite family of real polynomials F= (f1, . . . , fk)with fi∈R[X1, . . . , Xm]and maxideg fi≤4, decide whether there exists x∈Rm such that F(x) = 0 i.e., f1(x) = · · · =fk(x) = 0. Equivalently, given a polynomial map F:Rm→Rkof degree at most 4, decide whether 0∈F(Rm). Proposition 2.7 (BSS completeness of 4-FEASIBILITY).In the BSS model over R, 4-FEASIBILITY is NPR-complete [2,3]. 6 3 Main Results Theorem 3.1 (Fixed-dimension complexity classification).Let Hbe a finite-dimensional real or complex Hilbert space. Then: (1) If dim(H) = 1, weak and strong satisfiability coincide with Boolean satisfiability and are NP-complete. (2) If dim(H) = 2, both weak and strong satisfiability are NP-complete [1]. (3) If dim(H) = d≥3is fixed, both weak and strong satisfiability are NPR-complete [1]. (4) For every fixed d≥1, both weak and strong satisfiability many-one reduce in polynomial time to the Existential Theory of the Reals (ETR), hence lie in ∃R. Since ETR is in PSPACE [4], both problems are in PSPACE. (5) If dis part of the input, strong satisfiability is polynomial-time equivalent to feasibility of non-commutative integer polynomial equations [1]. The proof of Theorem 3.1 combines results from Herrmann–Ziegler [1] with our constructive ETR reductions developed in Sections 4 and 5. Item (4) constitutes our principal technical contribution and will be established through two independent approaches. 4 Realification-Based ETR Reduction We now develop the first constructive reduction to ETR, based on explicit realification of complex Hilbert spaces. This approach provides detailed control over the complex-to-real translation and yields precise complexity bounds. 4.1 Realification for vectors, matrices, and subspaces Definition 4.1 (Realification).Identify Cdwith R2dvia the map R:Cd→R2ddefined by R(x) = (<x, =x). Let J=0−Id Id0∈R2d×2d. For a complex matrix C=A+iB ∈Cd×dwith A, B ∈Rd×d, define R(C) = A−B B A ∈R2d×2d. For a complex subspace U≤Cd, define R(U) := {R(u) : u∈U} ≤ R2d. Lemma 4.2 (Basic properties of realification).Let C=A+iB ∈Cd×dwith A, B ∈Rd×d, and let R(C) = A−B B A, J =0−Id Id0. For every x∈Cdand C, D ∈Cd×dthe following hold: 7 (a) Ris R–linear and satisfies R(Cx) = R(C)R(x). (b) R(CD) = R(C)R(D)and R(C+D) = R(C) + R(D). (c) Every R(C)commutes with J. (d) Cis Hermitian iff R(C)is symmetric, and C2=Ciff R(C)2=R(C). Proof. Write x=u+iv with u, v ∈Rd. Then R(x) = u v. (a) Real-linearity and compatibility with multiplication. Since Racts by R(α+iβ) = (α, β) coordinatewise, it is R–linear. Moreover, R(C)R(x) = A−B B A u v=Au −Bv Bu +Av=R(A+iB)(u+iv)=R(Cx). (b) Compatibility with matrix addition and multiplication. Block multiplication gives R(C)R(D) = A−B B A A0−B0 B0A0=AA0−BB0−(AB0+BA0) AB0+BA0AA0−BB0=R((A+iB)(A0+iB0)) = R(CD). Addition is componentwise and immediate. (c) R(C)commutes with J.Compute R(C)J=A−B B A 0−Id Id0=−B−A A−B, JR(C) = 0−Id Id0A−B B A =−B−A A−B. Thus R(C)J=JR(C). (d) Hermitian ⇐⇒ symmetric; idempotent ⇐⇒ idempotent. Hermitian case. We have C∗=AT−iBT. Thus C∗=Ciff AT=A, BT=−B. But R(C)T=ATBT −BTAT, which equals R(C)exactly when the same two conditions hold. Hence Cis Hermitian iff R(C)is symmetric. Idempotent case. From (b), R(C)2=R(C)R(C) = R(C2). Thus C2=C⇐⇒ R(C2) = R(C)⇐⇒ R(C)2=R(C), since Ris injective on Cd×d. This completes the proof. 8 Lemma 4.3 (Commutant characterization).A matrix P∈R2d×2dsatisfies PJ =JP if and only if P=A−B B A =R(A+iB) for unique A, B ∈Rd×d. Moreover, under the assumption P J =JP and with this decomposition P=R(A+iB), the matrix Pis symmetric if and only if AT=Aand BT=−B, and Pis idempotent if and only if (A+iB)2=A+iB. Proof. Let J:= 0−Id Id0. (⇒) Write P=X Y Z W with d×dblocks. Then PJ =X Y Z W0−Id Id0=Y−X W−Z, JP =0−Id Id0X Y Z W=−Z−W X Y . Hence PJ =JP if and only if Y=−Zand W=X. Consequently P=X Y Z W=X−Z Z X . Setting A:= Xand B:= Zyields P=A−B B A =R(A+iB). Uniqueness of A, B is immediate from the identification Awith the (1,1)-block and Bwith the (2,1)-block of P. (⇐) Conversely, for any A, B ∈Rd×d, A−B B A 0−Id Id0=−B−A A−B=0−Id Id0A−B B A , so such Pcommute with J. For symmetry, compute A−B B A T =ATBT −BTAT. Thus PT=Pif and only if AT=Aand BT=−B. For idempotency, multiply blocks: A−B B A 2 =A2−B2−(AB +BA) AB +BA A2−B2. Hence P2=Pif and only if A2−B2=A, AB +BA =B, which is equivalent to (A+iB)2= (A2−B2) + i(AB +BA) = A+iB. This proves all claims. 9 Lemma 4.9 (Realification and subspace semantics).Let d≥1and D:= 2d. For orthogonal projectors Qion Cddefine vC(pi) := Ran(Qi)⊆Cd, vC(¬pi) := vC(pi)⊥, vC(ψ∧χ) := vC(ψ)∩vC(χ), vC(ψ∨χ) := vC(ψ)+vC(χ). Let Pi:= R(Qi)and define vRexactly as in Theorem 4.8. Then for every NNF formula φand every u∈Cdwe have u∈vC(φ)⇐⇒ R(u)∈vR(φ), equivalently, vR(φ) = R(vC(φ)). Proof. We prove by structural induction on NNF formulas that vR(φ) = R(vC(φ)). Base case 1: φ=pi.Since Pi=R(Qi), Lemma 4.4 gives Ran(Pi) = R(Ran(Qi)). Thus vR(pi) = Ran(Pi) = R(Ran(Qi)) = R(vC(pi)). Base case 2: φ=¬pi.By definition and Lemma 4.5, vR(¬pi) = vR(pi)⊥=R(vC(pi))⊥=R(vC(pi)⊥) = R(vC(¬pi)). Inductive step 1: φ=ψ∧χ.Induction gives vR(ψ) = R(vC(ψ)) and vR(χ) = R(vC(χ)). Hence vR(ψ∧χ) = vR(ψ)∩vR(χ) = R(vC(ψ)) ∩ R(vC(χ)) = R(vC(ψ)∩vC(χ)) = R(vC(ψ∧χ)), using Lemma 4.5. Inductive step 2: φ=ψ∨χ.Similarly, vR(ψ∨χ) = vR(ψ) + vR(χ) = R(vC(ψ)) + R(vC(χ)) = R(vC(ψ) + vC(χ)) = R(vC(ψ∨χ)). Thus for all NNF formulas φ, vR(φ) = R(vC(φ)). Membership equivalence. Since R:Cd→R2dis a real-linear isomorphism, u∈vC(φ)⇐⇒ R(u)∈ R(vC(φ)) = vR(φ). This completes the proof. 16 4.3 ETR reduction with weak/strong size bounds Lemma 4.10 (ETR reduction for fixed dimension).Fix d≥1. In the real case set D=d; in the complex case set D= 2dand additionally require PiJ=JPi(1 ≤i≤n). From any input formula ϕ, one can compute in time O(d2· |ϕ|)an existential sentence over Rthat is true if and only if ϕis strongly (respectively weakly) satisfiable in Hof dimension d. Moreover, let nbe the number of distinct atoms, N∨the number of ∨–occurrences, and let |φ| denote the length of the NNF (number of connectives plus literal occurrences). Then the number of scalar unknowns is Weak satisfiability: O(nD2+N∨D), Strong satisfiability: O(nD2+N∨D2). The number of equations can be bounded by Weak satisfiability: O(nD2+|φ|D), Strong satisfiability: O(nD2+|φ|D2), and all equations have degree at most 2. Proof. Step 1: Normal form. Translate ϕinto negation normal form φ= NNF(ϕ)using Lemma 2.5. This takes O(|ϕ|)time and yields |φ|=O(|ϕ|). Let nbe the number of distinct atoms and N∨the number of ∨–occurrences in φ. Step 2: Projector variables. For each atom pi, introduce a matrix variable Pi∈RD×Dwith constraints PT i=Pi, P2 i=Pi, and, in the complex case, the commutation condition PiJ=JPi. By Lemma 2.3, the real constraints make Pia real orthogonal projector. By Lemma 4.4, the additional commutation constraint forces Pi=R(Qi)for a unique complex orthogonal projector Qi. Thus in both cases Pisemantically represents a valid valuation component. The projector part introduces nD2scalar variables and O(nD2)polynomial constraints (linear and quadratic). Step 3: Encoding the semantics. The real encoding EncR(φ, x)(Definition 4.7) uses only the atomic clauses Pix=x, Pix= 0, x =y+z, and for each ∨–occurrence fresh witness variables yψ,χ, zψ,χ. Expanding EncRand lifting all existential witnesses to the global prefix produces a single existential R–sentence whose matrix entries and vector coordinates are all explicitly quantified. By Theorem 4.8, for every real vector x, EncR(φ, x)is satisfiable ⇐⇒ x∈vR(φ). In the complex case, Lemma 4.9 additionally guarantees u∈vC(φ)⇐⇒ R(u)∈vR(φ), 17 so the real encoding is semantically faithful to the complex semantics. Step 4: Strong satisfiability. Strong satisfiability requires v(φ) = H=RD(real case) or H=Cd(complex case). By Lemma 4.6 and Lemma 4.9 this holds iff EncR(φ, ej)is satisfiable for all 1≤j≤D. Thus we impose D ^ j=1 EncR(φ, ej). Size. Each disjunction produces two D–dimensional witness vectors per basis vector ej. Hence the number of witness vectors is 2N∨D, i.e. O(N∨D2)scalar variables. Each witness participates in O(1) linear equations of the form x=y+zand O(1) quadratic equations of the form Piy=yor Piy= 0. Thus strong satisfiability requires O(nD2+N∨D2) scalar variables and equations. Step 5: Weak satisfiability. Weak satisfiability requires v(φ)6={0}. Introduce x∈RDwith the quadratic constraint kxk2= 1, and impose EncR(φ, x). By Theorem 4.8, this is satisfiable iff v(φ)6={0}. Size. Now each disjunction contributes only two witness vectors (no basis-vector expansion). Thus the witness part contributes O(N∨D)scalar variables and equations. Together with the projector part: O(nD2+N∨D). Step 6: Polynomial degree. All constraints are polynomial equations in the matrix entries of the Piand the coordinates of all witness vectors: • Linear: PT i=Pi,PiJ=JPi,x=y+z. • Quadratic: P2 i=Pi,kxk2= 1, and all clauses of the form Pix=xor Pix= 0. Thus every constraint has degree ≤2. Step 7: Construction time. Let |φ|=O(|ϕ|). Since n, N∨≤ |φ|, we have n, N∨=O(|ϕ|). The construction cost is dominated by the number of scalar variables and equations produced: weak: O(nD2+N∨D) = O(D2|ϕ|),strong: O(nD2+N∨D2) = O(D2|ϕ|). Because D=din the real case and D= 2din the complex case, both cases yield total running time O(D2|ϕ|) = O(d2|ϕ|). This proves the lemma. 18 5 Alternative Reduction: Rank-One Column Encoding 5.1 Rank-one block encoding (quadratic-only, with atom sharing) Fix D≥1and identify H≃RDwith the standard inner product. For each label X(a subformula or an auxiliary block), introduce a matrix VX= [vX 1· · · vX D]∈RD×Dwhose columns vX i∈RD, together with selector variables tX i∈R(i= 1, . . . , D). Impose: (R1) (column orthogonality) (vX i)TvX j= 0 (i6=j), (R2) (norm equals selector) (vX i)TvX i=tX i, (R3) (Booleanity) (tX i)2=tX i, (R4) (selector enforcement) tX ivX i=vX i. Define the block projection PX:= VX(VX)T= D X i=1 vX i(vX i)T. Lemma 5.1 (Rank-one blocks yield projections).Under (R1)–(R4),PXis an orthogonal projection and im(PX) = span{vX i:tX i= 1 }. Proof. From (R1)–(R2),(VX)TVX= diag(tX 1, . . . , tX D). By (R3)–(R4),tX i∈ {0,1}and tX ivX i=vX i, hence VXdiag(t) = VX. Then (PX)2=VX(VX)TVX(VX)T=VXdiag(t)(VX)T=VX(VX)T= PX, and PXis symmetric by construction. The image description follows from orthogonality and the unit/zero norm enforced by (R2)–(R4). 5.2 Rank-one block encoding Fix d≥1and identify Hwith Rdendowed with the standard inner product hx, yi=xTy. For each label X(representing a subformula or auxiliary frame), introduce a matrix VX= [vX 1· · · vX d]∈ Rd×dwhose columns are vX i∈Rd, together with selector variables tX i∈Rfor i= 1, . . . , d. Impose the constraints: (R1) (vX i)TvX j= 0 for all i6=j(orthogonality), (R2) (vX i)TvX i=tX ifor all i(squared norms), (R3) (tX i)2=tX ifor all i(Boolean selectors), (R4) tX ivX i=vX ifor all i(selector enforcement). Define the projection matrix PX:= VX(VX)T= d X i=1 vX i(vX i)T. 19 5.3 Binary connective gadgets (quadratic orthogonal splitting) For each binary node σwith children τ, ρ, introduce three blocks Wσ, Aσ, Bσeach satisfying (R1)–(R4), and impose the orthogonal splitting constraints (VWσ)TVAσ= 0,(VWσ)TVBσ= 0,(VAσ)TVBσ= 0.(5.1) These are quadratic and ensure that PWσPAσ=PWσPBσ=PAσPBσ= 0. Construction specification. C1. Atom sharing. For each distinct atom pi, introduce a single global block (Vpi, tpi)with Ppi:= Vpi(Vpi)T. For every atomic node σlabelled pi,do not create a fresh block; instead impose Pσ=Ppi(entrywise equality). C2. Projections for compound subformulas. For each non-atomic subformula σ, introduce a block Vσ(with Pσ:= Vσ(Vσ)T) plus the auxiliary blocks Wσ, Aσ, Bσused below. All these blocks satisfy (R1)–(R4). C3. Negation. If σ=¬τ, impose Pσ=I−Pτ. C4. Conjunction. If σ=τ∧ρ, impose Pτ=PWσ+PAσ, Pρ=PWσ+PBσ, Pσ=PWσ,(5.2) together with (5.1). C5. Disjunction. If σ=τ∨ρ, impose Pτ=PWσ+PAσ, Pρ=PWσ+PBσ, Pσ=PWσ+PAσ+PBσ,(5.3) together with (5.1). C6. Root condition. For strong satisfiability of the root formula ϕ, enforce Pϕej=ejfor all standard basis vectors ej,j= 1, . . . , D. For weak satisfiability, introduce x∈RDwith xTx= 1 and impose Pϕx=x. Proposition 5.2 (Correctness of rank-one encoding (commuting-projector semantics)).Let H≃ RDand let ϕbe in NNF. Let Eϕbe the conjunction of all instances of (R1)–(R4),(5.1), and C1–C6 above (including atom sharing). We say that ϕis commuting-algebraically satisfiable over Hif there exists a family of orthogonal projections (e Pσ)σon Hsuch that for every binary node with children τ, ρ, the projections e Pτand e Pρcommute and e P¬τ=I−e Pτ,e Pτ∧ρ=e Pτe Pρ,e Pτ∨ρ=e Pτ+e Pρ−e Pτe Pρ. At the root, require e Pϕ=I(strong) or e Pϕ6= 0 (weak). Then Eϕhas a real solution if and only if ϕis commuting-algebraically satisfiable over H (strong/weak respectively). 20 Proof. (Solution ⇒satisfiable) By Lemma 5.1, every block PXis an orthogonal projection. Quadratic orthogonality (5.1) yields PWσPAσ=PWσPBσ=PAσPBσ= 0, so the sums in (5.2)–(5.3) are projections and PτPρ=PWσ=Pσ, PρPτ=PWσ=Pσ, Pτ+Pρ−PτPρ=PWσ+PAσ+PBσ=Pσ. Thus setting e Pσ:= Pσgives the required commuting family and the root clause holds by C6. (Satisfiable ⇒solution) Given a commuting-algebraic model (e Pσ)σ, define PWσ:= e Pτe Pρ, PAσ:= e Pτ(I−e Pρ), PBσ:= (I−e Pτ)e Pρ. Since e Pτand e Pρcommute, each of PWσ,PAσ,PBσis an orthogonal projection and their pairwise products vanish. Choose orthonormal bases of their images to form VWσ, V Aσ, V Bσ; set t= 1 for used columns and 0otherwise to satisfy (R1)–(R4). For each non-atomic σtake Vσfor Pσ analogously; for atoms use the global (Vpi, tpi)and impose Pσ=Ppi(atom sharing). All constraints in C1–C6 follow, including the root clause. Corollary 5.3 (Alternative PSPACE upper bound (rank-one encoding; commuting projectors)). For fixed D≥1, both weak and strong satisfiability under the commuting-projector semantics reduce to ETR via the quadratic rank-one encoding of Section 5, and hence lie in PSPACE. Proof. By Proposition 5.2, the constraint system Eϕconstructed in Section 5 (with atom sharing for each distinct pi, the block constraints (R1)–(R4), and the quadratic orthogonal-splitting constraints (VWσ)TVAσ= (VWσ)TVBσ= (VAσ)TVBσ= 0) has a real solution if and only if ϕis (weakly/strongly) satisfiable under the commuting-projector semantics. All constraints in Eϕare polynomial equations of degree at most 2:(R1)–(R4) are linear/quadratic, the orthogonal-splitting equations are quadratic, the identities Pσ=I−Pτ,Pσ=PXPX σare linear in entries, and the root clauses are linear (Pϕej=ejfor strong) or quadratic+linear (xTx= 1, Pϕx=xfor weak). The construction introduces one global atomic block per distinct atom and O(1) auxiliary blocks per binary connective, hence O(|ϕ|)blocks in total. Each block contributes O(D2)scalar variables and O(D2)equations; therefore, for fixed D, the resulting existential sentence over Rhas size polynomial in |ϕ|. ETR lies in PSPACE by Canny [4], so both variants lie in PSPACE. (For the standard subspace semantics, the PSPACE upper bound already follows from Lemma 4.10; the present corollary provides an alternative via the rank-one encoding under commuting-projector semantics.) 6 Proof of Main Theorem We now synthesize the results to establish Theorem 3.1. Proposition 6.1 (Dimension one).If dim(H)=1, weak and strong satisfiability coincide with Boolean satisfiability and are NP-complete. Proof. When dim(H)=1, the only proper subspaces are {0}and H. Identify {0}with Boolean False and Hwith True. Under this identification, ∧,∨,¬coincide with Boolean ∧,∨,¬, so satisfiability reduces to propositional SAT. NP-hardness follows from the identity reduction on formulas; NP membership is immediate. 21 Proposition 6.2 (Dimension two).If dim(H) = 2, both weak and strong satisfiability are NPcomplete. Proof. Herrmann and Ziegler [1] established this through explicit reductions between Boolean SAT and quantum logic satisfiability in dimension two, exploiting the special structure of onedimensional subspaces in C2. Proposition 6.3 (Fixed dimension d≥3).For fixed d≥3, both weak and strong satisfiability are NPR-complete. Proof. Membership. A nondeterministic BSS machine guesses all entries of the orthogonal projectors Piand the witness vectors (one unit vector for weak, all dbasis vectors for strong) and verifies the polynomial equalities in polynomial time. Hence both problems lie in NPR. Hardness. By Herrmann and Ziegler [1], any constant-degree real feasibility instance reduces in polynomial time to quantum logic satisfiability. In particular, 4-FEASIBILITY (Definition 2.6), which is NPR-complete by Blum–Shub–Smale [2,3], reduces to satisfiability. Therefore both weak and strong satisfiability are NPR-hard, hence complete. Proposition 6.4 (PSPACE upper bound).For every fixed d≥1, both weak and strong satisfiability many-one reduce to ETR, hence lie in ∃Rand in PSPACE. Proof. Combine Lemma 4.10 (realification-based reduction) or Corollary 5.3 (rank-one encoding) with Canny’s PSPACE algorithm for ETR [4]. Proposition 6.5 (Unbounded dimension).If dis part of the input, strong satisfiability is polynomialtime equivalent to feasibility of non-commutative integer polynomial equations. Proof. Herrmann and Ziegler [1] provide polynomial-time reductions in both directions between strong satisfiability in indefinite dimension and the problem of deciding whether non-commutative polynomials over integer variables have a solution in some matrix algebra. Proof of Theorem 3.1.Combine Propositions 6.1,6.2,6.3,6.4, and 6.5. 7 Discussion The classification established in Theorem 3.1 places quantum logic satisfiability in a precise complexitytheoretic position between classical NP and the existential theory of the reals. In fixed dimension d≥3, the problem achieves NPR-completeness and thus stands outside classical NP under reasonable complexity-theoretic assumptions. Yet both ETR reductions developed in this paper demonstrate membership in ∃R, yielding a PSPACE upper bound in the Turing model via Canny’s algorithm. Whether this upper bound is tight remains a central open question. The distinction between weak and strong satisfiability, while semantically natural, proves inessential for complexity classification: both variants achieve the same complexity in each fixed dimension. Nevertheless, our size analysis in Lemma 4.10 reveals a quadratic separation in the encoding complexity. Weak satisfiability requires O(N∨D)witness scalars for disjunction handling, while strong satisfiability demands O(N∨D2)scalars due to the necessity of verifying the full-space condition through all basis vectors. This separation becomes pronounced in formulas with extensive disjunctive structure. 22 The realification-based and rank-one encodings offer complementary perspectives on the reduction structure. The realification approach provides explicit control over complex-to-real translation through commutant characterizations and benefits from the clean algebraic properties of the realification functor. The rank-one encoding emphasizes the geometric decomposition of subspace lattice operations through orthogonal splittings and may prove more amenable to generalization to infinite-dimensional settings or non-standard logics. 7.1 Open problems Several questions emerge naturally from this work: 1. PSPACE-hardness in fixed dimension. Can quantum logic satisfiability for some fixed d≥3be shown PSPACE-hard in the Turing model? Such a result would establish the tightness of our upper bound. The difficulty lies in encoding PSPACE-complete problems such as quantified Boolean formulas into the subspace lattice structure with bounded dimension. 2. Weak satisfiability in unbounded dimension. While strong satisfiability in indefinite dimension reduces to non-commutative polynomial feasibility, the complexity of weak satisfiability when dis part of the input remains unclassified. Does it also achieve polynomial-time equivalence with this algebraic problem, or does it occupy an intermediate position? 3. Quantified quantum logic. What is the complexity of deciding formulas with quantifiers over propositional variables under the subspace semantics? In the classical Boolean setting, quantifier alternation leads to the polynomial hierarchy. The quantum case may exhibit richer structure due to the continuous nature of subspace choice. 4. Fine-grained complexity. Can the O(d2· |ϕ|)time bound for constructing the ETR reduction be improved? Are there lower bounds on the size of any ETR encoding, potentially establishing optimality of our constructions? 5. Approximate satisfiability. In dimension d≥3, exact strong satisfiability requires v(ϕ) = H. What is the complexity of deciding whether there exists a valuation with dim(v(ϕ)) ≥αd for some threshold α∈(0,1)? Such approximate notions may connect to quantum circuit complexity and quantum algorithm analysis. These questions intersect with broader themes in algebraic complexity, the compendium of ∃Rcomplete problems [5], and the foundations of quantum logic. Resolution of these problems would deepen our understanding of the computational structure of quantum-mechanical propositions and their classical representations. 8 Conclusion We have provided a comprehensive complexity analysis of quantum propositional logic satisfiability, distinguishing weak and strong semantics and establishing precise complexity bounds in all dimensional regimes. Through two independent constructive reductions to the Existential Theory of the Reals, we have proven that for every fixed dimension, both satisfiability variants lie in the complexity class ∃Rand hence in PSPACE. Our detailed size analysis reveals a quadratic separation 23 between weak and strong satisfiability in their witness requirements, underscoring the geometric complexity of the full-space condition. The main classification theorem positions quantum logic satisfiability between classical NP and ∃R, with dimension serving as the fundamental complexity parameter. In dimension one, we recover classical Boolean satisfiability and NP-completeness. In dimension two, we remain in NP through special structural properties. For dimension d≥3fixed, we achieve NPR-completeness in the BSS model, while maintaining PSPACE decidability in the Turing model. When dimension becomes part of the input, strong satisfiability transcends polynomial hierarchy and becomes equivalent to algebraic feasibility in non-commutative polynomial rings. Our work supplies the detailed technical foundations necessary for further investigation of quantum logic complexity and its connections to algebraic geometry, quantum computing, and the theory of real computation. The two reduction techniques developed here may prove valuable tools for analyzing related problems in quantum algebra and operator theory. The open questions identified in Section 7 suggest rich directions for future research at the intersection of logic, algebra, and computational complexity. References [1] C. Herrmann and M. Ziegler. Computational complexity of quantum satisfiability. Annals of Pure and Applied Logic, 163(12):1955–1982, 2012. [2] L. Blum, M. Shub, and S. Smale. On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal machines. Bulletin of the American Mathematical Society, 21(1):1–46, 1989. [3] L. Blum, F. Cucker, M. Shub, and S. Smale. Complexity and Real Computation. Springer, 1998. [4] J. F. Canny. Some algebraic and geometric computations in PSPACE. In Proceedings of the 20th Annual ACM Symposium on Theory of Computing (STOC), pages 460–467, 1988. [5] M. Schaefer, J. Cardinal, and T. Miltzow. The Existential Theory of the Reals as a Complexity Class: A Compendium. arXiv:2407.18006, 2024. [6] R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013. [7] F. Zhang, Matrix Theory: Basic Results and Techniques, 2nd ed., Springer, 2011. 24