MP02 (μ = 5, rotation constant −2/3): Einstein–Maxwell certificate with 𝒜 = 0 via the reduced system
ProvedExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.candidate_certificateMP02 (μ = 5, rotation constant −2/3): Einstein–Maxwell certificate with 𝒜 = 0 via the reduced system
EMCertificateD candG candGi candF dom for A = r² + a², H = ((r²+a²)² + 5a²)/(r²+a²), W = 5a/((r²+a²)² + 5a²), B = ((r²+a²)² − 5r²)/((r²+a²)² + 5a²), D = r²(r²+a²)/((r²+a²)² − 5r²) with the transcribed constant a = −2/3, Φ = Ψ = 0, dom = esDomain {r | 0 < r ∧ rX r ≠ 0}, rX r = (r² + (−2/3)²)² − 5r². Proved only through the Goal es_certificate_iff from the seven reduced equations; no VacuumCertificate statement is made for MP02. A second fixed instance, not an arbitrary-parameter theorem.
Scope. Fixed rational parameters transcribed from the candidate JSON; domain dom = esDomain radR with radR = {r | 0 < r ∧ rX r ≠ 0}; no horizon/axis regularity.
中文摘要 MP02（μ=5，转动常数 −2/3）：经目标定理由七个约化方程得到的 EMCertificateD（𝒜=0）。只是第二个固定参数实例。
import Mathlib import Definitions.Def_Atlas_Core_Basic import Definitions.Def_Atlas_Core_Certificate import Definitions.Def_Atlas_EinsteinMaxwell_Basic import Definitions.Def_Atlas_EinsteinMaxwell_D_Basic import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Cand_MP02_Defs import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Cand_MP02_Reduced import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Defs import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Cert import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Data import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Reduced import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Tables open scoped ContDiff open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D open ExactVacuumAtlas.EinsteinMaxwell.ES5 open ExactVacuumAtlas open ExactVacuumAtlas.EinsteinMaxwell open ExactVacuumAtlas.EinsteinMaxwell.ES5 open ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand open ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02 set_option maxHeartbeats 8000000 set_option maxRecDepth 100000 set_option linter.unusedVariables false set_option linter.unusedSimpArgs false set_option linter.unusedTactic false set_option linter.unreachableTactic false
theorem ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.candidate_certificate : EMCertificateD candG candGi candF dom := by sorry
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.