Velocity addition below c
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.
TWO BOOSTS BELOW c COMPOSE TO A BOOST BELOW c, for every pair — c is not approached by adding.
Proposition
(p₁ q₁ p₂ q₂ : Int) (h₁ : belowC p₁ q₁) (h₂ : belowC p₂ q₂) : belowC (addNum p₁ q₁ p₂ q₂) (addDen p₁ q₁ p₂ q₂)Proof
By obtain ⟨a, b, c⟩ := h₁; obtain ⟨d, e, f⟩ := 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--velocity_addition_below_c
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
- Timelike invariant
- Spacelike invariant
- Null invariant
- Timelike order absolute
- Spacelike order reverses
- Spacelike simultaneous