Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

Compact variations of the quadratic field functional: first variation and the coefficient equation

Statement

Assume the Axiom of Countable Choice (ACω). Let U⊆R4 be a bounded open set, let N⊆R4 be an open neighbourhood of its closure, let κ>0, and let A:N→V=R4 and J:N→V be smooth (Ck Euclidean maps and diffeomorphisms). Use the Minkowski form η and the index conventions of The Minkowski affine four-space: the form η, causal cones, frames and Lorentz maps: Aμ denotes the components of A in the standard basis, Aν:=ηνμAμ, Fμν:=∂μAν−∂νAμ, Fμν:=ημαηνβFαβ, and JνAν is the indicated contraction of the components of J with the covector Aν. Put L:=−14κFμνFμν+JνAν and S[A]:=∫UL dλ, the 4-dimensional Lebesgue integral of L over U. Then S[A] is a finite real number, and for every h∈Cc∞(U;V), with hν:=ηνμhμ and Gμν:=∂μhν−∂νhμ: (a) the map s↦S[A+sh] is the quadratic polynomial S[A]+s∫Uℓ1 dλ+s2∫Uℓ2 dλ, where ℓ1:=−κ−1Fμν∂μhν+Jνhν and ℓ2:=−14κGμνGμν, so that its derivative at s=0 is ∫U(−κ−1Fμν∂μhν+Jνhν)dλ; (b) that first variation also equals ∫U(κ−1∂μFμν+Jν)hν dλ; (c) A is stationary for S, meaning that the derivative in (a) vanishes for every h∈Cc∞(U;V), if and only if ∂μFμν=−κJν for every ν on U, all derivatives being classical partial derivatives of the smooth field A. This is a pure mathematical statement about the functional S: existence of a stationary field A is not asserted, and identifying κ with the vacuum permeability, A with a physical potential or S with a physical action is a later physical model choice.

Conventions. Repeated Greek indices are summed over {0,1,2,3}. With ημν:=η(eμ,eν) the matrix entries in the ordered basis (e0,e1,e2,e3) one has ημν=diag⁡(−1,1,1,1)μν, and ημν denotes the entries of the inverse matrix; since diag⁡(−1,1,1,1) is its own inverse, ημν=ημν and ημαηαν=δνμ (The Minkowski affine four-space: the form η, causal cones, frames and Lorentz maps). Thus Aν=ηνμAμ=(−A0,A1,A2,A3)ν, the lowering map m↦(mν)ν is the componentwise involution m↦(−m0,m1,m2,m3) with inverse mμ=ημνkν=(−k0,k1,k2,k3)μ, and likewise for h. For h∈Cc∞(U;V) the zero extension to N is smooth; A+sh denotes the map x↦A(x)+sh(x) on N, and ∫Uf dλ denotes the Lebesgue integral of the zero extension of f∣U to R4 (Integrable real and complex functions, and their integrals, Integral over a measurable subset).

Facts & Assumptions

Given: The Axiom of Countable Choice ACω; a bounded open set U⊆R4; an open N⊇U‾; a real κ>0; smooth maps A,J:N→V=R4; the Minkowski form η and conventions of [F1]; Fμν:=∂μAν−∂νAμ, Fμν:=ημαηνβFαβ, L:=−14κFμνFμν+JνAν and S[A]:=∫UL dλ; and, for parts (a)-(c), a fixed h∈Cc∞(U;V) with hν:=ηνμhμ and Gμν:=∂μhν−∂νhμ.

[F1]

Minkowski form and index conventions: V=R4 has the ordered basis e0,…,e3, the form η(v,w)=−v0w0+v1w1+v2w2+v3w3 is symmetric bilinear with matrix diag⁡(−1,1,1,1), that matrix is its own inverse, and nondegeneracy and the tensor-component transformation are as stated there (The Minkowski affine four-space: the form η, causal cones, frames and Lorentz maps).

[F2]

Componentwise smoothness, compact support and zero extension: a map is smooth exactly when all its components are, a member of Cc∞(U;V) has compact support in the open U and extends by zero to a smooth compactly supported map on N, and constant-coefficient linear combinations of components preserve smoothness and compact support (Ck Euclidean maps and diffeomorphisms, Test function space d of an open set). Hence h↦(hν)ν is a bijection of Cc∞(U;V) onto Cc∞(U;R4) with inverse k↦mμ:=ημνkν by [F1].

[F3]

Cutoff functions, in ZF: for compact K⊆Ω⊆R4 with Ω open there is χ∈Cc∞(Ω) with 0≤χ≤1 and χ=1 on a neighborhood of K (Test function cutoffs and euclidean localization).

[F4]

Compactness of the closure: U‾ is closed and, since U is bounded, bounded; a closed bounded subset of R4 is compact, with no choice principle (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F5]

Integrability of continuous compactly supported functions: let F:R4→R be continuous with compact support K. If K=∅ then F=0 and ∫F dλ=0; otherwise M:=max⁡K∣F∣ is a finite real number (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), K is bounded (A compact subset of a metric space is closed and bounded) and hence contained in a closed box Q with λ(Q)<+∞ (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included), and ∣F∣≤MχQ gives ∫∣F∣ dλ≤∫MχQ dλ=Mλ(Q)<+∞ (Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions, The integral of a nonnegative simple function), so F is integrable (Integrable real and complex functions, and their integrals). Under ACω every continuous map between Euclidean spaces is Borel measurable (Continuous functions on Euclidean spaces are Borel measurable), the Borel sigma-algebra is generated by the open sets (The Borel sigma-algebra of a topological space) and every Borel set is Lebesgue measurable (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable); consequently, for a continuous f on an open G⊆R4, the zero extension fχG is Borel measurable, because for a≥0 one has {fχG>a}=G∩{f>a}, open as f is continuous on the open G, while for a<0 it is the union of the closed set R4∖G and that open set, and the rays (a,+∞) generate the Borel sigma-algebra.

[F6]

Signed integrals, monotonicity and linearity: for measurable real f with at most one of ∫f+, ∫f− infinite one sets ∫f dλ:=∫f+dλ−∫f−dλ, and f is integrable when both are finite; for nonnegative measurable f the integral over a measurable set E is ∫Ef dλ=∫fχE dλ; if 0≤f≤h are nonnegative measurable then ∫f dλ≤∫h dλ, and if c>0 then ∫cf dλ=c∫f dλ, while the zero function has integral 0; on L1 the integral is linear, ∫(αf+βg) dλ=α∫f dλ+β∫g dλ (Integrable real and complex functions, and their integrals, Integral over a measurable subset, Monotonicity and nonnegative homogeneity of the nonnegative integral, The Lebesgue integral is linear on L1(μ)).

[F7]

Partial derivatives and their linearity: for a map on an open subset of R4, ∂μ is the directional derivative in the standard direction eμ (Directional derivatives and partial derivatives of a map U⊆Rm→Rn), and differentiation is linear, D(f+cg)=Df+cDg for a real constant c (Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives), so ∂μ(f+cg)=∂μf+c ∂μg componentwise.

[F8]

Weak derivatives and the test identity, under ACω: a real function u of class C1 on an open Ω⊆Rn has each classical partial derivative ∂μu locally integrable and equal to its weak derivative (Classical derivatives agree with weak derivatives), so for every test function ψ∈Cc∞(Ω;R) the defining test identity of the weak derivative gives ∫Ωu ∂μψ dλ=−∫Ω(∂μu)ψ dλ (Weak derivative of a locally integrable function).

[F9]

Polynomial derivative: for real a0,a1,a2 the polynomial function P(s)=a0+a1s+a2s2 is differentiable at every real c, and P′(c)=a1+2a2c; in particular P′(0)=a1, the term a0 contributing 0 and the term a2s2 contributing 2a2c (For a natural n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(n) x−n−1; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, clause 4).

[F10]

Fundamental variation lemma, under ACω: if a continuous g:U→Rm on an open U⊆Rn satisfies ∫U⟨g,k⟩ dλ=0 for every k∈Cc∞(U;Rm), then g=0 on U (The fundamental lemma of the calculus of variations for continuous coefficients).

[F11]

Euclidean inner product: ⟨x,y⟩=∑i<mxiyi on Rm, so ∑νCνhν=⟨C,k⟩ for the arrays C=(C0,…,C3) and k=(h0,…,h3) (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn).

Proof

technique · direct; expand the functional along a compactly supported variation, move the derivative onto the coefficient with the weak-derivative test identity, and read off the coefficient equation with the fundamental variation lemma
1.1givenF1F3F4

The conventions of [F1] fix the index conventions of the Statement, and x↦Fμν(x) and x↦Fμν(x) are smooth on N because A is smooth and ημαηνβ is constant; hence L is smooth on N. The closure U‾ is a compact subset of N by [F4], so [F3] with Ω:=N and K:=U‾ yields χ∈Cc∞(N) with 0≤χ≤1 and χ=1 on U‾.

2.1step 1.1F5F6

The product Lχ, defined to be 0 outside supp⁡χ, is continuous with compact support, so ∫R4∣Lχ∣ dλ<+∞ by [F5]; since χ=1 on U, the nonnegative measurable functions ∣L∣χU and ∣L∣χ satisfy ∣L∣χU≤∣L∣χ pointwise on R4, so [F6] gives ∫U∣L∣ dλ≤∫R4∣Lχ∣ dλ<+∞; hence L is integrable over U and S[A]=∫UL dλ is a finite real number.

2.2step 1.1F1F2F5F7

The zero extension of h to N is smooth with compact support in U by [F2], and for every real s the map A+sh:N→V is smooth with components (A+sh)ν=Aν+shν by [F1] and [F7]; every product below vanishes outside the compact set supp⁡h⊆U, so the corresponding integrands are continuous with compact support and integrable by [F5].

3.1step 2.2F1F7

For every real s and all μ,ν one has F(s)μν=Fμν+sGμν and F(s)μν=Fμν+sGμν on U, where F(s)μν:=∂μ(A+sh)ν−∂ν(A+sh)μ and F(s)μν:=ημαηνβF(s)αβ: the first identity is linearity of the partial derivative, ∂μ(Aν+shν)=∂μAν+s∂μhν and ∂ν(Aμ+shμ)=∂νAμ+s∂νhμ [F7], and the second follows by multiplying by the constant coefficients ημαηνβ and collecting terms [F1].

4.1step 3.1algebra

Multiplying out with step 3.1 gives F(s)μνF(s)μν=FμνFμν+2sFμνGμν+s2GμνGμν, and FμνGμν=FμνGμν=2Fμν∂μhν: the first equality renames the summation indices, and in the second one substitutes Gμν=∂μhν−∂νhμ, relabels μ↔ν in the second sum and uses Fνμ=−Fμν, so the two sums coincide. Since (A+sh)ν=Aν+shν, the source term is Jν(A+sh)ν=JνAν+sJνhν, and therefore L(A+sh)=L+sℓ1+s2ℓ2 pointwise on U with ℓ1=−κ−1Fμν∂μhν+Jνhν and ℓ2=−14κGμνGμν.

5.1step 2.1step 2.2step 4.1F6F9

The functions L, ℓ1, ℓ2 are integrable over U by steps 2.1 and 2.2, so linearity of the integral [F6] applied to step 4.1 gives S[A+sh]=∫U(L+sℓ1+s2ℓ2) dλ=S[A]+s∫Uℓ1 dλ+s2∫Uℓ2 dλ for every real s; thus s↦S[A+sh] is the polynomial P(s)=a0+a1s+a2s2 with the finite real coefficients a0=S[A], a1=∫Uℓ1 dλ and a2=∫Uℓ2 dλ, and [F9] gives P′(0)=a1=∫U(−κ−1Fμν∂μhν+Jνhν)dλ. This is (a).

6.1step 5.1F2F6F8

For each fixed ν the functions x↦Fμν(x), μ=0,1,2,3, are of class C1 on the open U by step 1.1, and hν∈Cc∞(U;R) by [F2]; applying [F8] to each of the four functions and summing over μ gives ∫UFμν∂μhν dλ=−∫U(∂μFμν)hν dλ. Substituting this into step 5.1 and using linearity [F6] yields ∫Uℓ1 dλ=∫U(κ−1∂μFμν+Jν)hν dλ, which is (b).

7.1step 5.1step 6.1F2F10F11

Put Cν:=κ−1∂μFμν+Jν; each Cν is continuous on U by step 1.1, and by steps 5.1 and 6.1 the first variation of S at A in the direction h equals ∫UCνhν dλ=∫U⟨C,k⟩ dλ, where k:=(hν)ν∈Cc∞(U;R4) and the pairing is that of [F11]. Assume first that A is stationary, so that this first variation vanishes for every h∈Cc∞(U;V). Given any k∈Cc∞(U;R4), [F2] provides h∈Cc∞(U;V) with hν=kν, so ∫U⟨C,k⟩ dλ=0; the fundamental variation lemma [F10] applied to the continuous array C gives C=0 on U, that is ∂μFμν=−κJν on U for every ν.

8.1step 5.1step 6.1step 7.1given∎

Conversely, if ∂μFμν=−κJν on U for every ν, then C=0 and steps 5.1 and 6.1 give vanishing first variation for every h∈Cc∞(U;V), so A is stationary; hence stationarity is equivalent to the coefficient equation, which is (c). The point h∈Cc∞(U;V) was arbitrary throughout, so (a)-(c) hold as stated; existence of a stationary field A and the identifications of κ, A and J with physical quantities are not asserted, and the Axiom of Countable Choice entered only through [F5], [F8] and [F10], the expansions of steps 3.1-5.1 being choice-free.

Depends on

Dependency tree · 2 levels

Sources