V-03 background Φ₁ prefactor

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Res.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.prefPhi
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_V03Mode
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 2): the eight frozen III residuals `res1a … res1d`, `res1aN … res1dN`

Each complexified, source-free linearised NP identity (`V03C3`) is evaluated on single-mode fields: frame derivatives
of mode fields are III's `j = 0` operators (V-01 `mode_directions`), the prefactors `q, q̄` of the scaled fields are
differentiated by the 2D product rule (`cpd_pref`), and the KN spin coefficients are inserted (V-02 tables; the
`B`-suffixed ones in `npKN_B`). The `j` terms, `3/ρ̄*` and `3ia sin θ/ρ̄*` of III come out of these derivatives
and coefficients; III's definitions are imported unchanged. Only `phaseP`, `q`, `q̄`, `√2`, `Σ`, `Δ`, `sin θ`
(proved nonzero on `domKN`) and, in `res1d`/`res1dN` only, `Q` (`p.hQ : Q ≠ 0`) are divided by; never `ω`, `m`, `F₊`, `F₋`. -/

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

section knB

variable {M a Q : ℝ} {x : Pt 4}

end knB

/-! ### The background `Φ₁ = Q/(2 ρ̄*²)` as a (`ω = m = 0`) mode field -/

section phi

variable (p : Hintz2026.SubextremalKN)

/-- `Φ₁` of the KN background as a function of `(r, θ)` (class B). -/
noncomputable def prefPhi (w : Fin 2 → ℝ) : ℂ := (p.Q : ℂ) / 2 * (Hintz2026.rhoBarStar p w ^ 2)⁻¹

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

end phi

section res

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 : ℝ) : ℂ)

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

end res

end ExactVacuumAtlas.EinsteinMaxwell.NP

• 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).