The time cone of a Hodge-definite pairing #
HodgeIndex.lean gives a DivisorSpace — a real vector space with a symmetric
pairing — and HodgeDefinite e, which says e² > 0 together with negative
definiteness on e^⊥. A pairing carrying that certificate is Lorentzian, and
this file records the structure that follows from it alone: the splitting of a
vector into a coordinate along e and a part orthogonal to e, the sign
identity that splitting produces, and the two inequalities that run opposite to
their Euclidean counterparts.
What is proved #
pair_self_eq_timeCoord_sq_add— the splitting identityx² = t(x)² + s(x)²for a unit reference vector, wherespacePart_self_nonposgivess(x)² ≤ 0. So the coordinate alongedominates:pair_self_le_timeCoord_sq.pair_mul_pair_le_sq— reverse Cauchy–Schwarz,x² · y² ≤ ⟨x, y⟩²wheneverx² > 0. The inequality points the other way from the Euclidean one, and it is immediate from the existingHodgeDefinite.of_pair_posandHodgeDefinite.toHodgeIndex: a vector of positive square carries its own Hodge certificate, andHodgeIndex.index_leat that vector is the statement.pair_pos_of_isFuture— two vectors of positive square with positive coordinate alongepair positively. The proof is elementary and avoids Cauchy–Schwarz one^⊥entirely: the explicit combinationt(y) • x - t(x) • yis orthogonal toe, so its square is nonpositive, and expanding that square is the inequality.sqrt_add_sqrt_le_sqrt_pair_add— the reverse triangle inequality, the statement the cone exists to carry.
What is not here #
No Lorentzian structure, class or certificate is introduced. HodgeDefinite e
is carried as a hypothesis on each theorem, so this file adds no new carrier and
nothing downstream has a new obligation. Unit normalization e² = 1 is likewise
a per-theorem hypothesis rather than a field; a caller with e² > 0 rescales.
Nothing here is named for Minkowski space, for special relativity, or for any
surface. IsFuture is a predicate on a pair of vectors in a real quadratic
space, and no claim is made that it is the set of ample classes of anything.
The diagonal model diag(1, -1, …, -1) and its Hodge certificate are a separate
concern and are not in this file.
Bilinearity of the pairing #
HodgeIndex.lean exposes pair with symmetry and the two zero lemmas, and
expands bilinearity inline where it needs it. These stay private: promoting
them is a change to the owner of pair, and the repository asks for two
independent consumers before a root moves.
The orthogonal splitting #
The coordinate of x along a reference vector e.
Instances For
The part of x orthogonal to a unit reference vector e.
Instances For
The splitting recovers the vector it split.
The space part is orthogonal to a unit reference vector.
The splitting identity: the square of a vector is the square of its
coordinate along a unit e plus the square of its space part.
The space part of any vector has nonpositive square.
The coordinate along e dominates the square.
Reverse Cauchy–Schwarz #
Reverse Cauchy–Schwarz. On a Hodge-definite pairing, a vector of positive square satisfies the Cauchy–Schwarz inequality with the sense reversed, against every other vector.
No unit normalization is needed: HodgeDefinite.of_pair_pos transports the
certificate from e to x, and HodgeIndex.index_le at x is the statement.
FiniteDimensional ℝ D is inherited from HodgeDefinite.of_pair_pos, which
routes through the signature theory of the associated quadratic form. It is
the only finite-dimensionality hypothesis in this file, and the future-cone
results below deliberately do not depend on it: sqrt_mul_sqrt_le_pair proves
the special case they need by an elementary argument instead.
The future cone #
x lies in the future cone of e: it has positive square and positive
coordinate along e.
This is a predicate on two vectors of a real quadratic space. It is not claimed to describe an ample cone, a positive cone, or any geometric locus.
Instances For
A positive multiple of a future vector is a future vector.
Two future vectors pair positively.
The witness is explicit: with a and b the coordinates of x and y along
e, the combination b • x - a • y is orthogonal to e, so Hodge definiteness
makes its square nonpositive. Expanding that square gives
b² x² + a² y² ≤ 2ab ⟨x, y⟩, and the left side is positive.
The future cone is closed under addition.
The reverse triangle inequality #
The product of the lengths of two future vectors is at most their pairing.
Proved from futureCombination_le and the arithmetic-geometric mean
inequality — in the form (b·A - a·B)² ≥ 0 for A, B the two lengths —
rather than from pair_mul_pair_le_sq, so that no finite-dimensionality
hypothesis reaches the reverse triangle inequality below.
The reverse triangle inequality. On a Hodge-definite pairing the length of a sum of future vectors is at least the sum of their lengths — the opposite of the Euclidean inequality.