GPPVerify: Lean 4 Formalization of the ONON Framework

4 Shadow Symmetry = Time Reversal

4.1 The Three-Step Proof

Theorem 4.1 Shadow is Involution
#

The map \(\Delta \mapsto 2-\Delta \) has order \(2\).

Theorem 4.2 Penrose Antipodal from Hodge Star
#

The orthogonal complement \(\Lambda \mapsto \Lambda ^\perp \) on \(\mathrm{Gr}(2,4)\) acts as the antipodal map on \(S^2\) via the Penrose correspondence.

Theorem 4.3 Antipodal Forces Energy Inversion
#

Under \(\Lambda \mapsto \Lambda ^\perp \), the symplectic normalisation forces \(\omega \mapsto \omega ^{-1}\).

Theorem 4.4 Shadow = Time Reversal
#

On the principal series \(\Delta = 1+i\lambda \), time reversal \(T\) sends \(\Delta \mapsto 2-\Delta \): the shadow transform. (Most-cited result in ONON52: 16 cross-references.)

Theorem 4.5 Canonical Dictionary \(\Delta = 2s\)

Under \(\Delta = 2s\), shadow \(\Delta \leftrightarrow 2-\Delta \) is the functional equation \(s \leftrightarrow 1-s\).

Theorem 4.6 Critical Lines Coincide
#

\(\mathrm{Re}(\Delta ) = 1\) under \(\Delta = 2s\) gives \(\mathrm{Re}(s) = \tfrac {1}{2}\).