Timelike invariant
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and resting on no axiom beyond propext and Quot.sound. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
TIMELIKE STAYS TIMELIKE in every frame below c.
Proposition
(p q t x : Int) (h : belowC p q) (ht : 0 < interval t x) : 0 < interval (boostT p q t x) (boostX p q t x)Proof
By have hs := scale_positive p q h in spacetime.lean. Checked by the Lean kernel: it rests on Quot.sound and propext and on no other axiom.
Sources and identifiers
- Lean source · src/pair/formal/proofs/spacetime.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
- Deposit record ·
spacetime--timelike_invariant
Proved in the same file
- Light is the fixed point
- Light is fixed from either side
- Rest is the identity
- Composition is symmetric
- Below c composes to below c
- The boost preserves the interval
- The light cone is carried to itself
- The reverse boost undoes the boost
- The reverse boost undoes every boost
- Sq lt
- Lt of sq
- Interval scales
- Scale positive
- Spacelike invariant
- Null invariant
- Timelike order absolute
- Spacelike order reverses
- Spacelike simultaneous
- Velocity addition below c