The boost preserves the interval

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided 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 INTERVAL IS INVARIANT UP TO THE ONE COMMON FACTOR. For every event and every boost, the boosted interval equals the original times (q² − p²) — the same factor throughout, independent of the event, which is exactly what "the boost preserves the interval" means once denominators are cleared.

Proposition

∀ e ∈ events, ∀ b ∈ boosts, interval (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) * interval e.1 e.2

Proof

By decide in spacetime.lean. The kernel reduces the proposition and reports no axiom dependency.

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_boost_preserves_the_interval

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 light cone is carried to itself
• The reverse boost undoes the boost
• The reverse boost undoes every boost

All machine-checked theorems