Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableprecheck passjudge 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.

Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space

Definition

Let V be a 4-dimensional real vector space (Vector space over a field, Finite-dimensional vector space, and its dimension dim⁡FV; infinite-dimensional means having no finite basis). A Lorentz form on V is a symmetric bilinear form η:V×V→R (Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms) such that

  1. η is nondegenerate: both radicals rad⁡L(η)={u:η(u,v)=0 for every v} and rad⁡R(η)={v:η(u,v)=0 for every u} are {0} (The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space); and
  2. η has inertia (3,1,0): in some (equivalently, in every) basis of V in which the matrix of η is diagonal, exactly three diagonal entries are positive, exactly one is negative, and none is zero (Positive and negative definiteness, the inertia (p,q,r), rank p+q, and signature p−q of a real symmetric bilinear or quadratic form).

The inertia of a symmetric bilinear form is the triple (p,q,r) of numbers of positive, negative and zero diagonal entries of any diagonalizing basis, and it is independent of the diagonalizing basis by Sylvester's law of inertia (Positive and negative definiteness, the inertia (p,q,r), rank p+q, and signature p−q of a real symmetric bilinear or quadratic form); hence clause 2 is a property of η itself and not of a chosen basis. The associated quadratic form of η is

q(v):=η(v,v),v∈V.

A Lorentz vector space of signature (−,+,+,+) is a pair (V,η) consisting of a 4-dimensional real vector space V and a Lorentz form η on V; the name records that the diagonal normal form of η has one negative entry followed by three positive entries. No positive-definite structure on V is assumed or implied by this definition, and q takes both negative and positive values on nonzero vectors: a basis in which η is diagonal with diagonal entries −1,1,1,1 exists by clause 2, and on its first vector q is −1, while on each of the other three it is +1.

Depends on

Dependency tree · 2 levels

Sources