The reverse boost undoes the boost
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
THE BOOST IS UNDONE BY THE REVERSE BOOST. Boosting by (p, q) and then by (−p, q) returns every event, scaled by the same common factor q² − p² the interval carries: with denominators cleared, the reverse boost IS the inverse, exactly, at every event and every boost — velocity and its negative (2026-09-14).
Proposition
∀ e ∈ events, ∀ b ∈ boosts, boostT (-b.1) b.2 (boostT b.1 b.2 e.1 e.2) (boostX b.1 b.2 e.1 e.2) = (b.2 * b.2 - b.1 * b.1) * e.1 ∧ boostX (-b.1) b.2 (boostT b.1 b.2 e.1 e.2) (boostX b.1 b.2 e.1 e.2) = (b.2 * b.2 - b.1 * b.1) * e.2Proof
By decide in spacetime.lean. Checked by the Lean kernel: it depends on no 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--the_reverse_boost_undoes_the_boost
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 every boost
- Sq lt
- Lt of sq
- Interval scales
- Scale positive
- Timelike invariant
- Spacelike invariant
- Null invariant
- Timelike order absolute
- Spacelike order reverses
- Spacelike simultaneous
- Velocity addition below c