Prove2Me

The KN Kinnersley frame is a null frame

Proved
ExactVacuumAtlas.EinsteinMaxwell.NP.nullFrameData_KN

by He Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-vexact-vacuum-atlasgeneral-relativitynewman-penrose

The KN Kinnersley frame is a null frame

NullFrameData for gKN, giKN, knE, knTh on domReg (every real M, a, Q).

Scope. Exactly the hypotheses printed in the formal statement.

中文摘要 KN Kinnersley 标架满足零标架条件。

Preamble
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Domain
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_NP_CCalc
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameConn
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameNull
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFaraday
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFrame
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNSpin
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Riemann
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
open Real Complex
open scoped ComplexConjugate Matrix ContDiff
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del gKN giKN faradayKN domReg)
Formal statement
theorem ExactVacuumAtlas.EinsteinMaxwell.NP.nullFrameData_KN (M a Q : ℝ) :
    NullFrameData (gKN M a Q) (giKN M a Q) (knE M a Q) (knTh M a Q) (domReg M a Q) := by sorry
Source
He Wang, Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation Systems. Local source, no public repository; commit b8cd107a558e153ed41fb4972ac5315499d14778; Atlas/EinsteinMaxwell/NP/KNSpin.lean#L100-L111; SHA-256 296633d32af53ca44cec2982a7dc3dc99a1cb3e71bd617f51817c313623dfb02. Registered definitions: mission/PHYSICS_BOUNDARY.md (§K–§M); literature: P. Hintz, arXiv:2609.33661 (v1); Mark–Yang–Zimmerman–Chen, arXiv:1409.5800 (v1).
Human review

  • Endorsed by Shuze Chen · Oct 24, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 24, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph