NP Bianchi identity (b) with Ricci sources

Proved

ExactVacuumAtlas.EinsteinMaxwell.NP.np_bianchi_b

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

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

Any null frame: component (l,m; n,l,m) of the Bianchi identity with Ricci sources. Source of III's res1b.

Scope. Exactly the hypotheses printed in the formal statement.

中文摘要 NP Bianchi (b)，保留 Ricci 源项；res1b 的来源。

Preamble

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_KNFrame
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_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
open scoped ContDiff Matrix
open Complex
open ExactVacuumAtlas
open ExactVacuumAtlas.EinsteinMaxwell
open ExactVacuumAtlas.EinsteinMaxwell.NP
set_option linter.unusedSimpArgs false
variable {g gi : Metric 4} {E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ} {U : Set (Pt 4)}

Formal statement

theorem ExactVacuumAtlas.EinsteinMaxwell.NP.np_bianchi_b (hN : NullFrameData g gi E Θ U) {x : Pt 4} (hx : x ∈ U) :
    (1) * fdir E 1 (psi0 g gi E) x +
        (-1) * fdir E 2 (psi1 g gi E) x +
        (1/2) * fdir E 0 (ricF g gi E 2 2) x +
        (-1/2) * fdir E 2 (ricF g gi E 0 2) x
      = (-2) * psi1 g gi E x * npBeta g gi E Θ x +
        (-4) * psi1 g gi E x * npTau g gi E Θ x +
        (4) * psi0 g gi E x * npGamma g gi E Θ x +
        (-1) * psi0 g gi E x * npMu g gi E Θ x +
        (3) * psi2 g gi E x * npSigma g gi E Θ x +
        (-1) * npBeta g gi E Θ x * ricF g gi E 0 2 x +
        (1) * npEps g gi E Θ x * ricF g gi E 2 2 x +
        (-1) * npEpsB g gi E Θ x * ricF g gi E 2 2 x +
        (-1) * npKappa g gi E Θ x * ricF g gi E 1 2 x +
        (-1/2) * npLambdaB g gi E Θ x * ricF g gi E 0 0 x +
        (1) * npPiB g gi E Θ x * ricF g gi E 0 2 x +
        (1/2) * npRhoB g gi E Θ x * ricF g gi E 2 2 x +
        (1/2) * ricF g gi E 0 1 x * npSigma g gi E Θ x +
        (1/2) * ricF g gi E 2 3 x * npSigma g gi E Θ x := by sorry

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/NPBianchiNP.lean#L449-L484; SHA-256 ea0382ebea92c4638a3d050ceb9e7891f3c8fee12cfa1baecd44232265e2ddb3. 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