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 (). Let be a bounded open set, let be an open neighbourhood of its closure, let , and let and be smooth ( 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: denotes the components of in the standard basis, , , , and is the indicated contraction of the components of with the covector . Put and , the -dimensional Lebesgue integral of over . Then is a finite real number, and for every , with and : (a) the map is the quadratic polynomial , where and , so that its derivative at is ; (b) that first variation also equals ; (c) is stationary for , meaning that the derivative in (a) vanishes for every , if and only if for every on , all derivatives being classical partial derivatives of the smooth field . This is a pure mathematical statement about the functional : existence of a stationary field is not asserted, and identifying with the vacuum permeability, with a physical potential or with a physical action is a later physical model choice.
Conventions. Repeated Greek indices are summed over . With the matrix entries in the ordered basis one has , and denotes the entries of the inverse matrix; since is its own inverse, and (The Minkowski affine four-space: the form , causal cones, frames and Lorentz maps). Thus , the lowering map is the componentwise involution with inverse , and likewise for . For the zero extension to is smooth; denotes the map on , and denotes the Lebesgue integral of the zero extension of to (Integrable real and complex functions, and their integrals, Integral over a measurable subset).
Facts & Assumptions
Given: The Axiom of Countable Choice ; a bounded open set ; an open ; a real ; smooth maps ; the Minkowski form and conventions of [F1]; , , and ; and, for parts (a)-(c), a fixed with and .
Minkowski form and index conventions: has the ordered basis , the form is symmetric bilinear with matrix , 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).
Componentwise smoothness, compact support and zero extension: a map is smooth exactly when all its components are, a member of has compact support in the open and extends by zero to a smooth compactly supported map on , and constant-coefficient linear combinations of components preserve smoothness and compact support ( Euclidean maps and diffeomorphisms, Test function space d of an open set). Hence is a bijection of onto with inverse by [F1].
Cutoff functions, in ZF: for compact with open there is with and on a neighborhood of (Test function cutoffs and euclidean localization).
Compactness of the closure: is closed and, since is bounded, bounded; a closed bounded subset of is compact, with no choice principle (Heine-Borel in : with the Euclidean metric a subset of 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).
Integrability of continuous compactly supported functions: let be continuous with compact support . If then and ; otherwise 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), is bounded (A compact subset of a metric space is closed and bounded) and hence contained in a closed box with (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included), and gives (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 is integrable (Integrable real and complex functions, and their integrals). Under 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 is Lebesgue measurable); consequently, for a continuous on an open , the zero extension is Borel measurable, because for one has , open as is continuous on the open , while for it is the union of the closed set and that open set, and the rays generate the Borel sigma-algebra.
Signed integrals, monotonicity and linearity: for measurable real with at most one of , infinite one sets , and is integrable when both are finite; for nonnegative measurable the integral over a measurable set is ; if are nonnegative measurable then , and if then , while the zero function has integral ; on the integral is linear, (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 ).
Partial derivatives and their linearity: for a map on an open subset of , is the directional derivative in the standard direction (Directional derivatives and partial derivatives of a map ), and differentiation is linear, for a real constant (Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives), so componentwise.
Weak derivatives and the test identity, under : a real function of class on an open has each classical partial derivative locally integrable and equal to its weak derivative (Classical derivatives agree with weak derivatives), so for every test function the defining test identity of the weak derivative gives (Weak derivative of a locally integrable function).
Polynomial derivative: for real the polynomial function is differentiable at every real , and ; in particular , the term contributing and the term contributing (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, clause 4).
Fundamental variation lemma, under : if a continuous on an open satisfies for every , then on (The fundamental lemma of the calculus of variations for continuous coefficients).
Euclidean inner product: on , so for the arrays and (The Euclidean inner product on ).
Proof
The conventions of [F1] fix the index conventions of the Statement, and and are smooth on because is smooth and is constant; hence is smooth on . The closure is a compact subset of by [F4], so [F3] with and yields with and on .
The product , defined to be outside , is continuous with compact support, so by [F5]; since on , the nonnegative measurable functions and satisfy pointwise on , so [F6] gives ; hence is integrable over and is a finite real number.
The zero extension of to is smooth with compact support in by [F2], and for every real the map is smooth with components by [F1] and [F7]; every product below vanishes outside the compact set , so the corresponding integrands are continuous with compact support and integrable by [F5].
For every real and all one has and on , where and : the first identity is linearity of the partial derivative, and [F7], and the second follows by multiplying by the constant coefficients and collecting terms [F1].
Multiplying out with step 3.1 gives , and : the first equality renames the summation indices, and in the second one substitutes , relabels in the second sum and uses , so the two sums coincide. Since , the source term is , and therefore pointwise on with and .
The functions , , are integrable over by steps 2.1 and 2.2, so linearity of the integral [F6] applied to step 4.1 gives for every real ; thus is the polynomial with the finite real coefficients , and , and [F9] gives . This is (a).
For each fixed the functions , , are of class on the open by step 1.1, and by [F2]; applying [F8] to each of the four functions and summing over gives . Substituting this into step 5.1 and using linearity [F6] yields , which is (b).
Put ; each is continuous on by step 1.1, and by steps 5.1 and 6.1 the first variation of at in the direction equals , where and the pairing is that of [F11]. Assume first that is stationary, so that this first variation vanishes for every . Given any , [F2] provides with , so ; the fundamental variation lemma [F10] applied to the continuous array gives on , that is on for every .
Conversely, if on for every , then and steps 5.1 and 6.1 give vanishing first variation for every , so is stationary; hence stationarity is equivalent to the coefficient equation, which is (c). The point was arbitrary throughout, so (a)-(c) hold as stated; existence of a stationary field and the identifications of , and 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
The Minkowski affine four-space: the form , causal cones, frames and Lorentz maps
The Euclidean inner product on
Euclidean maps and diffeomorphisms
Directional derivatives and partial derivatives of a map
Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives
The fundamental lemma of the calculus of variations for continuous coefficients
Weak derivative of a locally integrable function
Classical derivatives agree with weak derivatives
The Lebesgue integral is linear on
A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
The Axiom of Countable Choice ()
Test function space d of an open set
Test function cutoffs and euclidean localization
Heine-Borel in : with the Euclidean metric a subset of 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
A compact subset of a metric space is closed and bounded
Continuous functions on Euclidean spaces are Borel measurable
The Borel sigma-algebra of a topological space
Assuming countable choice, every Borel subset of is Lebesgue measurable
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
Integral over a measurable subset
Integrable real and complex functions, and their integrals
For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term