V-02 q as a function of (r, θ)
DefinitionAtlas_EinsteinMaxwell_NP_KNCommeinstein-maxwellexact-spacetime-atlas-vexact-vacuum-atlasgeneral-relativitynewman-penrose
V-02 q as a function of (r, θ)
qrt (r, θ) = r + i a cos θ (notation).
中文摘要 V-02 q 的 (r,θ) 函数。
Registry: PHYSICS_BOUNDARY §L (V-02) L13.
Definition code
-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/KNComm.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.qrt
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
/-!
# Atlas V-02 (C, part 2): Kerr–Newman frame derivatives, commutators and `cL`
All frame components of V-01's Kinnersley frame depend only on `(r, θ) = (x 1, x 2)`. This file computes the
genuine slice derivatives (`HasDerivAt`, no junk values) of the non-constant components, the commutators
`[e_A, e_B]` for `(A, B) = (l, n), (l, m), (n, m), (m, m̄)` and the lowered commutator coefficients
`cL C A B = g(e_C, [e_A, e_B])` for these pairs (the remaining pairs follow from antisymmetry and the reality
relation `cL_swap`). Everything holds on IV's `domReg` for every real `M, a, Q`.
Notation in statements: `q = qK a x = r + i a cos θ`, `q̄ = qbarK a x`, `√2` is `((Real.sqrt 2 : ℝ) : ℂ)`.
-/
open Real Complex
open scoped ComplexConjugate
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del gKN domReg)
namespace ExactVacuumAtlas.EinsteinMaxwell.NP
attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin
/-- `q` as a function of `(r, θ)`. -/
noncomputable def qrt (a r θ : ℝ) : ℂ := ((r : ℝ) : ℂ) + I * ((a * Real.cos θ : ℝ) : ℂ)
/-! ### One-variable derivatives -/
section deriv
variable (M a Q : ℝ)
variable {M a Q}
end deriv
/-! ### Frame components as functions of `(r, θ)` and their derivatives -/
section comps
variable {M a Q : ℝ} {x : Pt 4}
end comps
/-! ### Algebraic facts used by the closed-form computations -/
/-! ### Lowered frame covectors in closed form -/
section cov
variable {M a Q : ℝ} {x : Pt 4}
end cov
/-! ### Derivatives of the frame components -/
section dcomp
variable {M a Q : ℝ} {x : Pt 4}
end dcomp
/-! ### Lowered commutator coefficients `cL C A B = g(e_C, [e_A, e_B])` -/
section cLval
variable {M a Q : ℝ} {x : Pt 4}
end cLval
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/KNComm.lean; SHA-256 bc2e5a3ee1709b32fe1e8fb95d154f3b7f3f2e4d32ee7305fe1e8d05012f1b43. 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.