The light cone is carried to itself

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.

Proposition

∀ e ∈ lightlike, ∀ b ∈ boosts, interval (boostT b.1 b.2 e.1 e.2) (boostX b.1 b.2 e.1 e.2) = 0

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_light_cone_is_carried_to_itself

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 reverse boost undoes the boost
• The reverse boost undoes every boost

All machine-checked theorems