Explicit RN tangents
DefinitionAtlas_EinsteinMaxwell_Variation_RNeinstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity
Explicit RN tangents
tanRN Q m q (h_vv = 2m/r − 2Qq/r²), tanFRN q (f_vr = −q/r², f_rv = q/r²), tanB (h_vv = −1/r²), domJ = ℝ × domRN.
中文摘要 RN 显式切向与非零检验方向。
Registry: PHYSICS_BOUNDARY §J (J19).
Definition code
-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Variation/RN.lean
-- definition bundle: kept ExactVacuumAtlas.Variation.RN.domJ, ExactVacuumAtlas.Variation.RN.tanB, ExactVacuumAtlas.Variation.RN.tanFRN, ExactVacuumAtlas.Variation.RN.tanRN
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_RN_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_RN_Frame
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_Transport_MatrixCalc
/-! # Reissner–Nordström (ingoing EF): parameter tangents and the nonzero test (ATLAS-IV-03)
Data `gRN M b`, `giRN M b`, `faradayRN Q`, `domRN = {r > 0, 0 < θ < π}` of IV-01, unchanged.
* **Parameter tangents** (`param_tangent`): for every real `M, Q` and every direction `(m, q)` (mass and
charge, or any real combination; `M = 0`, `Q = 0`, `m = 0`, `q = 0` allowed, no division by `Q`), the
actual family `ε ↦ (gRN (M+εm) ((Q+εq)²), giRN …, faradayRN (Q+εq))` is a `FamilyData` on
`ℝ × domRN`, each member is certified (`EF.cert`), and its genuine tangent is the explicit
`tanRN M Q m q` (only `h_vv = 2m/r - 2Qq/r²`) and `tanFRN q` (`f_rv = q/r² = -f_vr`). The bridge gives
`LE = LJ = LH = 0` for this tangent on `domRN`.
* **Nonzero test** (`nonzero_theta`): the off-shell family `b = Q² + ε` (`M`, `Q`, `F` fixed) has the actual
tangent `tanB` (`h_vv = -1/r²`, all other components `0`) and `f = 0`; the same `linEinstein` and the
off-shell bridge give `LE_θθ(tanB, 0) = 1/r² ≠ 0` on `domRN`, from the IV-01 identity
`E_θθ = (b - Q²)/r²`. `LJ` and `LH` vanish for this tangent (`J`, `H` vanish for every `b`). -/
open Real
open scoped ContDiff
open ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.RN
namespace ExactVacuumAtlas.Variation.RN
/-- Tangent of `gRN (M+εm) ((Q+εq)²)` at `ε = 0`: `h_vv = 2m/r - 2Qq/r²`, other components `0`. -/
noncomputable def tanRN (Q m q : ℝ) : Metric 4
| 0, 0 => fun x => 2 * m / x 1 - 2 * Q * q / x 1 ^ 2
| _, _ => fun _ => 0
/-- Tangent of `faradayRN (Q+εq)`: `f_vr = -q/r²`, `f_rv = q/r²`, other components `0`. -/
noncomputable def tanFRN (q : ℝ) : TwoForm 4
| 0, 1 => fun x => -q / x 1 ^ 2
| 1, 0 => fun x => q / x 1 ^ 2
| _, _ => fun _ => 0
/-- Tangent of the off-shell family `gRN M (Q² + ε)`: `h_vv = -1/r²`, other components `0`. -/
noncomputable def tanB : Metric 4
| 0, 0 => fun x => -1 / x 1 ^ 2
| _, _ => fun _ => 0
/-- The product domain `ℝ × domRN`. -/
def domJ : Set (ℝ × Pt 4) := {p | p.2 ∈ domRN}
/-! ## Families -/
/-! ## Genuine tangents -/
/-! ## Parameter tangents solve the linearised equations -/
/-! ## Nonzero test of the same operator -/
end ExactVacuumAtlas.Variation.RN
Source
He Wang, Exact Spacetime Atlas IV: Certified Einstein–Maxwell Backgrounds and First Variations. Local source, no public repository; commit 543904bfcfa3bb169f43fc4d9dbd569999b71886; Atlas/EinsteinMaxwell/Variation/RN.lean; SHA-256 7513cd6c91a5e550bb62e1cac2f2c8a8c17fa469087ba3c27bf9c1eab933f66f. Registered definitions and literature: mission/PHYSICS_BOUNDARY.md (§H–§J); Müller–Grave arXiv:0904.4184; Newman et al., J. Math. Phys. 6 (1965) 918.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.