V-01 Faraday NP scalars of the KN background
DefinitionAtlas_EinsteinMaxwell_NP_KNFaradayeinstein-maxwellexact-spacetime-atlas-vexact-vacuum-atlasgeneral-relativitynewman-penrose
V-01 Faraday NP scalars of the KN background
phi0K = F(l,m), phiC = ½(F(l,n) + F(m̄,m)), phi2K = F(m̄,n) for F = faradayKN (bilinear).
中文摘要 V-01 KN 背景 Faraday NP 标量。
Registry: PHYSICS_BOUNDARY §K (V-01) K4.
Definition code
-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/KNFaraday.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.phi0K, ExactVacuumAtlas.EinsteinMaxwell.NP.phi2K, ExactVacuumAtlas.EinsteinMaxwell.NP.phiC
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_KNFrame
import Definitions.Def_Atlas_Kerr_InAtoms
/-! # Kinnersley-frame projections of the Kerr–Newman Faraday field (ATLAS-V-01)
IV's `KN.faradayKN a Q` (from the potential `A = −(Qr/Σ)(dt − a sin²θ dφ)`, `F = dA` proved in IV) is used unchanged; no
constant is rescaled. `F(u, v) = Σ F_{μν} u^μ v^ν` is the complex-**bilinear** contraction `ccontr`.
On `domReg M a Q`, every real `M a Q` (`a = 0`, `Q = 0` allowed):
F(l,n) = Q(r² − a²cos²θ)/Σ², F(m,m̄) = −2i Q a r cosθ/Σ²,
F(l,m) = F(l,m̄) = F(n,m) = F(n,m̄) = 0,
and the full 4×4 frame matrix follows by antisymmetry (`faraday_frame`). With Hintz's convention
`Φ₀ = F₁₃ = F(l,m)`, `Φ₁ = ½(F₁₂ + F₄₃) = ½(F(l,n) + F(m̄,m))`, `Φ₂ = F₄₂ = F(m̄,n)` (arXiv:2609.33661v1, archived HTML;
see `notes/ATLAS_V_SOURCE_DICTIONARY.md`) we define the raw contractions `phi0K`, `phiC`, `phi2K` and prove
`Φ₀ = Φ₂ = 0`, `phiC = Q/(2 q̄²)` (the value stated in the source, `q̄ = ρ̄*`), `phiC ≠ 0` iff `Q ≠ 0`. The name `phiC`
marks a local definition (formula above), not a claim about other references' `φ₁` normalisation. -/
open Real
open scoped ComplexConjugate Matrix
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del faradayKN domReg)
namespace ExactVacuumAtlas.EinsteinMaxwell.NP
attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin
/-! ### Real contractions -/
section RealF
variable {M a Q : ℝ} {x : Pt 4}
end RealF
/-! ### The six independent frame components -/
section Frame
variable {M a Q : ℝ} {x : Pt 4}
end Frame
/-! ### Maxwell scalars in Hintz's convention (raw contractions) -/
/-- `Φ₀ = F₁₃ = F(l, m)`. -/
noncomputable def phi0K (M a Q : ℝ) (x : Pt 4) : ℂ := ccontr (faradayKN a Q) x (knL M a Q x) (knM a x)
/-- `Φ₁ = ½(F₁₂ + F₄₃) = ½(F(l,n) + F(m̄,m))` — local name `phiC` (see module docstring). -/
noncomputable def phiC (M a Q : ℝ) (x : Pt 4) : ℂ :=
(ccontr (faradayKN a Q) x (knL M a Q x) (knN M a Q x) + ccontr (faradayKN a Q) x (knMbar a x) (knM a x)) / 2
/-- `Φ₂ = F₄₂ = F(m̄, n)`. -/
noncomputable def phi2K (M a Q : ℝ) (x : Pt 4) : ℂ := ccontr (faradayKN a Q) x (knMbar a x) (knN M a Q x)
section Scalars
variable {M a Q : ℝ} {x : Pt 4}
end Scalars
end ExactVacuumAtlas.EinsteinMaxwell.NP
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/KNFaraday.lean; SHA-256 cab1226e82c48431de6bcae27caa3784dedabf5a67e7c2bb040fee2dce482b03. 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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.