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.
Four-dimensional chiral anomaly coefficient interface
Definition
Fix a finite-dimensional real Lie algebra , a finite index set with real basis , and a finite species index set . Let be its complexification, with complex scalar multiplication on the second tensor factor and the complex-bilinear bracket specified on pure tensors by for and . Identify with its canonical real embedding ; in particular in a representation argument means . For each , let be a finite-dimensional complex vector space and let be a complex-linear Lie-algebra representation, so . Attach the bookkeeping label to each species. In this interface, a “left-handed Weyl species” means exactly the data ; the label is not a spinor field or a chirality operator. No spacetime manifold, spinor bundle or field, kinetic operator or action, integration of to a gauge group, regulator, effective action, or gauge-variation map is constructed or assumed.
Set and define for endomorphisms of . The algebraic cubic representation coefficient is The basis and generator normalization are fixed as part of the data. No factor is included in the anticommutator. If , then is twice . Cancellation of this coefficient means for every basis triple in this convention. These are representation traces only; calling them anomaly coefficients in a physical model requires an additional theorem.
Define the separate linear representation coefficient by For one-dimensional representation spaces of a one-dimensional Abelian Lie algebra with fixed generator and , this gives . The coefficient is recorded separately because a later mixed gauge-gravitational analysis needs its own representation data. Such an analysis must specify its spacetime and gauge connections, curvature conventions, and index polynomial; no mixed-anomaly formula is asserted by this interface.
The only local BRST obstruction statement recorded here is a separate formal result for the specific Abelian jet complex used by the mathematical supplier, not a BRST construction for the general Lie algebra above. In the convention of def-qftx-brst-relative-local-cohomology, a compactly supported local horizontal -form is a finite sum of , with each coefficient smooth and compactly supported in and polynomial in finitely many field-jet coordinates ; indexes the field and ghost generators and their derivative multi-indices. Its total derivative is , where is the unit multi-index and is the left graded derivative; . The differential is the odd ghost-number-one Abelian derivation fixed by def-qftx-abelian-local-brst, with , , , , and , extended by the graded Leibniz rule and commutation with spacetime derivatives; are even, are odd, and their ghost numbers are , respectively. On a horizontal -form , use , where is this coefficient derivation. Thus and , with nilpotence of established by lem-qftx-brst-nilpotence-doublets. Write for the space of these forms homogeneous of ghost number and form degree , and set it to zero outside that form-degree range. For each order , let be a bigraded subspace with that is stable in the sense that and . The relative class is the quotient
The direct supplier prop-qftx-anomaly-obstruction is a draft proposition with a supplied conditional proof. Its scalar construction premise is the draft theorem thm-qftx-scalar-eg-induction: under the Axiom of Choice (every family of nonempty sets has a choice function) and Countable Choice (every sequence of nonempty sets has a choice function), and for admissible flat scalar free data and a local scalar polynomial class as defined by def-qftx-local-time-ordered-system, that theorem asserts existence of symmetric multilinear time-ordered maps satisfying its contract at every finite order, with finite graph scaling bounds and local extension ambiguities. It asserts no convergence, adiabatic limit, positivity, or Ward identity. The exact statement of prop-qftx-anomaly-obstruction assumes those data and a time-ordering scheme satisfying that theorem. For each ghost number , define the local-functional quotient and put . The formal series module is , where is a formal indeterminate. For some , it further assumes an odd formal ghost-number-one operator on this module, , and an element with , where denotes terms of formal degree at least , all lower coefficients vanish, and for compactly supported . It requires to be exactly the admissible local counterterm densities. Under these hypotheses, that proposition states that is -exact and that there exists an admissible such that shifting by cancels the order- breaking if and only if . This is used only in the stated conditional form: it does not establish that the hypotheses hold for the representation data above or construct a physical effective action, and it does not prove a quantum action principle.
Accordingly, this interface asserts no physical anomaly-cancellation criterion from . A later physical theorem must specify its spacetime, field space, action, regulator and renormalized effective-action map, and the map that assigns a local gauge-variation density to that data. It must then prove the relation of that density to an explicitly specified local BRST cohomology class and invariant six-form polynomial, with mixed gauge-gravitational coefficients and loop-order hypotheses stated separately. No conclusion about transformations outside the identity component of a separately specified full gauge-transformation group follows from this infinitesimal representation tensor. Vanishing alone proves neither a nonperturbative gauge theory nor the absence of failures under such transformations.