Formalize: perturbative uniqueness near Kerr using Mars-Simon tensor estimates (machine-checkable Carleman skeleton).
Summary
Stationary, asymptotically flat vacuum spacetimes admit tensorial characterizations of the Kerr geometry via the (spacetime) Simon/Mars tensor and related Weyl–Killing alignment conditions (Mars, CQG 1999). Separately, perturbative stationary uniqueness near Kerr often proceeds via Carleman-type estimates and curvature tensors in weighted Sobolev classes. This **formalization** problem asks for a proof-assistant–ready modularization: state minimal axioms (smoothness, stationarity, AF fall-off, smallness in a named norm), list lemmas with precise hypotheses, and isolate where Simon/Mars identities substitute for raw tensor estimates—without claiming a new PDE theorem beyond the literature.
Why this matters
Separates tensorial Kerr characterizations from PDE stability formalizations; high formal-verification value for rigidity modules reused in wider relativity formalization efforts.
Exact scope
- Background / setting
- asymptotically flat general relativity context; see family and coupling tags for matter model.
- Equation type
- PDE level: full-einstein.
- Linearity
- linearized
- Regularity
- Smooth / Sobolev hypotheses must be stated precisely in any final theorem; this provisional entry does not fix minimal regularity.
- Parameter regime
- Neighborhood of a fixed subextremal Kerr solution in a stationary AF vacuum class; smallness in weighted Sobolev (or equivalent) norms as in the chosen Carleman route—**not** a dynamical Cauchy stability problem.
- Asymptotics
- asymptotically flat
- Gauge / formulation
- State gauge/fixing class compatible with cited stability or interior programs (e.g. generalized harmonic, double-null interior charts).
Status explanation
**Open (formalization):** the underlying analytic rigidity technology exists in the literature, but a proof-assistant–checkable decomposition linking Mars/Simon tensor algebra to a concrete Carleman estimate package is not recorded as completed here.
Problem statement
Produce a machine-checkable proof skeleton (e.g. Lean/Coq) that derives a stated **local** perturbative uniqueness or rigidity lemma for smooth stationary AF vacuum metrics near Kerr, following a published Carleman/unique continuation route, and explicitly interfaces any use of the Mars/Simon tensor characterization as algebraic lemmas (not as a black box “Kerr uniqueness”).
What is already known
- Mars gives a spacetime Simon tensor characterization: stationary AF vacuum with vanishing spacetime Simon tensor is locally isometric to Kerr (CQG 1999; arXiv:gr-qc/9904070).Regime: Stationary AF vacuum; local isometry conclusion.Sharp tensorial certificate of Kerr geometry—potential algebraic layer in a formalized perturbative argument if hypotheses match.
- Global smooth stationary uniqueness without analyticity (K-301) remains a separate open PDE benchmark; formalizing **local** Carleman lemmas near Kerr is a smaller, well-scoped target.Regime: Stationary uniqueness cluster.Prevents conflating this formalization task with full global uniqueness programs.
- Surveys (e.g. Mazur) summarize Carter–Robinson–Mazur lines and reduction routes; use them for bibliographic context, not as a substitute for checking hypotheses in code.Regime: Stationary uniqueness literature.Orientation for where tensor characterizations sit relative to global theorems.
Progress summary: Mars (1999) supplies a sharp Kerr characterization tensor; packaging it with a Carleman route into a proof assistant is the remaining engineering/mathematics formalization work.
What remains open
Deliver an actual formalization artifact (definitions + lemma statements + proof-term outline) tied to one published Carleman/unique continuation argument; document any axioms that remain mathematically open.
Mathematical prerequisites
Proof-assistant infrastructure; tensor calculus; weighted Sobolev estimates; unique continuation/Carleman inequalities as in the chosen primary PDE reference (to be pinned to one paper in a follow-up edit if needed).
Completion criteria
Public repository artifact compiling formal definitions, lemma statements, and completed or sketched proof terms for a single named analytic argument, with explicit dependency graph to Mars (1999) lemmas.
Implications if solved
Reusable formal library for stationary uniqueness and near-Kerr rigidity lemmas inside larger GR formalization efforts.
Formal verification suitability
FV: high
Formalization targets map naturally to proof-assistant-sized subtasks once scoped.
See Formal verification for how this database uses these labels.
References
- primary A spacetime characterization of the Kerr metric — Mars, Marc (1999) Defines the spacetime Simon tensor and proves a Kerr characterization among stationary AF vacuum solutions—algebraic input for any formalized perturbative uniqueness module that imports tensor identities.
- survey Black Uniqueness Theorems — Mazur (2001) Survey of stationary uniqueness and reduction routes (including Ernst-type formulations).
Related problems
Related by shared tags
- K-306 — Hidden symmetries and approximate Carter-type operators under metric perturbation
- K-307 — Persistence of normally hyperbolic trapping for dynamical near-Kerr spacetimes
- K-508 — Stability or obstruction for approximate Killing–Yano tensors near Kerr
- K-617 — Prove a quantitative distance-to-Kerr estimate from a small invariant (Mars-Simon-type) with computable constants.
- K-618 — Prove global Kerr uniqueness without analyticity under minimal smoothness/decay hypotheses.
- K-633 — Prove that near-Kerr spacetimes admit approximate Carter operators with controlled commutators (usable in PDE estimates).
- K-646 — Prove global uniqueness/rigidity for Kerr with minimal assumptions on horizon regularity and connectedness.
Editorial / maintainer notes
Source manifest: N-096 (expansion_from_manifest.tsv). Numeric footnotes from the original table are not reproduced in this repository.