§2.2: $SL(2,\mathbb C)$ acts on $\mathbb R^{1,3}$ by Lorentz transformations

Proved

CelestialHolography.lorentzOfSL2C_preserves_minkowski

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

celestial-holographylorentz-groupmathematical-physics

For every $M\in SL(2,\mathbb C)$ and every $x\in\mathbb R^4$ , $\;\|\Lambda(M)x\|_\eta^2=\|x\|_\eta^2$ , where $\Lambda(M)x=V(M\,H(x)\,M^\dagger)$ . (Since $\det H(x)=-\|x\|^2_\eta$ and $\det M=1$ .)

Preamble

import Mathlib
import Definitions.Def_CelestialHolography_LorentzMobius_Defs

Formal statement

namespace CelestialHolography

theorem lorentzOfSL2C_preserves_minkowski (M : Matrix.SpecialLinearGroup (Fin 2) ℂ)
    (x : Fin 4 → ℝ) : minkowskiNormSq (lorentzOfSL2C M x) = minkowskiNormSq x := by sorry

end CelestialHolography

Source

F. Barzi, *Celestial Holography, A Hitchhiker's Guide to the Celestial Sphere*, arXiv:2608.07568v1 [hep-th], https://arxiv.org/abs/2608.07568

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as drafter

Non-blind read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It is not independent testimony and must not be mistaken for a blind audit; reviewers should compare it against the Lean code themselves.

For every complex $2\times2$ matrix $M$ with $\det M=1$ and every $x\in\mathbb R^4$ ,

-(y_0)^2+(y_1)^2+(y_2)^2+(y_3)^2=-(x_0)^2+(x_1)^2+(x_2)^2+(x_3)^2,\qquad y=V\bigl(M\,H(x)\,M^\dagger\bigr),

with $H(x)=\begin{pmatrix}x_0-x_3&x_1+ix_2\\x_1-ix_2&x_0+x_3\end{pmatrix}$ , $M^\dagger$ the conjugate transpose, and $V(X)=\bigl(\tfrac{\mathrm{Re}X_{00}+\mathrm{Re}X_{11}}2,\mathrm{Re}X_{01},\mathrm{Im}X_{01},\tfrac{\mathrm{Re}X_{11}-\mathrm{Re}X_{00}}2\bigr)$ .

View graph

§2.2: SL(2,C)SL(2,\mathbb C)SL(2,C) acts on R1,3\mathbb R^{1,3}R1,3 by Lorentz transformations

§2.2: $SL(2,\mathbb C)$ acts on $\mathbb R^{1,3}$ by Lorentz transformations