Countable finite-excitation Fock space

Abstract

Countably many fermionic modes act on all finite occupation states through an exact coherent finite-prefix construction.

The carrier is algebraic: every state has finite support among finite subsets of the natural numbers. No completion or infinite operator sum is used. FullC is the original finite Jordan–Wigner annihilator. Its signed entry formula is supplied by HardCoreCompression.fullC_entry; the Boolean occupation encoding and its inverse are supplied by CompletedCorrelationalBound. The new intertwinings identify those matrix actions with the all-particle-number signed occupation action. Finite capture and word transport then transfer the actual finite CAR to unrestricted natural indices. The same-site square is obtained algebraically from FockMajoranaCarrier.majorana_clifford_and_parity. The linear extension uses Mathlib Finsupp.lsum.

Definition 1.1 (Fock).

$$Fock=\mathrm{Finsupp}\left(\mathrm{Finset}\left(Nat\right),Complex\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.Fock (✓ std3).

Source. Repository-derived.

Commentary.

The direct sum has one coordinate for each finite occupation set.

Definition 1.2 (ket).

$$\forall S\in \mathrm{Finset}\left(Nat\right),\mathrm{ket}\left(S\right)=\mathrm{Finsupp}.\mathrm{single}\left(S,1\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.ket (✓ std3).

Source. Repository-derived.

Commentary.

The occupation basis vector has coefficient one at S.

Definition 1.3 (vacuum).

$$vacuum=\mathrm{ket}\left(\mathrm{Finset}.\mathrm{empty}\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.vacuum (✓ std3).

Source. Repository-derived.

Commentary.

The vacuum is the empty occupation.

Definition 1.4 (lowerCount).

$$\forall j\in Nat,\forall S\in \mathrm{Finset}\left(Nat\right),\mathrm{lowerCount}\left(j,S\right)=\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left(\lambda (i:Nat)\mapsto i<j,S\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.lowerCount (✓ std3).

Source. Repository-derived.

Commentary.

Only occupied sites strictly below j contribute to the sign.

Definition 1.5 (phase).

$$\forall j\in Nat,\forall S\in \mathrm{Finset}\left(Nat\right),\mathrm{phase}\left(j,S\right)=(-1:Complex{)}^{\mathrm{lowerCount}\left(j,S\right)}$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.phase (✓ std3).

Source. Repository-derived.

Commentary.

The sign is real and equals plus or minus one.

Definition 1.6 (annihilate).

$$\forall j\in Nat,\mathrm{annihilate}\left(j\right)=\mathrm{Finsupp}.\mathrm{lsum}\left(Complex,\lambda (S:\mathrm{Finset}\left(Nat\right))\mapsto \mathrm{LinearMap}.\mathrm{smulRight}\left(\mathrm{LinearMap}.\mathrm{id},\mathrm{ite}\left(j\in S,\mathrm{smul}\left(\mathrm{phase}\left(j,S\right),\mathrm{ket}\left(\mathrm{Finset}.\mathrm{erase}\left(S,j\right)\right)\right),0\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.annihilate (✓ std3).

Source. Repository-derived.

Commentary.

The signed deletion rule extends linearly to a genuine endomorphism.

Definition 1.7 (create).

$$\forall j\in Nat,\mathrm{create}\left(j\right)=\mathrm{Finsupp}.\mathrm{lsum}\left(Complex,\lambda (S:\mathrm{Finset}\left(Nat\right))\mapsto \mathrm{LinearMap}.\mathrm{smulRight}\left(\mathrm{LinearMap}.\mathrm{id},\mathrm{ite}\left(j\in S,0,\mathrm{smul}\left(\mathrm{phase}\left(j,S\right),\mathrm{ket}\left(\mathrm{insert}\left(j,S\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.create (✓ std3).

Source. Repository-derived.

Commentary.

The signed insertion rule vanishes at an already occupied site and extends linearly.

Theorem 1.8 (annihilate ket).

$$\forall j\in Nat,\forall S\in \mathrm{Finset}\left(Nat\right),\mathrm{annihilate}\left(j,\mathrm{ket}\left(S\right)\right)=\mathrm{ite}\left(j\in S,\mathrm{smul}\left(\mathrm{phase}\left(j,S\right),\mathrm{ket}\left(\mathrm{Finset}.\mathrm{erase}\left(S,j\right)\right)\right),0\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.annihilate_ket (✓ std3). ∎

Source. Repository-derived.

Commentary.

Annihilation acts on each occupation basis vector by signed deletion.

Theorem 1.9 (create ket).

$$\forall j\in Nat,\forall S\in \mathrm{Finset}\left(Nat\right),\mathrm{create}\left(j,\mathrm{ket}\left(S\right)\right)=\mathrm{ite}\left(j\in S,0,\mathrm{smul}\left(\mathrm{phase}\left(j,S\right),\mathrm{ket}\left(\mathrm{insert}\left(j,S\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.create_ket (✓ std3). ∎

Source. Repository-derived.

Commentary.

Creation acts on each occupation basis vector by signed insertion.

Theorem 1.10 (end ext).

$$\forall T\in \mathrm{Module}.\mathrm{End}\left(Complex,Fock\right),\forall U\in \mathrm{Module}.\mathrm{End}\left(Complex,Fock\right),\left(\forall S\in \mathrm{Finset}\left(Nat\right),T\left(\mathrm{ket}\left(S\right)\right)=U\left(\mathrm{ket}\left(S\right)\right)\right)\Rightarrow T=U$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.end_ext (✓ std3). ∎

Source. Repository-derived.

Commentary.

Complex linear endomorphisms agreeing on every occupation basis vector are equal.

Definition 1.11 (parity).

$$parity=\mathrm{Finsupp}.\mathrm{lsum}\left(Complex,\lambda (S:\mathrm{Finset}\left(Nat\right))\mapsto \mathrm{LinearMap}.\mathrm{smulRight}\left(\mathrm{LinearMap}.\mathrm{id},\mathrm{smul}\left((-1:Complex{)}^{\mathrm{Finset}.\mathrm{card}\left(S\right)},\mathrm{ket}\left(S\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.parity (✓ std3).

Source. Repository-derived.

Commentary.

Parity is the occupation-cardinality sign.

Definition 1.12 (prefixEmbed).

$$\forall N\in Nat,\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{prefixEmbed}\left(N,v\right)=\sum _{t:\mathrm{Assignment}\left(N\right)}\mathrm{smul}\left(v\left(t\right),\mathrm{ket}\left(\mathrm{occupationSet}\left(t\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.prefixEmbed (✓ std3).

Source. Repository-derived.

Commentary.

The finite Boolean vector is embedded by its original occupation coordinates.

Theorem 1.13 (prefixEmbed injective).

$$\forall N\in Nat,\mathrm{Function}.\mathrm{Injective}\left(\mathrm{prefixEmbed}\left(N\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.prefixEmbed_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reading the coefficient at an encoded occupation recovers the finite input coordinate.

Theorem 1.14 (jw annihilate intertwining).

$$\forall N\in Nat,\forall j\in \mathrm{Fin}\left(N\right),\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{annihilate}\left(\mathrm{Fin}.\mathrm{val}\left(j\right),\mathrm{prefixEmbed}\left(N,v\right)\right)=\mathrm{prefixEmbed}\left(N,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{fullC}\left(j\right),v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.jw_annihilate_intertwining (✓ std3). ∎

Source. Repository-derived.

Commentary.

The existing signed matrix coefficient and occupation deletion identify the two actual actions.

Theorem 1.15 (jw create intertwining).

$$\forall N\in Nat,\forall j\in \mathrm{Fin}\left(N\right),\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{create}\left(\mathrm{Fin}.\mathrm{val}\left(j\right),\mathrm{prefixEmbed}\left(N,v\right)\right)=\mathrm{prefixEmbed}\left(N,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{fullC}\left(j\right)\right),v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.jw_create_intertwining (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conjugate transposition of the existing entry formula gives signed occupation insertion; the phase is real.

Definition 1.16 (prefixExtend).

$$\forall N\in Nat,\forall M\in Nat,\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{prefixExtend}\left(N,M,v\right)=\sum _{t:\mathrm{Assignment}\left(N\right)}\mathrm{smul}\left(v\left(t\right),\mathrm{Pi}.\mathrm{single}\left(\mathrm{occupationOfSet}\left(M,\mathrm{occupationSet}\left(t\right)\right),1\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.prefixExtend (✓ std3).

Source. Repository-derived.

Commentary.

Assignments are extended by false at the additional sites. On basis assignments the displayed occupationOfSet formula is literal.

Theorem 1.17 (prefix coherence).

$$\forall N\in Nat,\forall M\in Nat,N\le M\Rightarrow \left(\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{prefixEmbed}\left(M,\mathrm{prefixExtend}\left(N,M,v\right)\right)=\mathrm{prefixEmbed}\left(N,v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.prefix_coherence (✓ std3). ∎

Source. Repository-derived.

Commentary.

For N at most M, extending by empty sites preserves the countable state.

Theorem 1.18 (cutoff annihilate coherence).

$$\forall N\in Nat,\forall M\in Nat,\forall h\in N\le M,\forall j\in \mathrm{Fin}\left(N\right),\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{fullC}\left(\mathrm{Fin}.\mathrm{castLE}\left(h,j\right)\right),\mathrm{prefixExtend}\left(N,M,v\right)\right)=\mathrm{prefixExtend}\left(N,M,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{fullC}\left(j\right),v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.cutoff_annihilate_coherence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Injectivity of the larger embedding and the annihilator intertwining prove coherent matrix transport.

Theorem 1.19 (cutoff create coherence).

$$\forall N\in Nat,\forall M\in Nat,\forall h\in N\le M,\forall j\in \mathrm{Fin}\left(N\right),\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{fullC}\left(\mathrm{Fin}.\mathrm{castLE}\left(h,j\right)\right)\right),\mathrm{prefixExtend}\left(N,M,v\right)\right)=\mathrm{prefixExtend}\left(N,M,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{fullC}\left(j\right)\right),v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.cutoff_create_coherence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The creator matrices obey the same coherent extension law.

Theorem 1.20 (finite capture).

$$\forall v\in Fock,\forall J\in \mathrm{Finset}\left(Nat\right),\exists N\in Nat,\left(\forall j\in Nat,j\in J\Rightarrow j<N\right)\wedge \left(\exists w\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{prefixEmbed}\left(N,w\right)=v\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.finite_capture (✓ std3). ∎

Source. Repository-derived.

Commentary.

One prefix contains every occupied site of the state and every site in the selected finite set J. Capture is exact, including the empty-state boundary.

Definition 1.21 (mode).

$$\forall j\in Nat,\forall b\in Bool,\mathrm{mode}\left(j,b\right)=\mathrm{ite}\left(b,\mathrm{create}\left(j\right),\mathrm{annihilate}\left(j\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.mode (✓ std3).

Source. Repository-derived.

Commentary.

True selects creation and false selects annihilation.

Definition 1.22 (finiteMode).

$$\forall N\in Nat,\forall j\in \mathrm{Fin}\left(N\right),\forall b\in Bool,\mathrm{finiteMode}\left(j,b\right)=\mathrm{ite}\left(b,\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{fullC}\left(j\right)\right),\mathrm{fullC}\left(j\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.finiteMode (✓ std3).

Source. Repository-derived.

Commentary.

The finite supplier follows the same Boolean convention.

Definition 1.23 (word).

$$\mathrm{word}\left(\mathrm{List}.\mathrm{nil}\right)=(1:\mathrm{Module}.\mathrm{End}\left(Complex,Fock\right))\wedge \left(\forall p\in \mathrm{Prod}\left(Nat,Bool\right),\forall w\in \mathrm{List}\left(\mathrm{Prod}\left(Nat,Bool\right)\right),\mathrm{word}\left(\mathrm{List}.\mathrm{cons}\left(p,w\right)\right)=\mathrm{mode}\left(\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\cdot \mathrm{word}\left(w\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.word (✓ std3).

Source. Repository-derived.

Commentary.

Products act on the rightmost state first.

Definition 1.24 (finiteWord).

$$\forall N\in Nat,\mathrm{finiteWord}\left(\mathrm{List}.\mathrm{nil}\right)=\mathrm{Matrix}.\mathrm{one}\left(\mathrm{Assignment}\left(N\right)\right)\wedge \left(\forall p\in \mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right),\forall w\in \mathrm{List}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right)\right),\mathrm{finiteWord}\left(\mathrm{List}.\mathrm{cons}\left(p,w\right)\right)=\mathrm{finiteMode}\left(\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\cdot \mathrm{finiteWord}\left(w\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CountableOccupationFock.finiteWord (✓ std3).

Source. Repository-derived.

Commentary.

Finite matrix words include the empty identity word.

Theorem 1.25 (word intertwining).

$$\forall N\in Nat,\forall w\in \mathrm{List}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right)\right),\forall v\in \mathrm{Assignment}\left(N\right)\to Complex,\mathrm{word}\left(\mathrm{List}.\mathrm{map}\left(\lambda (p:\mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right))\mapsto \mathrm{Prod}.\mathrm{mk}\left(\mathrm{Fin}.\mathrm{val}\left(\mathrm{Prod}.\mathrm{fst}\left(p\right)\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right),w\right),\mathrm{prefixEmbed}\left(N,v\right)\right)=\mathrm{prefixEmbed}\left(N,\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{finiteWord}\left(w\right),v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.word_intertwining (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both single-operator intertwinings propagate through every finite word.

Theorem 1.26 (car).

$$\forall i\in Nat,\forall j\in Nat,\forall a\in Bool,\forall b\in Bool,\mathrm{mode}\left(i,a\right)\cdot \mathrm{mode}\left(j,b\right)+\mathrm{mode}\left(j,b\right)\cdot \mathrm{mode}\left(i,a\right)=\mathrm{ite}\left(i=j\wedge a\ne b,(1:\mathrm{Module}.\mathrm{End}\left(Complex,Fock\right)),0\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.car (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite state and the two chosen indices fit in one prefix. Word transport consumes the finite CAR, including the equal-site nilpotence supplied by the Majorana relations.

Theorem 1.27 (annihilate vacuum).

$$\forall j\in Nat,\mathrm{annihilate}\left(j,vacuum\right)=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.annihilate_vacuum (✓ std3). ∎

Source. Repository-derived.

Commentary.

No site is occupied in the vacuum.

Theorem 1.28 (create vacuum).

$$\forall j\in Nat,\mathrm{create}\left(j,vacuum\right)=\mathrm{ket}\left(\mathrm{Finset}.\mathrm{singleton}\left(j\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.create_vacuum (✓ std3). ∎

Source. Repository-derived.

Commentary.

Insertion into the vacuum has sign one.

Theorem 1.29 (parity involution).

$$parity\cdot parity=(1:\mathrm{Module}.\mathrm{End}\left(Complex,Fock\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.parity_involution (✓ std3). ∎

Source. Repository-derived.

Commentary.

Squaring the occupation sign gives the identity on every basis state.

Theorem 1.30 (parity odd).

$$\forall j\in Nat,\forall b\in Bool,parity\cdot \mathrm{mode}\left(j,b\right)+\mathrm{mode}\left(j,b\right)\cdot parity=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.parity_odd (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every nonzero insertion or deletion changes the cardinality by one.

Theorem 1.31 (creator spanning).

$$\mathrm{Submodule}.\mathrm{span}\left(Complex,\mathrm{Set}.\mathrm{range}\left(\lambda (w:\mathrm{List}\left(Nat\right))\mapsto \mathrm{word}\left(\mathrm{List}.\mathrm{map}\left(\lambda (j:Nat)\mapsto \mathrm{Prod}.\mathrm{mk}\left(j,true\right),w\right),vacuum\right)\right)\right)=\mathrm{Submodule}.\mathrm{top}\left(Complex,Fock\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.creator_spanning (✓ std3). ∎

Source. Repository-derived.

Commentary.

Insertion induction produces each occupation basis vector as a nonzero scalar multiple of a creator word. Finite linear extension spans the entire carrier.

Theorem 1.32 (common annihilator kernel).

$$\forall v\in Fock,\left(\forall j\in Nat,\mathrm{annihilate}\left(j,v\right)=0\right)\iff \left(\exists alpha\in Complex,v=\mathrm{smul}\left(alpha,vacuum\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.common_annihilator_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

If a nonempty occupation S contains j, the coefficient of S with j deleted in annihilate j v is phase j S times the coefficient of S in v. Deletion is injective among occupations containing j, and the sign is nonzero. Thus every nonempty coefficient vanishes, while the empty coefficient supplies the unique scalar. Conversely all annihilators kill each scalar multiple of the actual vacuum.

Theorem 1.33 (eq scalar of creator commutation).

$$\forall A\in \mathrm{Module}.\mathrm{End}\left(Complex,Fock\right),\forall alpha\in Complex,A\left(vacuum\right)=\mathrm{smul}\left(alpha,vacuum\right)\Rightarrow \left(\left(\forall j\in Nat,A\cdot \mathrm{create}\left(j\right)=\mathrm{create}\left(j\right)\cdot A\right)\Rightarrow A=\mathrm{smul}\left(alpha,(1:\mathrm{Module}.\mathrm{End}\left(Complex,Fock\right))\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/CountableOccupationFock.eq_scalar_of_creator_commutation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Commutation moves A through each finite creator word. Its scalar action on the vacuum therefore holds on every creator-word state, and creator_spanning with linear-map extensionality extends that same scalar to every Fock vector. No irreducibility hypothesis or finite cutoff is imposed.

This algebraic representation asserts CAR, exact cutoff transport and parity. Statewise quadratic normal sums, the bc Virasoro anomaly, the all-state super vertex algebra, graded tensor matter, BRST charge and nilpotence, cohomology, no-ghost results and the Monster, sewing, string and AdS identifications require further constructions.

References

• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.Fock
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.annihilate
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.annihilate_ket
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.annihilate_vacuum
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.car
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.common_annihilator_kernel
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.create
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.create_ket
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.create_vacuum
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.creator_spanning
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.cutoff_annihilate_coherence
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.cutoff_create_coherence
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.end_ext
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.eq_scalar_of_creator_commutation
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.finiteMode
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.finiteWord
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.finite_capture
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.jw_annihilate_intertwining
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.jw_create_intertwining
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.ket
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.lowerCount
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.mode
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.parity
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.parity_involution
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.parity_odd
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.phase
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.prefixEmbed
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.prefixEmbed_injective
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.prefixExtend
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.prefix_coherence
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.vacuum
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.word
• Truth anchor: D5/S3/Quantum/Fermionic/CountableOccupationFock.word_intertwining
• Dependency: D5/S3/Quantum/Fermionic/FockMajoranaCarrier
• Dependency: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound
• Dependency: D5/S3/Quantum/SpinChains/SupersymmetricFermion/HardCoreCompression