Charged commutants with arbitrary matter

Abstract

A nonzero ghost charge degree annihilates any endomorphism commuting with all tensor ghost modes.

M is an arbitrary complex module. Tensor products and endomorphisms are algebraic; no topology, finite dimension, positivity or irreducibility is assumed. The maps b, c and ghostNumber are the actual maps of BcGhostFock and BcGhostCharge. Bracketed group and module assumptions are anonymous instance arguments.

Definition 1.1 (liftGhost).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall T\in \mathrm{Module}.\mathrm{End}\left(Complex,Fock\right),\mathrm{liftGhost}\left(T\right)=\mathrm{TensorProduct}.\mathrm{map}\left(\mathrm{LinearMap}.\mathrm{id}\left(M\right),T\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostChargeTensor.liftGhost (✓ std3).

Source. Repository-derived.

Commentary.

The matter factor is acted on by its identity map.

Definition 1.2 (number).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]number=\mathrm{liftGhost}\left(ghostNumber\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostChargeTensor.number (✓ std3).

Source. Repository-derived.

Commentary.

The tensor ghost-number operator.

Definition 1.3 (B).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall m\in Int,B\left(m\right)=\mathrm{liftGhost}\left(b\left(m\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostChargeTensor.B (✓ std3).

Source. Repository-derived.

Commentary.

Every integer b mode acts on the ghost factor.

Definition 1.4 (C).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall m\in Int,C\left(m\right)=\mathrm{liftGhost}\left(c\left(m\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostChargeTensor.C (✓ std3).

Source. Repository-derived.

Commentary.

Every integer c mode acts on the ghost factor.

Definition 1.5 (partialNumber).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall K\in \mathrm{Finset}\left(Int\right),\mathrm{partialNumber}\left(K\right)=\mathrm{Finset}.\mathrm{sum}\left(K,\lambda (n:Int)\mapsto (\mathrm{liftGhost}\left(\mathrm{normalTerm}\left(n\right)\right))\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostChargeTensor.partialNumber (✓ std3).

Source. Repository-derived.

Commentary.

A finite sum of the actual lifted normal bilinears.

Theorem 1.6 (tensor finite capture).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall x\in \mathrm{TensorProduct}\left(Complex,M,Fock\right),\exists K\in \mathrm{Finset}\left(Int\right),\forall L\in \mathrm{Finset}\left(Int\right),\mathrm{Finset}.\mathrm{Subset}\left(K,L\right)\Rightarrow \mathrm{partialNumber}\left(L,x\right)=\mathrm{number}\left(x\right)$$

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

Source. Repository-derived.

Commentary.

Each pure tensor inherits a finite capture from its ghost vector. Tensor-product induction combines captures by finite union, so every larger finite set still computes number on the original tensor.

Theorem 1.7 (number commutes of signed modes).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall E\in \mathrm{Module}.\mathrm{End}\left(Complex,\mathrm{TensorProduct}\left(Complex,M,Fock\right)\right),\forall epsilon\in Complex,epsilon\cdot epsilon=1\Rightarrow \left(\left(\forall m\in Int,E\cdot B\left(m\right)=\mathrm{smul}\left(epsilon,B\left(m\right)\cdot E\right)\right)\Rightarrow \left(\left(\forall m\in Int,E\cdot C\left(m\right)=\mathrm{smul}\left(epsilon,C\left(m\right)\cdot E\right)\right)\Rightarrow number\cdot E-E\cdot number=0\right)\right)$$

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

Source. Repository-derived.

Commentary.

For epsilon squared equal to one, the two signs cancel in each normal bilinear. At a fixed x choose one finite union capturing x and E x. Commutation with that finite sum identifies number applied to E x with E applied to number x. Epsilon one gives commutation, and epsilon minus one covers anticommutation with both odd families.

Theorem 1.8 (charged commutant vanishes).

$$\forall M\in Type,[\mathrm{AddCommGroup}\left(M\right)][\mathrm{Module}\left(Complex,M\right)]\forall E\in \mathrm{Module}.\mathrm{End}\left(Complex,\mathrm{TensorProduct}\left(Complex,M,Fock\right)\right),\left(\forall m\in Int,E\cdot B\left(m\right)=B\left(m\right)\cdot E\right)\Rightarrow \left(\left(\forall m\in Int,E\cdot C\left(m\right)=C\left(m\right)\cdot E\right)\Rightarrow \left(\forall d\in Complex,d\ne 0\Rightarrow \left(number\cdot E-E\cdot number=\mathrm{smul}\left(d,E\right)\Rightarrow E=0\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Finite normal capture first proves that the charge commutator is zero. The stipulated degree d is nonzero, so d times E equal to zero forces E itself to be zero. This uses no scalar-commutant assertion on the tensor product.

The theorem can eliminate a later BRST residual only after that residual is constructed on this tensor carrier and its mode commutation and nonzero degree are proved. It does not construct a total BRST operator, prove nilpotence, or complete the string objective.

References

• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.B
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.C
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.charged_commutant_vanishes
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.liftGhost
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.number
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.number_commutes_of_signed_modes
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.partialNumber
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostChargeTensor.tensor_finite_capture
• Dependency: D5/S3/Quantum/Fermionic/BcGhostCharge