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.
The Minkowski affine four-space: the form , causal cones, frames and Lorentz maps
Definition
Let and let be the set of all functions , with the pointwise vector-space structure of The vector space of all functions with pointwise operations, and as the case ; so is the function space of The vector space of all functions with pointwise operations, and as the case at and , and its elements are written with for , the components being indexed from and written with an upper index; the index conventions used throughout this item are fixed below. Let be the same set , whose elements are now called points, together with the map
given by pointwise addition of functions. Then the following three conditions hold.
- for all and all .
- for every .
- For all there is exactly one with , namely .
Conditions 1 and 2 are read at each of the four coordinates from the field axioms of , and condition 3 holds because satisfies coordinatewise while any with agrees with at every coordinate (Vector space over a field). A triple consisting of a set , a vector space and a map satisfying 1–3 is called an affine space with translation space ; the three conditions are its definition, so by 1–3 the set above is an affine space with translation space .
For let be given by for and for . Then is an ordered basis of (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis): every equals , because the two sides have the same value at each ; and if then evaluating at gives , so the list is linearly independent. We write and use the coordinate columns of Coordinate columns and matrices of linear maps relative to ordered bases with respect to this ordered basis.
The Minkowski form. Define
This is the standard bilinear form of The standard bilinear form on with the sign of the first coordinate reversed, together with the Euclidean inner product of The Euclidean inner product on on the last three coordinates; directly from the formula, for fixed the assignment is a linear combination of the component functions , hence linear, and similarly in , so is a bilinear form, and for all , so it is symmetric (Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms). Its matrix in the ordered basis is
and this matrix is its own inverse, the product of with itself being the identity matrix (Rectangular matrix multiplication and the identity matrix , including zero-sized shapes); in particular it is invertible, so is nondegenerate (The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space).
Index conventions. The components of a vector are the numbers in its expansion in the ordered basis , and for a linear map one writes for the components of and for the matrix entries, so that . Write , so that , and let denote the inverse matrix of , that is, when and when . The lowered components of are , and the operation is inverted by , because is its own inverse; explicitly and for . In these conventions for all .
Causal classification. Let with . Then is timelike when , null when , and spacelike when ; it is causal when . If the nonzero is causal, then : the inequality gives , and would force , hence and , contrary to the hypothesis. A nonzero causal is therefore future-directed when and past-directed when , and exactly one of these two alternatives holds for a nonzero real (Order on the reals). The future causal cone is
whose elements are exactly the future-directed causal vectors; the zero vector is not in , because it fails .
Orientation. The standard orientation of is the orientation class of the ordered basis (Orientation of a finite-dimensional real vector space).
Lorentz maps. A Lorentz map is a linear map (Linear map between vector spaces over the same field) that is invertible (Invertible linear maps, linear isomorphisms, and inverse linear maps) and satisfies
Writing for the matrix of in the ordered basis (Coordinate columns and matrices of linear maps relative to ordered bases), for its transpose (The transpose of a matrix), and also for the matrix , the condition is the matrix identity
Expanding and in the basis gives , whereas , and the two sides agree for all exactly when for every , since inserting the basis vectors , gives the converse (Rectangular matrix multiplication and the identity matrix , including zero-sized shapes). Equivalently, the matrix of in the basis is again ; this is the change-of-basis congruence of A basis change by changes the matrix of a bilinear form from to for the basis change from to its image under the invertible map . The invertibility requirement in the definition of a Lorentz map is in fact automatic: if satisfies the displayed identity and , then for every , so lies in the left radical of , which is because is nondegenerate; thus is injective, and an injective linear endomorphism of the four-dimensional space is surjective by Rank-nullity: together with If and is a linear subspace of , then is finite-dimensional, , and if and only if , so is a bijection, and its inverse is linear: for all and all reals , linearity of gives , and applying gives ; thus is invertible (Invertible linear maps, linear isomorphisms, and inverse linear maps). The map is proper when (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and on the zero space) and orthochronous when .
Frames. A frame of is a point together with an ordered basis of such that for all and . The coordinates of in that frame are the unique with ; uniqueness holds because is an ordered basis, and is the unique element of carrying to .
Tensors and components. For nonnegative integers , a tensor of type on is a map that is linear in each argument separately, where is the algebraic dual of Linear functionals and the algebraic dual . An empty product is a singleton, so a tensor is a scalar. Covectors are the case, a vector defines the tensor , and a two-form is a skew-symmetric tensor. These objects are maps, with arrays recording their components in a chosen basis.
Fix a frame and define its linear coordinate map by . It is invertible because is a basis, and by its defining pairings. For a Lorentz map , put , identifying its matrix with the linear map on . With origin fixed and new basis , the coordinates of the same point obey : indeed is equivalent to this identity. The basis is orthonormal since preserves , and it is a frame when is orthochronous, since then .
For a fixed vector , covector and two-form , let , and be their old component columns and matrix; primes denote the corresponding components in . Then
The vector law follows from . Substituting into and gives the other two laws by linearity and bilinearity. Equivalently, the coordinate functional is , the transpose operation of The transpose or algebraic adjoint , , of a linear map , and the coordinate bilinear form obeys . The geometric objects themselves are unchanged. In the standard frame , is the standard coordinate matrix of ; in a general frame it is .
Finally, a fixed positive real is separate extra structure: the coordinate has the dimension of length, and the time coordinate is . No physical claim is made here; in particular the identification of with physical spacetime, of with the future light cone, and of with the speed of light in vacuum are later physical premises.
Remarks
- Sign convention. The form has signature : with the index conventions of the Definition, is the time component and are the spatial components of ; the lowered time component carries the opposite sign, while for .
- What is not asserted. The affine space, the form, the cone and the transformation laws are mathematical data and conventions; the physical readings of these objects, and any statement that some physical trajectory or force equation has this form, are separate premises that this item does not supply.
Depends on
The vector space of all functions with pointwise operations, and as the case
Vector space over a field
Linear map between vector spaces over the same field
The Euclidean inner product on
The standard bilinear form on
Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms
The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space
The transpose or algebraic adjoint , , of a linear map
The transpose of a matrix
Rectangular matrix multiplication and the identity matrix , including zero-sized shapes
Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
Coordinate columns and matrices of linear maps relative to ordered bases
Invertible linear maps, linear isomorphisms, and inverse linear maps
A basis change by changes the matrix of a bilinear form from to
Orientation of a finite-dimensional real vector space
The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and on the zero space
Order on the reals
Linear functionals and the algebraic dual
Rank-nullity:
If and is a linear subspace of , then is finite-dimensional, , and if and only if