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.
Static electrostatic test-energy first integral
Example
Let be open and let , assigned volts in SI bookkeeping. On with Minkowski metric, orientation , future time-orientation , and length coordinate , take the static one-form and . Let be an open interval with nonempty interior (Intervals of : the nine order-convex forms, nondegeneracy, and length) and let be an existing future-timelike curve parametrized by proper time in the sense of Timelike worldlines, proper time, length and four-velocity on a Lorentzian four-manifold, with , , and for constants and , assigned kilograms and coulombs respectively. Write , , and .
Facts & Assumptions
Given: The stated Minkowski metric and static potential, a supplied timelike curve satisfying the Lorentz-force equation, and the constants .
Smooth formal matter, EM tensors and observer quantities: a local potential is a supplied one-form with ; .
Killing exchange current and gauge-compensated charged first integral: if is Killing, , and the supplied curve satisfies , then is constant. Its current stress clause remains conditionally open at its draft Maxwell-stress supplier; this example uses only the separate test-particle clause at its exact interface.
Timelike worldlines, proper time, length and four-velocity on a Lorentzian four-manifold: proper-time parametrization of a future-timelike curve gives ; this normalization is also stated explicitly in the Example.
The metric and potential are prescribed; the curve is assumed to exist in . No self-field or coupled-field existence claim is included.
Verification
The vector field is Killing because the Minkowski components are constant. The potential is independent of , so with . The hypotheses of the test-particle clause in [F2] are exactly those in the Example.
Put , so and . The normalization gives ; because the curve is future-directed, , hence and . Thus , while . The conserved scalar is , and multiplying by gives the conserved energy expression .
Remarks
This is a test-particle first integral in a prescribed static background. It does not assert that Minkowski space with nonzero solves the coupled Einstein equation. The expression uses kinetic momentum and the stated potential gauge; general gauge changes are covered by the compensator in the supplier theorem.
Depends on
Dependency tree · 2 levels
Sources
- Sean M. Carroll, Lecture Notes on General Relativity, arXiv:gr-qc/9712019v1 (1997), Ch. 5, equations (5.41)–(5.43), PDF pp. 146–147 (printed pp. 140–141)
- David Tong, General Relativity, full author-hosted lecture notes, 2019, §§4.3 and 4.5.5, PDF pp. 166–169 and 194–196 (printed pp. 159–162 and 187–189)