ExampleConstruction: AI-generatedVerification: AI-generatedprecheck pending

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.

Component Check of the SU(2) BRST Differential

Example

Let $g = s u (2)$ with basis $T_{a} = - \frac{i}{2} σ_{a}$ , where

σ_{1} = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), σ_{2} = (\begin{array}{cc} 0 & - i \\ i & 0 \end{array}), σ_{3} = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}) .

Then $[T_{a}, T_{b}] = ϵ_{a b}^{c} T_{c}$ . Use the defining representation on $V = C^{2}$ , so $ρ (T_{a}) = T_{a}$ , and let $U \subseteq R^{n}$ be a nonempty open set, where $n$ is a nonnegative integer. Place $V$ wholly in either even or odd parity. For $n \geq 1$ , use the finite-jet algebra of the earlier BRST definition. For $n = 0$ , $U = R^{0}$ is a point: take the graded-commutative algebra over $C$ freely generated by the two matter components of the chosen parity and three odd ghosts, with no gauge-potential components or positive-order jets. On these algebras, with even gauge potential $A_{μ} = A_{μ}^{a} T_{a}$ , odd ghosts $c^{a}$ , and homogeneous matter components $ψ^{α}$ , define the odd left derivation $s$ by $s f = 0$ on coefficient functions, by prolongation $s (D_{I} Φ) = D_{I} (s Φ)$ on jets, and by

$s A_{μ}^{a} = \partial_{μ} c^{a} + ϵ^{a}_{b c} A_{μ}^{b} c^{c}, s c^{a} = - \frac{1}{2} ϵ^{a}_{b c} c^{b} c^{c}, s ψ = - c^{a} T_{a} ψ .$

The operator $s$ squares to zero on these generators and their formal spacetime jets.

Example references

Finite-jet BRST algebra and sign convention

General nilpotence proof

Facts & Assumptions

Given: The displayed basis, representation, fields, and local BRST formulas.

[A1]

$ϵ^{a}_{b c}$ is the totally antisymmetric symbol with $ϵ^{1}_{23} = 1$ .

[F1]

Finite-Jet Non-Abelian BRST Complex: for $n \geq 1$ , an even gauge potential, odd ghost, and parity-preserving Lie-algebra representation, $s A_{μ} = \partial_{μ} c + [A_{μ}, c]$ , $s c = - \frac{1}{2} [c, c]$ , $s ψ = - ρ (c) ψ$ , and $s (D_{I} Φ) = D_{I} (s Φ)$ , with $s (F G) = (s F) G + (- 1)^{∣ F ∣} F (s G)$ for homogeneous $F$ .

[F2]

Nilpotence of the Finite-Jet Non-Abelian BRST Differential: for $n \geq 1$ , these formulas square to zero on all finite-jet polynomials whenever the Lie-algebra Jacobi and representation identities hold.

Verification

1.1A1F1algebra

Direct multiplication gives $σ_{1} σ_{2} = i σ_{3}$ , $σ_{2} σ_{1} = - i σ_{3}$ , $σ_{2} σ_{3} = i σ_{1}$ , $σ_{3} σ_{2} = - i σ_{1}$ , $σ_{3} σ_{1} = i σ_{2}$ , and $σ_{1} σ_{3} = - i σ_{2}$ , while $σ_{a}^{2} = I$ . Hence $[T_{a}, T_{b}] = (- i / 2)^{2} [σ_{a}, σ_{b}] = ϵ_{a b}^{c} T_{c}$ by [A1]. Matrix commutators satisfy Jacobi because the Jacobiator expands to $X Y Z - Y X Z - Z X Y + Z Y X + Y Z X - Z Y X - X Y Z + X Z Y + Z X Y - X Z Y - Y Z X + Y X Z = 0$ , so these structure constants obey Jacobi. Since $ρ (T_{a}) = T_{a}$ , the same commutator identity is the representation identity; it preserves either chosen pure grading of $V$ . For $n \geq 1$ , substitution into [F1] gives exactly the three component formulas.

2.1givenF2step 1.1

If $n \geq 1$ , the hypotheses of [F2] hold for $s u (2)$ and its defining representation with either pure grading. Applying that lemma gives $s^{2} = 0$ on the generators, every total-derivative jet, and their finite graded-polynomial algebra.

3.1givenA1step 1.1step 2.1algebra∎

If $n = 0$ , the displayed formulas reduce to $s c^{1} = - c^{2} c^{3}$ , $s c^{2} = - c^{3} c^{1}$ , $s c^{3} = - c^{1} c^{2}$ , and $s ψ = - c^{a} T_{a} ψ$ . The odd left-derivation rule gives $s^{2} c^{1} = c^{3} c^{1} c^{3} - c^{2} c^{1} c^{2} = 0$ , since each odd ghost has square zero; cyclic permutation proves $s^{2} c^{2} = s^{2} c^{3} = 0$ . Put $C = c^{a} T_{a}$ . Anticommutation and step 1.1 give $C^{2} = \frac{1}{2} c^{a} c^{b} [T_{a}, T_{b}] = \frac{1}{2} ϵ^{d}_{a b} c^{a} c^{b} T_{d} = - s C$ , so $s^{2} ψ = - (s C) ψ + C (s ψ) = C^{2} ψ - C^{2} ψ = 0$ for either matter parity. The square of an odd derivation is an even derivation, as the cross terms in $s^{2} (F G)$ cancel. It therefore vanishes on this entire freely generated graded-commutative algebra. There are no remaining gauge components or positive-order jets. Together with step 2.1, this proves the assertion for every allowed $n$ .

Component Check of the SU(2) BRST Differential

Example

Example references

Facts & Assumptions

Verification

Depends on

Dependency tree · 1 level