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.
Constant-radius Bertotti–Robinson data are outside areal-coordinate rigidity
Statement refuted
Every exact spherical Einstein–Maxwell– datum is locally expressible in the charged Reissner–Nordström–(A)dS form with its areal radius as a coordinate, without any restriction on .
Statement references
Facts & Assumptions
Given: The first Bertotti–Robinson product branch with parameter , its sphere radius and electromagnetic two-form.
Constant-radius Bertotti-Robinson product data defines the branch , , with sphere radius .
Product electrovacuum equations from full factor Ricci proves that every datum in Constant-radius Bertotti-Robinson product data, including this branch, satisfies the source-free geometric Einstein–Maxwell equations.
Local charged Birkhoff rigidity away from critical areal gradients assumes and before using the areal radius as a coordinate.
Dyonic Reissner-Nordström metric and field domains fixes the unit-sphere outward area form .
Spherical orbit geometry and rotational invariance defines the exact local -action, the pullback action on tensor fields, and rotational invariance.
Spherical electrovacuum quotient and charged mass defines the spherical Einstein–Maxwell– datum, including the requirement that its smooth two-form be rotationally invariant; for its equations are exactly the geometric electrovac equations verified in [F2].
Counterexample
On the branch of [F1], take , , , future timelike field , and constant . This is a nonempty, connected, simply connected smooth Lorentzian orbit patch with the orientation, time orientation, and product metric of [F5]; its prescribed four-volume form is , matching [F1]. For each the lift fixes the base two-form , so ; also preserves the induced round metric. Thus the field and metric satisfy the rotational-invariance and warped-product clauses in [F5] and [F6]. Each symmetry sphere has induced metric and area by [F4]. Its areal radius is therefore the constant scalar , so throughout the product patch. A function whose differential vanishes cannot serve as a coordinate in a chart, because the differential of every coordinate function is nonzero.
By [F2], [F5], [F6], and step 1.1 this is an exact spherical Einstein–Maxwell datum with , yet it does not admit its areal radius as a coordinate. It therefore refutes the unrestricted claim: the Reissner–Nordström–(A)dS areal-coordinate form needs a nonzero areal-radius gradient. This example is excluded by [F3] and makes no claim about whether other coordinates or limiting relations connect the two geometries.
Depends on
Local charged Birkhoff rigidity away from critical areal gradients
Constant-radius Bertotti-Robinson product data
Product electrovacuum equations from full factor Ricci
Dyonic Reissner-Nordström metric and field domains
Spherical orbit geometry and rotational invariance
Spherical electrovacuum quotient and charged mass