Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Kerr geometry and hidden symmetry — Schwarzschild limit

Physical scope

Pure mathematical limit and separation example; no measurement or claim about gravitational collapse is made.

Example

At a=0, the Kerr exterior is exactly the Schwarzschild exterior with Schwarzschild radius 2M, and ΩH=0. Its Ricci tensor vanishes. The Hamilton-Jacobi separation constant reduces to Q=pθ2+Lz2cot⁡2θ=Lsph2−Lz2, where pθ:=Sθ′, Lz:=∂ϕS, and Lsph2:=pθ2+Lz2/sin⁡2θ. The axial Killing field Φ also gives the reducible Killing tensor KΦ=Φ♭⊗Φ♭, whose quadratic integral is constant along affine geodesics.

Facts & Assumptions

Given: M>0, a=0, geometric units GN=c=1, and the Kerr and Schwarzschild metric data.

[F1]

Subextremal Kerr exterior in length coordinates: Σ=r2+a2cos⁡2θ, Δ=r2−2Mr+a2, with the stated Boyer-Lindquist metric components.

[F2]

The Schwarzschild exterior model datum: domain, metric, mass parameter and time orientation: in geometric units its exterior has s=2m∗ and line element −(1−s/r)dt2+(1−s/r)−1dr2+r2γS2 on r>s.

[F3]

Kerr horizon angular velocity and the ergoregion: T=∂t and Φ are Killing, and ΩH=a/(r+2+a2).

[F4]

Killing tensors and quadratic geodesic integrals: a symmetric tensor is Killing when ∇(aKbc)=0; reducible tensors include symmetric products of lowered Killing fields.

[F5]

Conservation of quadratic geodesic integrals: a rank-two Killing tensor gives a constant quadratic integral along every affine geodesic.

[F6]

Kerr exterior vacuum verification: the Kerr exterior metric has Ric⁡=0.

[F7]

Local Kerr Hamilton-Jacobi separation: the local separated equations for Sr′ and Sθ′ hold with the stated constants.

[F8]

Killing fields and conserved currents, and on-shell conservation of the Hilbert stress-energy tensor: a Killing field satisfies ∇aΦb+∇bΦa=0.

[A1]

The smooth Lorentzian and tangent-bundle conventions use only countable choice ACω (The Axiom of Countable Choice (ACω)).

Verification

1.1givenA1F1F2algebra

Setting a=0 gives r+=2M, Σ=r2, Δ=r(r−2M), and gtϕ=0. The remaining components are gtt=−(1−2M/r), grr=(1−2M/r)−1, gθθ=r2, and gϕϕ=r2sin⁡2θ. These are exactly [F2] with s=2m∗=2M and the same domain r>2M.

1.2F3F4F8algebra

Since Φ is Killing by [F3] and [F8], set KabΦ:=ΦaΦb. The product rule gives ∇(aKbc)Φ=13[Φb(∇aΦc+∇cΦa)+Φc(∇aΦb+∇bΦa)+Φa(∇bΦc+∇cΦb)]=0. Thus KΦ is a reducible Killing tensor by [F4].

2.1givenF3F6step 1.1algebra

By [F3], ΩH=a/(r+2+a2), so ΩH=0 at a=0. The vacuum statement follows by applying [F6] to this same metric and restricting its domain to r>2M.

2.2F4F5step 1.2

Along an affine geodesic, KabΦvavb=(Φava)2 is constant by [F5]. This is the axial quadratic integral; it is reducible and is not identified with an irreducible Carter tensor.

3.1F7algebra∎

Setting a=0 in [F7] gives Q=pθ2+Lz2cos⁡2θ/sin⁡2θ=pθ2+Lz2cot⁡2θ. Since 1/sin⁡2θ−cot⁡2θ=1, this equals Lsph2−Lz2 under the definitions in the Example.

Remarks

This limit identifies the separated angular constant with the familiar spherical expression. It does not infer a formula or irreducibility result for the Kerr Carter tensor away from a=0.

Depends on

Dependency tree · 2 levels

Sources