V-03 scaled radiative fields and single-mode conditions

Definition

Atlas_EinsteinMaxwell_NP_V03Mode

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

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

embRT, posPsi2F … negLF (ψ₂ = δΨ₀^ℂ, ψ₁ = √2 q̄ δΨ₁^ℂ, k = δκ^ℂ/(√2 q̄²), s = q δσ^ℂ/q̄²; ψ₋₂ = q̄⁴ δΨ₄^ℂ, ψ₋₁ = q̄³ δΨ₃^ℂ/√2, n = q q̄ δν^ℂ/√2, ℓ = q̄ δλ^ℂ/2), PosMode, NegMode, prefactors pref*. posPsi2F (III's ψ₂) is the scaled δΨ₀^ℂ, NOT the background NP scalar Ψ₂.

中文摘要 V-03 缩放辐射场与单模式条件。

Registry: PHYSICS_BOUNDARY §M (V-03) M7, M15.

Definition code

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Mode.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.NegMode, ExactVacuumAtlas.EinsteinMaxwell.NP.PosMode, ExactVacuumAtlas.EinsteinMaxwell.NP.embRT, ExactVacuumAtlas.EinsteinMaxwell.NP.negLF, ExactVacuumAtlas.EinsteinMaxwell.NP.negNF, ExactVacuumAtlas.EinsteinMaxwell.NP.negPsim1F, ExactVacuumAtlas.EinsteinMaxwell.NP.negPsim2F, ExactVacuumAtlas.EinsteinMaxwell.NP.posKF, ExactVacuumAtlas.EinsteinMaxwell.NP.posPsi1F, ExactVacuumAtlas.EinsteinMaxwell.NP.posPsi2F, ExactVacuumAtlas.EinsteinMaxwell.NP.posSF, ExactVacuumAtlas.EinsteinMaxwell.NP.prefK, ExactVacuumAtlas.EinsteinMaxwell.NP.prefL, ExactVacuumAtlas.EinsteinMaxwell.NP.prefN, ExactVacuumAtlas.EinsteinMaxwell.NP.prefPsi1, ExactVacuumAtlas.EinsteinMaxwell.NP.prefPsim1, ExactVacuumAtlas.EinsteinMaxwell.NP.prefPsim2, ExactVacuumAtlas.EinsteinMaxwell.NP.prefS
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_Bianchi
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_KNComm
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_KNWeyl
import Definitions.Def_Atlas_EinsteinMaxwell_NP_ModeOperators
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPBianchi
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPMaxwell
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPRicci
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPScalars
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Riemann
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03C3
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Cplx
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Family
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03LinKN
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03LinMx
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Realize
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Src
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Tan
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Var
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Local
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
import Definitions.Def_Hintz2026_Chiral
import Definitions.Def_Hintz2026_Core
import Definitions.Def_Hintz2026_Domain
import Definitions.Def_Hintz2026_System1
import Definitions.Def_Hintz2026_System4
/-!
# Atlas V-03 (block D, part 1): scaled fields, single-mode conditions, amplitude regularity

* Scaled four-dimensional fields from the complexified variations (V-03 dictionary; `q = qK = r + i a cos θ`,
  `q̄ = qbarK`): positive `ψ₂ = δΨ₀`, `ψ₁ = √2 q̄ δΨ₁`, `k = δκ/(√2 q̄²)`, `s = q δσ/q̄²`; negative
  `ψ₋₂ = q̄⁴ δΨ₄`, `ψ₋₁ = q̄³ δΨ₃/√2`, `n = q q̄ δν/√2`, `ℓ = q̄ δλ/2`. (`posPsi2F` is III's `PosFields.psi2`, the
  scaled `δΨ₀`; it is **not** the background `Ψ₂ = psi2`.)
* `PosMode` / `NegMode`: each scaled field equals `phaseP ω m · (amplitude ∘ toRT)` on `domKN` (class B; the
  amplitudes are arbitrary functions, never defined through `res1`).
* The amplitudes are then `C^∞` on III's `U p` (`PosMode.smooth`, `NegMode.smooth`): III's `PosSmooth`/`NegSmooth`
  are derived, not assumed. -/

open Complex Filter Topology
open scoped ComplexConjugate Matrix ContDiff
open ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.Variation
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del gKN giKN domReg domKN faradayKN)

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin

/-! ### Embedding of `(r, θ)` -/

/-- `(r, θ) ↦ (t, r, θ, φ) = (0, r, θ, 0)` (class B). -/
def embRT (z : Fin 2 → ℝ) : Pt 4 := ![0, z 0, z 1, 0]

/-! ### 2D product rule with a differentiable prefactor -/

/-! ### Scaled fields and the single-mode conditions -/

section defs

variable (p : Hintz2026.SubextremalKN) (τ : CTan)

/-- III's `PosFields.psi2` as a 4D field: `ψ₂ = δΨ₀^ℂ` (not the background `Ψ₂`). -/
noncomputable def posPsi2F (y : Pt 4) : ℂ := cPsi0 p.M p.a p.Q τ y
/-- `ψ₁ = √2 q̄ δΨ₁^ℂ`. -/
noncomputable def posPsi1F (y : Pt 4) : ℂ := ((Real.sqrt 2 : ℝ) : ℂ) * qbarK p.a y * cPsi1 p.M p.a p.Q τ y
/-- `k = δκ^ℂ / (√2 q̄²)`. -/
noncomputable def posKF (y : Pt 4) : ℂ := cKappa p.M p.a p.Q τ y / (((Real.sqrt 2 : ℝ) : ℂ) * qbarK p.a y ^ 2)
/-- `s = q δσ^ℂ / q̄²`. -/
noncomputable def posSF (y : Pt 4) : ℂ := qK p.a y * cSigma p.M p.a p.Q τ y / qbarK p.a y ^ 2
/-- `ψ₋₂ = q̄⁴ δΨ₄^ℂ`. -/
noncomputable def negPsim2F (y : Pt 4) : ℂ := qbarK p.a y ^ 4 * cPsi4 p.M p.a p.Q τ y
/-- `ψ₋₁ = q̄³ δΨ₃^ℂ / √2`. -/
noncomputable def negPsim1F (y : Pt 4) : ℂ := qbarK p.a y ^ 3 * cPsi3 p.M p.a p.Q τ y / ((Real.sqrt 2 : ℝ) : ℂ)
/-- `n = q q̄ δν^ℂ / √2`. -/
noncomputable def negNF (y : Pt 4) : ℂ := qK p.a y * qbarK p.a y * cNu p.M p.a p.Q τ y / ((Real.sqrt 2 : ℝ) : ℂ)
/-- `ℓ = q̄ δλ^ℂ / 2`. -/
noncomputable def negLF (y : Pt 4) : ℂ := qbarK p.a y * cLambda p.M p.a p.Q τ y / 2

/-- **Single-mode condition, positive branch** (class B): every scaled field is `phaseP ω m · (amplitude ∘ toRT)`
on `domKN`. -/
structure PosMode (om mm : ℝ) (F : Hintz2026.PosFields) : Prop where
  psi2 : ∀ y ∈ domKN p.M p.a p.Q, posPsi2F p τ y = phaseP om mm y * F.psi2 (toRT y)
  psi1 : ∀ y ∈ domKN p.M p.a p.Q, posPsi1F p τ y = phaseP om mm y * F.psi1 (toRT y)
  k : ∀ y ∈ domKN p.M p.a p.Q, posKF p τ y = phaseP om mm y * F.k (toRT y)
  s : ∀ y ∈ domKN p.M p.a p.Q, posSF p τ y = phaseP om mm y * F.s (toRT y)

/-- **Single-mode condition, negative branch** (class B). -/
structure NegMode (om mm : ℝ) (G : Hintz2026.NegFields) : Prop where
  psim2 : ∀ y ∈ domKN p.M p.a p.Q, negPsim2F p τ y = phaseP om mm y * G.psim2 (toRT y)
  psim1 : ∀ y ∈ domKN p.M p.a p.Q, negPsim1F p τ y = phaseP om mm y * G.psim1 (toRT y)
  n : ∀ y ∈ domKN p.M p.a p.Q, negNF p τ y = phaseP om mm y * G.n (toRT y)
  l : ∀ y ∈ domKN p.M p.a p.Q, negLF p τ y = phaseP om mm y * G.l (toRT y)

end defs

/-! ### Prefactors of the amplitudes and their `(r, θ)` derivatives (class B) -/

section pref

variable (p : Hintz2026.SubextremalKN)

local notation "rb" => Hintz2026.rhoBar p
local notation "rbs" => Hintz2026.rhoBarStar p
local notation "s2" => ((Real.sqrt 2 : ℝ) : ℂ)

/-- `δΨ₁ = P · (√2 ρ̄*)⁻¹ ψ₁`. -/ noncomputable def prefPsi1 (w : Fin 2 → ℝ) : ℂ := (s2 * rbs w)⁻¹
/-- `δκ = P · √2 ρ̄*² k`. -/ noncomputable def prefK (w : Fin 2 → ℝ) : ℂ := s2 * rbs w ^ 2
/-- `δσ = P · ρ̄*² ρ̄⁻¹ s`. -/ noncomputable def prefS (w : Fin 2 → ℝ) : ℂ := rbs w ^ 2 * (rb w)⁻¹
/-- `δΨ₄ = P · ρ̄*⁻⁴ ψ₋₂`. -/ noncomputable def prefPsim2 (w : Fin 2 → ℝ) : ℂ := (rbs w ^ 4)⁻¹
/-- `δΨ₃ = P · √2 ρ̄*⁻³ ψ₋₁`. -/ noncomputable def prefPsim1 (w : Fin 2 → ℝ) : ℂ := s2 * (rbs w ^ 3)⁻¹
/-- `δν = P · √2 (ρ̄ ρ̄*)⁻¹ n`. -/ noncomputable def prefN (w : Fin 2 → ℝ) : ℂ := s2 * (rb w * rbs w)⁻¹
/-- `δλ = P · 2 ρ̄*⁻¹ ℓ`. -/ noncomputable def prefL (w : Fin 2 → ℝ) : ℂ := 2 * (rbs w)⁻¹

variable {z : Fin 2 → ℝ} (hz : z ∈ Hintz2026.U p)
include hz

local notation "ds" => (I * ((p.a * Real.sin (z 1) : ℝ) : ℂ))

end pref

/-! ### Mode-field form of the complexified variations -/

section modeform

variable (p : Hintz2026.SubextremalKN) {τ : CTan} {om mm : ℝ}

local notation "rb" => Hintz2026.rhoBar p
local notation "rbs" => Hintz2026.rhoBarStar p
local notation "s2" => ((Real.sqrt 2 : ℝ) : ℂ)

end modeform

/-! ### Regularity of the complexified variations and of the amplitudes -/

section smooth

variable {M a Q : ℝ} {U : Set (Pt 4)} {τ : CTan}

variable (hτ : KNCTan M a Q U τ)
include hτ

end smooth

section amp

variable (p : Hintz2026.SubextremalKN) {τ : CTan} {om mm : ℝ}

variable (hτ : KNCTan p.M p.a p.Q (domKN p.M p.a p.Q) τ)
include hτ

end amp

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/V03Mode.lean; SHA-256 8e4b8e1a3467925c10c2fd5721cf8b99b42212988b78d23703870c2b3313f99a. 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