Pipeline-generated

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.

Linearized coupled equations and gauge identities — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

A stationary Reissner–Nordström charge mode does not decay to zero

Example

Work in the $Λ = 0$ specialization of the linearized geometric electrovacuum system. Fix $M > 0$ , $q_{0} > 0$ , $R_{0} > 4 M$ , and a length $ℓ_{*} > 0$ . Set the dimensionless parameter radius $ϵ : = q_{0} / (2 ℓ_{*})$ and $q (λ) : = q_{0} + λ ℓ_{*}$ . Then $q (λ) > q_{0} / 2 > 0$ for $∣ λ ∣ < ϵ$ . On the fixed exterior $U = R_{x^{0}} \times (R_{0}, \infty) \times S^{2}$ , put $f_{λ} (r) = 1 - \frac{2 M}{r} + \frac{q (λ)^{2}}{r^{2}}, g_{λ} = - f_{λ} (d x^{0})^{2} + f_{λ}^{- 1} d r^{2} + r^{2} γ_{S^{2}}, F_{λ} = - \frac{q (λ)}{r^{2}} d x^{0} \land d r .$ Then $h : = \partial_{λ} g_{λ} ∣_{0}$ and $f : = \partial_{λ} F_{λ} ∣_{0}$ form a smooth stationary solution of the linearized geometric electrovacuum system at $(g_{0}, F_{0})$ . Its electromagnetic perturbation is nonzero and its electric-flux variation through every outward coordinate sphere $S_{r}$ is $\partial_{λ} q_{e} (S_{r}) ∣_{0} = ℓ_{*}$ . Thus this exact mode does not tend to zero in time at fixed $r$ ; an unqualified claim that every linearized component decays to zero without retaining or subtracting parameter modes is false.

Example references

Dyonic Reissner-Nordström metric and field domains

Lorentzian exterior calculus and Hodge star

Full dyonic Reissner-Nordström electrovac verification

Linearized geometric electrovacuum operator and gauge equivalence

Pure-gauge and exact-family perturbations solve the linearized electrovacuum system

Facts & Assumptions

Given: $M > 0$ , $q_{0} > 0$ , $R_{0} > 4 M$ , $ℓ_{*} > 0$ , and the family and fixed exterior domain in the Example.

[F1]

Dyonic Reissner-Nordström metric and field domains: for electric charge $q$ and zero magnetic charge, the geometric Reissner–Nordström metric and field are $g = - f (d x^{0})^{2} + f^{- 1} d r^{2} + r^{2} γ_{S^{2}}$ and $F = - q r^{- 2} d x^{0} \land d r$ .

[F2]

Full dyonic Reissner-Nordström electrovac verification: in the $Λ = 0$ sector, for every real mass and electric charge, this datum solves $d F = d (⋆_{g} F) = 0$ and $Ric = 2 Q (F)$ wherever $r > 0$ and $f \neq 0$ .

[F3]

Geometric electrovac equations and flux normalization: $q_{e} (S) = (4 π)^{- 1} \int_{S} ⋆_{g} F$ for the specified oriented sphere.

[F4]

Lorentzian exterior calculus and Hodge star: $(⋆_{g} F)_{a b} = \frac{1}{2} ({v o l}_{g})_{a b c d} F^{c d}$ in the positive spacetime orientation.

[F5]

Pure-gauge and exact-family perturbations solve the linearized electrovacuum system: a smooth derivative of exact solutions on one fixed domain solves the linearized system.

[A1]

The geometric electrovac suppliers retain the background assumption ${A C}_{ω}$ . No additional choice principle is used for this explicit parameter family. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

Verification

Given: The constants and geometric field family in the Example, with $λ$ dimensionless and $q (λ)$ a length parameter.

1.1A1givenF1F2algebra

For $r > R_{0} > 4 M$ , $f_{λ} (r) > 1 - 2 M / r > 1 / 2$ , so the metric is Lorentzian and the fixed exterior domain avoids every zero of $f_{λ}$ . The parameter family is smooth on $(- ϵ, ϵ) \times U$ and is the $q_{m} = 0$ Reissner–Nordström family of [F1]. By [F2], every member is an exact geometric electrovacuum on the same $U$ .

2.1givenF1F2F5step 1.1algebra

Differentiating the displayed formulas gives ${\dot{f}}_{0} = 2 q_{0} ℓ_{*} / r^{2}$ , $h = - {\dot{f}}_{0} (d x^{0})^{2} - f_{0}^{- 2} {\dot{f}}_{0} d r^{2}, f = - \frac{ℓ_{*}}{r^{2}} d x^{0} \land d r .$ These tensors are smooth on $U$ , independent of $x^{0}$ , and $f \neq 0$ . By [F5] the pair solves the linearized equations.

3.1F1F3F4step 2.1algebra∎

For any $λ$ , on the fixed exterior $f_{λ} > 1 / 2$ , so $g^{00} = - f_{λ}^{- 1}$ , $g^{r r} = f_{λ}$ , and $∣ \det g ∣ = r^{4} \sin^{2} θ$ . Hence ${v o l}_{g_{λ}} = r^{2} \sin θ d x^{0} \land d r \land d θ \land d ϕ$ . The two-form has $(F_{λ})_{0 r} = - q (λ) / r^{2}$ , so $(F_{λ})^{0 r} = q (λ) / r^{2}$ . Using the orientation in [F1] and the component Hodge formula [F4] gives $⋆_{g_{λ}} F_{λ} = q (λ) \sin θ d θ \land d ϕ = q (λ) ω_{S^{2}}$ . The outward coordinate sphere has this positive area orientation, and direct integration in polar coordinates gives $\int_{S_{r}} ω_{S^{2}} = \int_{0}^{2 π} \int_{0}^{π} \sin θ d θ d ϕ = 4 π$ . By [F3], $q_{e} (S_{r}) = q (λ)$ , so differentiating yields $\partial_{λ} q_{e} (S_{r}) ∣_{0} = ℓ_{*} > 0$ . Since the nonzero component $f_{x^{0} r} = - ℓ_{*} / r^{2}$ is independent of $x^{0}$ , it cannot converge to zero as time tends to either infinity at any fixed $r > R_{0}$ . This is a mathematical counterexample to universal componentwise decay without parameter-mode subtraction, not an assertion about physical observations or nonlinear stability.