Light is the fixed point

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.

LIGHT IS THE FIXED POINT OF COMPOSITION. Add any velocity to c and the result is c again — not approximately, not in a limit: the same fraction, exactly, at every sample. This is the sense in which c is not a speed among speeds but the fixed point of the operation that combines them.

Proposition

∀ v ∈ sample, same (add light v) light = true

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--light_is_the_fixed_point

Proved in the same file

• 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

All machine-checked theorems