The actual normally ordered cubic ghost charge

Abstract

Statewise locally finite cubic ghost charge

The formulas are the classical bc ghost BRST construction, with vacuum cuts b at minus one and c at two. See Kato and Ogawa, Nuclear Physics B 212 (1983), 443–460, and Polchinski, String Theory, volume 1, chapter 4. No novelty of these formulas is claimed. The formal carrier is the original complex finitely supported occupation space.

Definition 1.1 (cubic).

$$\forall p\in Int,\forall q\in Int,\mathrm{cubic}\left(p,q\right)=\mathrm{ite}\left(\mathrm{LE}.\mathrm{le}\left(p,1\right),\mathrm{ite}\left(\mathrm{LE}.\mathrm{le}\left(q,1\right),c\left(p\right)\cdot c\left(q\right)\cdot b\left(-p-q\right),\mathrm{ite}\left(\mathrm{LE}.\mathrm{le}\left(-p-q,-2\right),-\left(c\left(p\right)\cdot b\left(-p-q\right)\cdot c\left(q\right)\right),c\left(p\right)\cdot c\left(q\right)\cdot b\left(-p-q\right)\right)\right),\mathrm{ite}\left(\mathrm{LE}.\mathrm{le}\left(q,1\right),\mathrm{ite}\left(\mathrm{LE}.\mathrm{le}\left(-p-q,-2\right),c\left(q\right)\cdot b\left(-p-q\right)\cdot c\left(p\right),-\left(c\left(q\right)\cdot c\left(p\right)\cdot b\left(-p-q\right)\right)\right),\mathrm{ite}\left(\mathrm{LE}.\mathrm{le}\left(-p-q,-2\right),b\left(-p-q\right)\cdot c\left(p\right)\cdot c\left(q\right),c\left(p\right)\cdot c\left(q\right)\cdot b\left(-p-q\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostCubic.cubic (✓ std3).

Source. Repository-derived.

Commentary.

Creators precede annihilators before summation. When b is a creator its cyclic move through both c factors has positive sign. Anticommuting the c factors gives exactly the stable fermionic order; no contraction is added by definition.

Definition 1.2 (cubicTerm).

$$\forall pq\in \mathrm{Prod}\left(Int,Int\right),\mathrm{cubicTerm}\left(pq\right)=\mathrm{smul}\left(\mathrm{div}\left(1,2\right)\cdot \mathrm{Int}.\mathrm{cast}\left(\mathrm{Prod}.\mathrm{fst}\left(pq\right)-\mathrm{Prod}.\mathrm{snd}\left(pq\right)\right),\mathrm{cubic}\left(\mathrm{Prod}.\mathrm{fst}\left(pq\right),\mathrm{Prod}.\mathrm{snd}\left(pq\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostCubic.cubicTerm (✓ std3).

Source. Repository-derived.

Commentary.

The full ordered pair sum carries the classical factor one half.

Theorem 1.3 (cubic finite).

$$\forall v\in Fock,\mathrm{Function}.\mathrm{HasFiniteSupport}\left((pq\mapsto \mathrm{cubic}\left(\mathrm{Prod}.\mathrm{fst}\left(pq\right),\mathrm{Prod}.\mathrm{snd}\left(pq\right),v\right))\right)$$

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

Source. Repository-derived.

Commentary.

On a basis occupation S, put A equal to its largest site plus three. A live cubic has p and q at most A and p plus q at least minus A. Both indices therefore lie in the finite interval from minus twice A to A. Finite linear combinations give the assertion for every actual state.

Theorem 1.4 (cubicTerm finite).

$$\forall v\in Fock,\mathrm{Function}.\mathrm{HasFiniteSupport}\left((pq\mapsto \mathrm{cubicTerm}\left(pq,v\right))\right)$$

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

Source. Repository-derived.

Commentary.

Weighting cannot enlarge the pointwise support. This fact is consumed by the linear charge and every sum exchange.

Definition 1.5 (Qg).

$$\forall v\in Fock,\mathrm{Qg}\left(v\right)=\sum _{pq\in \mathrm{Prod}\left(Int,Int\right)}^{fin}\mathrm{cubicTerm}\left(pq,v\right)$$

Formalization. D5/S3/Quantum/Fermionic/BcGhostCubic.Qg (✓ std3).

Source. Repository-derived.

Commentary.

This is a genuine complex-linear endomorphism. Its value is defined by a statewise finite sum; the operator family itself is not declared finitely supported.

Theorem 1.6 (cubic b).

$$\forall p\in Int,\forall q\in Int,\forall r\in Int,\mathrm{cubic}\left(p,q\right)\cdot b\left(r\right)+b\left(r\right)\cdot \mathrm{cubic}\left(p,q\right)=\mathrm{ite}\left(q+r=0,\mathrm{normal}\left(-p-q,p\right),0\right)-\mathrm{ite}\left(p+r=0,\mathrm{normal}\left(-p-q,q\right),0\right)$$

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

Source. Repository-derived.

Commentary.

Finite CAR reduces the individual cubic to two bilinears with the Virasoro normal ordering.

Theorem 1.7 (cubic c).

$$\forall p\in Int,\forall q\in Int,\forall r\in Int,\mathrm{cubic}\left(p,q\right)\cdot c\left(r\right)+c\left(r\right)\cdot \mathrm{cubic}\left(p,q\right)=\mathrm{ite}\left(-p-q+r=0,c\left(p\right)\cdot c\left(q\right),0\right)$$

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

Source. Repository-derived.

Commentary.

Only the b contraction remains. All signs are checked in the actual operator algebra.

Theorem 1.8 (Qg vacuum).

$$\mathrm{Qg}\left(\mathrm{vacuum}\right)=0$$

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

Source. Repository-derived.

Commentary.

An all-creator cubic on the vacuum forces p and q both equal to one, whose repeated c factor is zero. Every other branch has an annihilator on the right. The square proof consumes this vacuum identity.

This is an algebraic ghost-sector construction. It supplies a dependency for the broader Monster, vertex algebra, conformal field theory and string programme. It does not establish the matter-tensor BRST charge, its cohomology, a no-ghost theorem, string dynamics or AdS/CFT.

References

• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.Qg
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.Qg_vacuum
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.cubic
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.cubicTerm
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.cubicTerm_finite
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.cubic_b
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.cubic_c
• Truth anchor: D5/S3/Quantum/Fermionic/BcGhostCubic.cubic_finite
• Dependency: D5/S3/Quantum/Fermionic/BcGhostVirasoro