TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Slater and symmetric occupation-number bases of the finite-dimensional permutation sectors

Statement

Slot convention. For $ℓ \geq 1$ , $S_{ℓ}$ acts on ${0, \dots, ℓ - 1}$ as in Permutation sector projections on the n-fold tensor power. On one-based tuple positions use $\hat{π} (k) : = 1 + π (k - 1)$ for $1 \leq k \leq ℓ$ . Conjugation by $k \mapsto k - 1$ gives $\hat{π σ} = \hat{π} \circ \hat{σ}$ and $\hat{π^{- 1}} = {\hat{π}}^{- 1}$ ; thus the supplier's tensor action becomes $U_{π} (v_{1} \otimes \dots \otimes v_{ℓ}) = v_{{\hat{π}}^{- 1} (1)} \otimes \dots \otimes v_{{\hat{π}}^{- 1} (ℓ)}$ . The parameters of $U_{π}$ and $sgn (π)$ remain canonical zero-based permutations.

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space of finite dimension $d \geq 1$ with orthonormal basis $(e_{1}, \dots, e_{d})$ (Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases). Let $n \geq 1$ , and let $H^{\otimes n}$ be the $n$ -fold completed tensor power with $H^{\otimes 0} : = C$ , $H^{\otimes 1} : = H$ and $H^{\otimes (k + 1)} : = H^{\otimes k} \hat{\otimes} H$ (Hilbert tensor construction: inner product, completion and product bases), and let $P_{\pm}^{(n)} \in B (H^{\otimes n})$ , $n \geq 1$ , be the permutation projections of Permutation sector projections on the n-fold tensor power. For a multi-index $i = (i_{1}, \dots, i_{n}) \in {1, \dots, d}^{n}$ write $e_{i} : = e_{i_{1}} \otimes \dots \otimes e_{i_{n}}, ∣ i ∣_{j} : = # {k : i_{k} = j} (j = 1, \dots, d) .$ For $J \subseteq {1, \dots, d}$ with $∣ J ∣ = n$ , written $J = {j_{1} < \dots < j_{n}}$ , put $e_{J}^{\land} : = \frac{1}{\sqrt{n!}} \sum_{σ \in S_{n}} sgn (σ) e_{j_{\hat{σ} (1)}} \otimes \dots \otimes e_{j_{\hat{σ} (n)}},$ and for $λ \in W (n, d) : = {λ \in N^{d} : \sum_{j} λ_{j} = n}$ put $orb (λ) : = {c \in {1, \dots, d}^{n} : ∣ c ∣ = λ}$ and $m_{λ} : = \sum_{c \in orb (λ)} e_{c}$ . Then:

(a) product basis: $(e_{i})_{i \in {1, \dots, d}^{n}}$ is an orthonormal basis of $H^{\otimes n}$ , and $\dim H^{\otimes n} = d^{n}$ ;

(b) Slater basis: for every $J$ with $∣ J ∣ = n$ one has $e_{J}^{\land} = \sqrt{n!} P_{-}^{(n)} (e_{j_{1}} \otimes \dots \otimes e_{j_{n}})$ and the family $(e_{J}^{\land})_{J \subseteq {1, \dots, d}, ∣ J ∣ = n}$ is an orthonormal family whose closed linear span is $ran P_{-}^{(n)}$ ; it is therefore an orthonormal basis of $ran P_{-}^{(n)}$ , $\dim ran P_{-}^{(n)} = (\binom{d}{n})$ , and $ran P_{-}^{(n)} = {0}$ when $n > d$ . Moreover for every multi-index $i$ one has $P_{-}^{(n)} (e_{i}) = 0$ when two entries of $i$ coincide, and $P_{-}^{(n)} (e_{i}) = sgn (ρ_{i}) \frac{e_{J}^{\land}}{\sqrt{n!}}$ when the entries of $i$ are pairwise distinct with underlying set $J$ and $ρ_{i} \in S_{n}$ is the unique permutation with $i_{k} = j_{\hat{ρ_{i}} (k)}$ ;

(c) symmetric basis: for every $λ \in W (n, d)$ the vector $m_{λ}$ is nonzero, the family $(m_{λ})_{λ \in W (n, d)}$ is orthogonal, $U_{π} m_{λ} = m_{λ}$ for every $π \in S_{n}$ , and for every multi-index $i$ there is a real number $γ_{i} > 0$ with $P_{+}^{(n)} (e_{i}) = γ_{i} m_{∣ i ∣}$ ; consequently $ran P_{+}^{(n)}$ is the linear span of $(m_{λ})$ , the family $(m_{λ})$ is an orthogonal basis of $ran P_{+}^{(n)}$ , and $\dim ran P_{+}^{(n)} = (\binom{n + d - 1}{n})$ ;

(d) occupation operators: for $j \in {1, \dots, d}$ the map $N_{j} : H^{\otimes n} \to H^{\otimes n}, N_{j} x : = \sum_{i \in {1, \dots, d}^{n}} ∣ i ∣_{j} ⟨ x, e_{i} ⟩ e_{i},$ is a self-adjoint bounded endomorphism, the $N_{j}$ commute pairwise, $\sum_{j = 1}^{d} N_{j} = n I$ , and $N_{j} e_{J}^{\land} = 1_{J} (j) e_{J}^{\land}, N_{j} m_{λ} = λ_{j} m_{λ} .$ Consequently both sectors are invariant under every $N_{j}$ , the joint eigenspaces of $(N_{1}, \dots, N_{d})$ inside $ran P_{-}^{(n)}$ are the lines $C e_{J}^{\land}$ (one for each $n$ -element subset $J$ , with eigenvalue vector $1_{J}$ ), and the joint eigenspaces inside $ran P_{+}^{(n)}$ are the lines $C m_{λ}$ (one for each $λ \in W (n, d)$ , with eigenvalue vector $λ$ ).

Facts & Assumptions

Given: The finite-dimensional complex Hilbert space $H$ of dimension $d \geq 1$ with orthonormal basis $(e_{1}, \dots, e_{d})$ , the tensor powers $H^{\otimes n}$ with permutation projections $P_{\pm}^{(n)}$ , multi-indices $i \in {1, \dots, d}^{n}$ , subsets $J$ with $∣ J ∣ = n$ , and $λ \in W (n, d)$ .

[F1]

Tensor powers. For all $n$ the tensor power carries bilinear elementary tensors $v_{1} \otimes \dots \otimes v_{n}$ with $∥ v_{1} \otimes \dots \otimes v_{n} ∥ = ∥ v_{1} ∥ \dots ∥ v_{n} ∥$ and $⟨ v_{1} \otimes \dots \otimes v_{n}, w_{1} \otimes \dots \otimes w_{n} ⟩ = \prod_{k} ⟨ v_{k}, w_{k} ⟩$ ; for orthonormal families $(f_{a})_{a \in A}$ in $H$ and $(g_{b})_{b \in B}$ in $K$ with dense spans, the products $f_{a} \otimes g_{b}$ form an orthonormal family in $H \hat{\otimes} K$ with dense span; the algebraic tensor product is dense in each completion (Hilbert tensor construction: inner product, completion and product bases clauses (b)-(d)).

[F2]

Permutation projections. $U_{π} (v_{1} \otimes \dots \otimes v_{n}) = v_{{\hat{π}}^{- 1} (1)} \otimes \dots \otimes v_{{\hat{π}}^{- 1} (n)}$ defines unitaries with $U_{π} U_{σ} = U_{π σ}$ and $U_{π}^{*} = U_{π^{- 1}}$ ; $P_{+}^{(n)} = \frac{1}{n!} \sum_{π \in S_{n}} U_{π}$ and $P_{-}^{(n)} = \frac{1}{n!} \sum_{π \in S_{n}} sgn (π) U_{π}$ are orthogonal projections with $U_{π} P_{-}^{(n)} = P_{-}^{(n)} U_{π} = sgn (π) P_{-}^{(n)}$ , and $P_{-}^{(n)} (v_{1} \otimes \dots \otimes v_{n}) = 0$ whenever two of the vectors $v_{k}$ coincide (Permutation sector projections on the n-fold tensor power clauses (a),(c),(d)).

[F3]

Determinant. For a square matrix $A$ of size $n$ over a commutative ring, write $a_{a b} : = A (a - 1, b - 1)$ for $1 \leq a, b \leq n$ . Relabeling the zero-based Leibniz formula then gives $\det (A) = \sum_{σ \in S_{n}} sgn (σ) \prod_{a = 1}^{n} a_{\hat{σ} (a), a}$ ; in particular $\det (I_{n}) = 1$ , and $\det (A) = 0$ if some row of $A$ is zero (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[F4]

Binomial coefficients as counts. $(\binom{d}{k}) = ∣ [d]^{k} ∣$ for $d, k \in N$ , so with $k = n$ the number of $n$ -element subsets of ${1, \dots, d}$ is $(\binom{d}{n})$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[F5]

Weak compositions. For $m \geq 1$ and $n \in N$ , $∣ W (n, m) ∣ = (\binom{n + m - 1}{m - 1})$ (For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ ); and $(\binom{n + d - 1}{d - 1}) = (\binom{n + d - 1}{n})$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ clause 3, with $N = n + d - 1$ and $k = d - 1$ ).

[F6]

Orthonormal expansions. For an orthonormal family $(f_{a})_{a \in A}$ in a Hilbert space whose closed linear span is the whole space, every $x$ equals the limit of the finite partial sums $\sum_{a \in F} ⟨ x, f_{a} ⟩ f_{a}$ ; for a finite complete orthonormal family this is the finite equality $x = \sum_{a} ⟨ x, f_{a} ⟩ f_{a}$ (Parseval equivalences for an orthonormal family clauses 1 and 4, Orthonormal families, complete orthonormal systems and Hilbert bases).

[F7]

Self-adjointness and boundedness. A bounded endomorphism $T$ of $H^{\otimes n}$ is self-adjoint when $⟨ T x, y ⟩ = ⟨ x, T y ⟩$ for all $x, y$ , equivalently $T^{*} = T$ for the Hilbert adjoint of The Hilbert-space adjoint of a bounded operator (A bounded linear operator between normed spaces).

Proof

technique · direct; build the product basis by induction from the tensor construction, determine the two permutation projections on basis vectors by explicit reindexing sums, evaluate the resulting orthonormality as a determinant, read the dimension counts off the index sets, and compute the occupation operators on the two resulting bases

Given: The data of the statement and [F1]-[F7].

1.1F1algebrainduction

[Product basis] We show by induction on $n \geq 1$ that $(e_{i})_{i \in {1, \dots, d}^{n}}$ is an orthonormal basis of $H^{\otimes n}$ . For $n = 1$ this is the hypothesis. If it holds for $n$ , then by [F1] applied to the orthonormal basis $(e_{i})_{i \in {1, \dots, d}^{n}}$ of $H^{\otimes n}$ and $(e_{j})_{j \in {1, \dots, d}}$ of $H$ , the products $e_{i} \otimes e_{j}$ form an orthonormal family with dense span in $H^{\otimes (n + 1)} = H^{\otimes n} \hat{\otimes} H$ . This family is finite, indexed by $Q : = {1, \dots, d}^{n} \times {1, \dots, d}$ . Its span is closed: if $z_{r} = \sum_{q \in Q} c_{r, q} g_{q} \to z$ , where $g_{q}$ denotes the corresponding product vector, orthonormality gives $∥ z_{r} - z_{s} ∥^{2} = \sum_{q \in Q} ∣ c_{r, q} - c_{s, q} ∣^{2}$ , so each coefficient sequence is Cauchy. Let $c_{q}$ be its limit in $C$ ; the same finite norm identity gives $z_{r} \to \sum_{q \in Q} c_{q} g_{q}$ , hence $z = \sum_{q \in Q} c_{q} g_{q}$ lies in the span. Since the span is also dense, it equals the whole tensor product. Thus the family is an orthonormal basis, its cardinality is $d \cdot d^{n} = d^{n + 1}$ and $\dim H^{\otimes (n + 1)} = d^{n + 1}$ . This proves the induction step and (a).

1.2F2algebra

[The alternating projection on basis vectors] Let $i \in {1, \dots, d}^{n}$ . By the action formula of [F2], $P_{-}^{(n)} (e_{i}) = \frac{1}{n!} \sum_{π \in S_{n}} sgn (π) e_{i_{{\hat{π}}^{- 1} (1)}} \otimes \dots \otimes e_{i_{{\hat{π}}^{- 1} (n)}} = \frac{1}{n!} \sum_{τ \in S_{n}} sgn (τ) e_{i_{\hat{τ} (1)}} \otimes \dots \otimes e_{i_{\hat{τ} (n)}}$ after the substitution $τ = π^{- 1}$ . If two entries of $i$ coincide, say $i_{k} = i_{l}$ with $k \neq l$ , then the transposition $υ = (k - 1 l - 1)$ satisfies $e_{i_{\hat{υ τ} (1)}} \otimes \dots = e_{i_{\hat{τ} (1)}} \otimes \dots$ for every $τ$ and $sgn (υ τ) = - sgn (τ)$ , so the sum pairs to zero and $P_{-}^{(n)} (e_{i}) = 0$ by [F2]. If the entries are pairwise distinct with underlying set $J = {j_{1} < \dots < j_{n}}$ and $i_{k} = j_{\hat{ρ_{i}} (k)}$ , then $e_{i_{\hat{τ} (1)}} \otimes \dots = e_{j_{\hat{ρ_{i} τ} (1)}} \otimes \dots$ and $sgn (τ) = sgn (ρ_{i}) sgn (ρ_{i} τ)$ ; substituting $ω = ρ_{i} τ$ gives $P_{-}^{(n)} (e_{i}) = \frac{sgn (ρ_{i})}{n!} \sum_{ω \in S_{n}} sgn (ω) e_{j_{\hat{ω} (1)}} \otimes \dots \otimes e_{j_{\hat{ω} (n)}} = sgn (ρ_{i}) \frac{e_{J}^{\land}}{\sqrt{n!}}$ , which is the second formula of (b).

1.3F1F2F3algebra

[Orthonormality of the Slater family] For subsets $J, K$ with $∣ J ∣ = ∣ K ∣ = n$ let $A$ be the canonical matrix with $A (a - 1, b - 1) = ⟨ e_{j_{a}}, e_{k_{b}} ⟩ = δ_{j_{a}, k_{b}}$ , and abbreviate this entry as $A_{a b}$ for $1 \leq a, b \leq n$ . By [F1], $⟨ e_{J}^{\land}, e_{K}^{\land} ⟩ = \frac{1}{n!} \sum_{σ, π \in S_{n}} sgn (σ) sgn (π) \prod_{l = 1}^{n} A_{\hat{σ} (l), \hat{π} (l)}$ . For each fixed $π$ substitute $σ = ω π$ and reindex the product by $t = \hat{π} (l)$ . Then $\prod_{l} A_{\hat{σ} (l), \hat{π} (l)} = \prod_{t} A_{\hat{ω} (t), t}$ and $sgn (σ) sgn (π) = sgn (ω)$ , so the sum over $π$ contributes $n!$ and the remaining sum is $\det (A)$ by [F3]. For $J = K$ , $A = I_{n}$ and this is $1$ ; for $J \neq K$ , some $j_{a}$ is absent from $K$ , giving a zero row and determinant $0$ . Thus the Slater family is orthonormal.

2.1F6F7step 1.1algebra

[Occupation operators] For $j \in {1, \dots, d}$ the formula of (d) defines a linear endomorphism of the finite-dimensional space $H^{\otimes n}$ ; by [F6] applied to the complete orthonormal family $(e_{i})$ we have $x = \sum_{i} ⟨ x, e_{i} ⟩ e_{i}$ and $N_{j} x = \sum_{i} ∣ i ∣_{j} ⟨ x, e_{i} ⟩ e_{i}$ for every $x$ . Self-adjointness: for $x, y \in H^{\otimes n}$ the expansions give $⟨ N_{j} x, y ⟩ = \sum_{i} ∣ i ∣_{j} ⟨ x, e_{i} ⟩ \overline{⟨ y, e_{i} ⟩} = ⟨ x, N_{j} y ⟩$ because the numbers $∣ i ∣_{j}$ are real, so $N_{j}$ is self-adjoint by [F7]; it is bounded because its range is spanned by the finitely many $e_{i}$ with eigenvalue at most $n$ , and $∥ N_{j} x ∥ \leq n ∥ x ∥$ . The same computation on the basis vectors $e_{i}$ , on which $N_{j}$ is diagonal with the real eigenvalues $∣ i ∣_{j}$ , gives $N_{j} N_{k} e_{i} = ∣ i ∣_{k} ∣ i ∣_{j} e_{i} = N_{k} N_{j} e_{i}$ and $\sum_{j} N_{j} e_{i} = (\sum_{j} ∣ i ∣_{j}) e_{i} = n e_{i}$ ; since the $e_{i}$ form a basis by step 1.1 and both sides of each identity are linear, $N_{j} N_{k} = N_{k} N_{j}$ and $\sum_{j = 1}^{d} N_{j} = n I$ . This proves the operator statements of (d) except the two eigenvector formulas.

2.2F4step 1.1step 1.2step 1.3algebra

[Slater basis and its dimension] By step 1.2 each $e_{J}^{\land} = \sqrt{n!} P_{-}^{(n)} (e_{j_{1}} \otimes \dots \otimes e_{j_{n}})$ lies in $ran P_{-}^{(n)}$ , and each $P_{-}^{(n)} (e_{i})$ is either zero or a multiple of some $e_{J}^{\land}$ ; since the $e_{i}$ form a basis of $H^{\otimes n}$ by step 1.1 and $P_{-}^{(n)}$ is linear, the closed linear span of $(e_{J}^{\land})$ is exactly $ran P_{-}^{(n)}$ (a finite-dimensional, hence closed, subspace). By step 1.3 the family is orthonormal, so it is an orthonormal basis of $ran P_{-}^{(n)}$ , indexed by the $n$ -element subsets $J$ of ${1, \dots, d}$ ; by [F4] there are $(\binom{d}{n})$ of them, so $\dim ran P_{-}^{(n)} = (\binom{d}{n})$ . If $n > d$ , then two of the $n$ entries of any $i$ coincide, so $P_{-}^{(n)} (e_{i}) = 0$ for every basis vector $e_{i}$ by step 1.2, whence $P_{-}^{(n)} = 0$ and $ran P_{-}^{(n)} = {0}$ . In particular $e_{J}^{\land} \neq 0$ whenever $∣ J ∣ = n \leq d$ . This completes (b).

2.3F1F2step 1.1algebra

[The symmetric sums] Fix $λ \in W (n, d)$ . The word $c$ that lists $1$ with multiplicity $λ_{1}$ , then $2$ with multiplicity $λ_{2}$ , and so on through $d$ has $∣ c ∣ = λ$ , so $orb (λ) \neq \emptyset$ and $m_{λ} = \sum_{c \in orb (λ)} e_{c}$ is a nonempty sum of orthonormal vectors of $H^{\otimes n}$ , hence nonzero, with $∥ m_{λ} ∥^{2} = ∣ orb (λ) ∣$ by the orthonormality of the product basis in step 1.1 [F1]. If $λ \neq μ$ then a word has a unique multiplicity vector, so $orb (λ) \cap orb (μ) = \emptyset$ and the inner product of $m_{λ}$ and $m_{μ}$ is the empty sum $0$ . For $π \in S_{n}$ the map $c \mapsto π \cdot c$ , $(π \cdot c)_{k} : = c_{{\hat{π}}^{- 1} (k)}$ , permutes $orb (λ)$ and $U_{π} e_{c} = e_{π \cdot c}$ by [F2], so $U_{π} m_{λ} = m_{λ}$ . Finally, $P_{+}^{(n)} e_{i} = \frac{1}{n!} \sum_{π \in S_{n}} e_{π \cdot i}$ has coefficients supported on $orb (∣ i ∣)$ ; for $c \in orb (∣ i ∣)$ the set ${π : π \cdot i = c}$ is the coset $π_{0} Stab (i)$ for any $π_{0}$ with $π_{0} \cdot i = c$ , hence has cardinality $∣ Stab (i) ∣ \geq 1$ , and it is empty for $c \notin orb (∣ i ∣)$ ; therefore $P_{+}^{(n)} e_{i} = γ_{i} m_{∣ i ∣}$ with $γ_{i} : = ∣ Stab (i) ∣ / n! > 0$ . This proves all the assertions of (c) except the dimension.

3.1F5step 2.3algebra

[Symmetric basis and its dimension] By step 2.3 the $m_{λ}$ are nonzero, pairwise orthogonal and lie in $ran P_{+}^{(n)}$ (indeed $m_{λ} = γ_{i}^{- 1} P_{+}^{(n)} e_{i}$ for any multi-index $i$ with $∣ i ∣ = λ$ , and such $i$ exists because $λ \in W (n, d)$ ); conversely every $P_{+}^{(n)} e_{i}$ is a multiple of some $m_{λ}$ , so by linearity and the basis property of the $e_{i}$ the span of $(m_{λ})_{λ \in W (n, d)}$ is $ran P_{+}^{(n)}$ . A pairwise orthogonal family of nonzero vectors spanning a finite-dimensional space is a basis, so $\dim ran P_{+}^{(n)} = ∣ W (n, d) ∣ = (\binom{n + d - 1}{d - 1}) = (\binom{n + d - 1}{n})$ by [F5]. This completes (c).

4.1step 2.1step 2.2step 3.1algebra

[Occupation numbers on the two bases] Every summand $e_{c}$ of $e_{J}^{\land}$ has exactly one entry equal to $j$ when $j \in J$ and none otherwise, so $∣ c ∣_{j} = 1_{J} (j)$ for every such $c$ ; and every $c \in orb (λ)$ has $∣ c ∣_{j} = λ_{j}$ . Since the $N_{j}$ are linear and act diagonally on the $e_{c}$ by the formula of step 2.1, this gives $N_{j} e_{J}^{\land} = 1_{J} (j) e_{J}^{\land}$ and $N_{j} m_{λ} = λ_{j} m_{λ}$ , the remaining assertions of (d). Both basis families displayed in (b) and (c) therefore consist of joint eigenvectors of $(N_{1}, \dots, N_{d})$ , and the two maps $J \mapsto 1_{J}$ and $λ \mapsto λ$ are injective; hence the joint eigenspaces inside the two sectors are the lines spanned by the corresponding basis vectors, as asserted in (d), and each sector is invariant under every $N_{j}$ .

5.1step 1.1step 1.2step 1.3step 2.2step 2.3step 3.1step 2.1step 4.1∎

[Assembly] Step 1.1 proves (a), steps 1.2, 1.3 and 2.2 prove (b), steps 2.3 and 3.1 prove (c), and steps 2.1 and 4.1 prove (d). The proof uses only the completed tensor powers, the permutation projections, the orthonormal expansions and the stated counting facts, under the Countable Choice hypothesis of [F1] and [F2]; no physical reading of the sectors or of the occupation operators is asserted.

Remarks

Reading of the operators. $N_{j}$ counts the particles occupying the declared basis vector $e_{j}$ ; the theorem proves the exact statements that the two permutation sectors diagonalise the family $(N_{1}, \dots, N_{d})$ and that the antisymmetric sector has only the occupation values $0$ and $1$ . The physical reading of this diagonalisation as an occupation readout of the framework belongs to The declared finite-mode model and its occupation readouts and Pauli exclusion in the declared finite-mode occupation readout, with the bosonic contrast.
Finite dimension. The dimension of $H$ is finite and is part of the hypotheses; no infinite-dimensional Slater basis or occupation operator is constructed here. The open case is treated by different machinery on the Fock-space pair.

Slater and symmetric occupation-number bases of the finite-dimensional permutation sectors

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources