KN moving parameter domain

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Variation/KN.lean
-- definition bundle: kept ExactVacuumAtlas.Variation.KN.domJ
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_KN_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Domain
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_Kerr_Frame
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_MatrixCalc
import Definitions.Def_KerrBL_CoordGeometry
import Definitions.Def_KerrBL_Kerr_Metric
/-! # Kerr–Newman (Boyer–Lindquist): parameter tangents (ATLAS-IV-03)

Data `gKN M a Q`, `giKN M a Q`, `faradayKN a Q`, `domReg M a Q = {Σ ≠ 0, Δ ≠ 0, sin θ ≠ 0}` of IV-02,
unchanged. For every real `M, a, Q` and every direction `(m, α, q)` (mass, rotation, charge, or any real
combination; `a = 0`, `Q = 0` allowed, no division by `a` or `Q`):

* the actual family `ε ↦ (gKN (M+εm) (a+εα) (Q+εq), giKN …, faradayKN (a+εα) (Q+εq))` is a `FamilyData`
  on the **open** set `domJ = {(ε, y) | y ∈ domReg (M+εm) (a+εα) (Q+εq)}` (parameter-dependent regular set;
  no uniform `ε`-interval over the noncompact exterior is claimed);
* every member is certified by `certReg` (no derivative of the horizon cut `rPlus` is taken);
* hence (`param_tangent`) its genuine tangent `paramTangent` (componentwise `ε`-derivative at `0`, a true
  `HasDerivAt` by `isTangent_paramTangent`) satisfies `LE = LJ = LH = 0` at every `x ∈ domReg M a Q`, and
  (`param_tangent_exterior`) on the BL exterior `domKN M a Q` when `0 < M`. -/

open Real
open scoped ContDiff
open ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.KN

namespace ExactVacuumAtlas.Variation.KN

/-- Parameter-dependent regular domain in `ℝ × ℝ⁴`. -/
def domJ (M a Q m α q : ℝ) : Set (ℝ × Pt 4) :=
  {p | p.2 ∈ domReg (M + p.1 * m) (a + p.1 * α) (Q + p.1 * q)}

end ExactVacuumAtlas.Variation.KN

• Endorsed by Shuze Chen · Oct 21, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 21, 2026

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