LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Smeared free Dirac CAR fields and graded locality

Statement

Assume Countable Choice The Axiom of Countable Choice ( ${A C}_{ω}$ ), let $μ \geq 0$ , and use Dirac Clifford matrices and energy projections, Dirac matrix identities and orthogonal energy projections, and the antisymmetric Fock and CAR conventions of Schwartz/distribution spaces and Hilbert Fock conventions and Bosonic and fermionic Fock operators with exact domains. Define $S (R^{4}; C^{4}) : = {F = (F_{0}, F_{1}, F_{2}, F_{3}) : F_{a} \in S (R^{4}) for a = 0, 1, 2, 3},$ with the finite-product topology generated by the scalar Schwartz seminorms on each component; $S (R^{4})$ and its seminorms are those of Schwartz/distribution spaces and Hilbert Fock conventions. For $F$ in this space, define $\hat{F} (t, k) = \int_{R^{3}} e^{- i k \cdot x} F (t, x) d^{3} x, u_{F} (k) = \int_{R} W_{D} (t, k) \hat{F} (t, k) d t .$ Then $u_{F} \in H_{D}$ , continuously in the Schwartz topology, and $Ψ (F) = c (P_{+} u_{F}) + c^{†} (\overline{P_{-} u_{F}})$ defines a bounded operator on $F_{a} (H_{+} \oplus \overline{H_{-}})$ , antilinear in $F$ . It satisfies ${Ψ (F), Ψ (G)} = 0, {Ψ (F), Ψ (G)^{†}} = ⟨ u_{F}, u_{G} ⟩_{H_{D}} I .$ The positive and negative contraction kernels, defined as tempered distributions by their Fourier integrals, are $C_{+} (τ, x) = \int e^{- i (ω τ - k \cdot x)} P_{+} (k) \frac{d^{3} k}{(2 π)^{3}}, C_{-} (τ, x) = \int e^{+ i (ω τ + k \cdot x)} P_{-} (k) \frac{d^{3} k}{(2 π)^{3}} .$ Their tested pairings give respectively $⟨ P_{+} u_{F}, P_{+} u_{G} ⟩$ and $⟨ P_{-} u_{F}, P_{-} u_{G} ⟩$ ; their sum is the anticommutator kernel $R$ below. Its tested free equation is $u_{(i \partial_{0} - h_{D} (- i \nabla)) F} = 0$ . For spatial Schwartz spinors $u, v$ , the equal-time field $Ψ_{t} (u) = c (P_{+} W_{D} (t, k) \hat{u}) + c^{†} (\overline{P_{-} W_{D} (t, k) \hat{u}})$ satisfies ${Ψ_{t} (u), Ψ_{t} (v)^{†}} = \int u (x)^{†} v (x) d^{3} x I$ and ${Ψ_{t} (u), Ψ_{t} (v)} = 0$ .

The spacetime anticommutator kernel is $R (τ, x) = \int_{R^{3}} W_{D} (- τ, k) e^{i k \cdot x} \frac{d^{3} k}{(2 π)^{3}} = \partial_{τ} Δ_{μ} (τ, x) I_{4} - i h_{D} (- i \nabla) Δ_{μ} (τ, x),$ where $Δ_{μ}$ is the scalar causal commutator distribution of Causal support of the scalar commutator distribution. Thus the kernel is supported in the closed causal cone. Spinor tests with compact spacelike-separated supports have vanishing anticommutators with one another and with each other's adjoints. Consequently, even polynomials in the bounded smeared fields commute across spacelike-separated regions. These are mathematical properties of the specified free-field construction.

Facts & Assumptions

Given: Countable Choice, the fixed $(-, +, +, +)$ metric and Fourier conventions, the explicit Dirac matrices and projections, the CAR Fock representation, the L1/L2 Fourier agreement, and the scalar causal commutator supplier.

[A1]

Countable Choice is the choice strength of the separable Fock and CAR suppliers. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

The scalar Schwartz space $S (R^{d})$ and its seminorms, second-variable-linear pairing and antisymmetric Fock conventions are those in Schwartz/distribution spaces and Hilbert Fock conventions.

[F2]

The Pauli matrices, $h_{D}$ , $P_{\pm}$ , $H_{\pm}$ , $W_{D} (t)$ , Clifford conventions, and conjugate Hilbert space are those in Dirac Clifford matrices and energy projections; by Dirac matrix identities and orthogonal energy projections the matrices are complementary orthogonal rank-two projections, $h_{D}$ is self-adjoint, and $W_{D}$ is unitary with $\partial_{t} W_{D} = i h_{D} W_{D}$ , while $H_{\pm}$ are closed separable Hilbert subspaces. Complex conjugation preserves separability, and the finite direct sum $K = H_{+} \oplus \overline{H_{-}}$ is separable by taking pairs from countable dense sets.

[F3]

Since $K$ is separable by [F2] and Countable Choice is assumed in [A1], the hypotheses of Bosonic and fermionic Fock operators with exact domains hold with $H = K$ . Its fermionic creation and annihilation operators are bounded, with ${c (h), c^{†} (k)} = ⟨ h, k ⟩ I$ and same-type anticommutators zero.

[F4]

In the negative-sign $2 π$ -normalized convention of Fourier transform agrees with l one and plancherel transforms, the Fourier transform preserves pairings on scalar Schwartz functions by the Plancherel theorem in that item's prerequisite chain. For each component, the transform $\hat{u} (k) = \int e^{- i k \cdot x} u (x) d^{3} x$ equals the $2 π$ -normalized transform evaluated at $k / (2 π)$ ; changing variables $k = 2 π ξ$ and summing components gives $\int {\hat{u}}^{†} \hat{v} d^{3} k / (2 π)^{3} = \int u^{†} v d^{3} x$ in the second-variable-linear pairing.

[F5]

The scalar distribution $Δ_{μ}$ is tempered, has support in ${(t, x) : ∣ x ∣ \leq ∣ t ∣}$ , and the scalar shell and causal conventions use $ω^{2} = ∣ k ∣^{2} + μ^{2}$ . Scalar future mass shell, invariant measure and test restriction Causal support of the scalar commutator distribution

[F6]

In the inertial coordinates, spacelike-separated compact supports have every pairwise difference outside the closed causal cone. Oriented time-oriented affine Minkowski space (the spacetime primitives) Inertial frames and inertial charts of the affine Minkowski model

[F7]

Absolutely integrable products may be rearranged by the sigma-finite Fubini theorem. Fubini's theorem for L^1 functions on a sigma-finite product

Proof

1.1F2givenalgebra

For every integer $N \geq 2$ , repeated integration by parts in $x$ gives $(1 + ∣ k ∣^{2})^{N} \hat{F} (t, k) = \hat{(1 - Δ_{x})^{N} F} (t, k)$ . Since $F$ is Schwartz, the right side is bounded by a finite Schwartz seminorm times $(1 + ∣ t ∣)^{- 2}$ . Thus $∣ \hat{F} (t, k) ∣ \leq C_{N} (F) (1 + ∣ t ∣)^{- 2} (1 + ∣ k ∣)^{- 2 N}$ . The matrix multiplier $W_{D} (t, k)$ is pointwise unitary by [F2]; integrating this bound in $t$ yields $∣ u_{F} (k) ∣ \leq C_{N}^{'} (F) (1 + ∣ k ∣)^{- 2 N}$ . This is square-integrable in three dimensions for $N \geq 2$ , with norm bounded by the displayed Schwartz seminorm, so $u_{F} \in H_{D}$ continuously.

1.2F2F3F4algebra

The equal-time CAR expansion gives ${Ψ_{t} (u), Ψ_{t} (v)^{†}} = \int \hat{u} (k)^{†} (P_{+} + P_{-}) \hat{v} (k) d^{3} k / (2 π)^{3}$ . By [F2] the sum is $I_{4}$ , and [F4] turns the integral into $\int u^{†} v d^{3} x$ . The same-type CAR vanish by [F3].

2.1A1F1F2F3step 1.1algebra

The first field term is antilinear in $F$ because $u_{F}$ is linear and $c$ is conjugate-linear; the second is antilinear because complex conjugation into $\overline{H_{-}}$ is conjugate-linear and $c^{†}$ is linear. Expanding the anticommutators with [F3], the only nonzero terms in ${Ψ (F), Ψ (G)^{†}}$ are the particle pairing $⟨ P_{+} u_{F}, P_{+} u_{G} ⟩$ and the conjugate negative-space pairing $⟨ \overline{P_{-} u_{G}}, \overline{P_{-} u_{F}} ⟩ = ⟨ P_{-} u_{F}, P_{-} u_{G} ⟩$ . Orthogonality and $P_{+} + P_{-} = I$ make their sum $⟨ u_{F}, u_{G} ⟩$ . The same-type anticommutator is zero because same-type CAR vanish within each species and the two species are orthogonal. Boundedness follows from $∥ Ψ (F) ∥ \leq ∥ P_{+} u_{F} ∥ + ∥ P_{-} u_{F} ∥ \leq \sqrt{2} ∥ u_{F} ∥$ .

2.2F2step 1.1givenalgebra

The spatial Fourier transform of $(i \partial_{0} - h_{D} (- i \nabla)) F$ is $i \partial_{t} \hat{F} - h_{D} (k) \hat{F}$ . Since $F$ is Schwartz, $W_{D} (t, k) \hat{F} (t, k)$ tends to zero as $t \to \pm \infty$ . Integration by parts and $\partial_{t} W_{D} = i h_{D} W_{D}$ give $\int W_{D} (t, k) i \partial_{t} \hat{F} d t = \int h_{D} W_{D} (t, k) \hat{F} d t$ , which cancels the second term in the definition of $u$ . Hence $u_{(i \partial_{0} - h_{D} (- i \nabla)) F} = 0$ . The matrix identity in [F2] identifies this with the stated tested Dirac equation.

2.3F2F3F5F7step 1.1algebra

The unsmeared CAR expansion gives the two separate kernels $C_{+}$ and $C_{-}$ displayed in the Statement: the positive term has coefficient $P_{+}$ and phase $e^{- i ω τ + i k \cdot x}$ , while the negative term has coefficient $P_{-}$ and phase $e^{+ i ω τ + i k \cdot x}$ . Their sum is $\int (P_{+} (\cos (ω τ) - i \sin (ω τ)) + P_{-} (\cos (ω τ) + i \sin (ω τ))) e^{i k \cdot x} d^{3} k / (2 π)^{3} = W_{D} (- τ, k)$ in Fourier form. Since $h_{D}^{2} = ω^{2} I_{4}$ , this equals $\partial_{τ} Δ_{μ} I_{4} - i h_{D} (- i \nabla) Δ_{μ}$ , using $\partial_{τ} (\sin ω τ / ω) = \cos ω τ$ . The equality is distributional: the shell weights grow at most polynomially and the test Fourier transforms decay rapidly, so the pairings converge absolutely and Fubini [F7] applies. Differential operators do not enlarge distributional support; [F5] therefore gives $supp R \subseteq {∣ x ∣ \leq ∣ τ ∣}$ .

3.1F1F2F3F5F6step 2.3algebra∎

If compact supports $K, L$ are spacelike separated, [F6] places the compact difference set $K - L$ outside $supp R$ . Pairing $R (x - y)$ with the product of any two supported spinor tests therefore gives ${Ψ (F), Ψ (G)^{†}} = 0$ . The field-field anticommutator vanishes for all tests independently: its same-type CAR terms vanish by [F3], and its mixed terms pair the orthogonal summands $H_{+}$ and $\overline{H_{-}}$ of $K$ , so their CAR scalar products are zero. Taking adjoints and interchanging $F, G$ gives the remaining cross anticommutators. Thus all field generators in the two spacelike-separated regions anticommute pairwise. Moving each of $r$ factors past each of $s$ factors contributes $(- 1)^{r s}$ ; when both monomials have even degree this sign is $+ 1$ . Finite sums of even monomials therefore commute, and norm limits preserve commutation because the generating fields are bounded.

Smeared free Dirac CAR fields and graded locality

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources