ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck pass

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.

Explicit static clock-rate ratios of the Schwarzschild exterior at r = 2s and r = 4s

Example

Let $(M, g, N)$ be the Schwarzschild exterior datum with Schwarzschild radius $s > 0$ , $f (r) = 1 - s / r$ (The Schwarzschild exterior model datum: domain, metric, mass parameter and time orientation) and static observer congruence $n = f^{- 1 / 2} \partial_{0}$ (The static observer congruence of the Schwarzschild exterior model: unit field, integral curves, acceleration and clock-rate ratios clause (a), Observer congruences, their observer curves and adapted charts). By The static observer congruence of the Schwarzschild exterior model: unit field, integral curves, acceleration and clock-rate ratios clause (c), a static observer worldline at radius $r_{0} \in (s, \infty)$ has proper-time increment

$Δ τ (r_{0}) = \sqrt{f (r_{0})} Δ t = \sqrt{1 - \frac{s}{r_{0}}} Δ t$

over a coordinate-time increment $Δ t = Δ x^{0} / c > 0$ . Then:

Exact values at the two radii. For $r_{1} = 2 s$ and $r_{2} = 4 s$ one has $f (r_{1}) = \frac{1}{2}$ , $f (r_{2}) = \frac{3}{4}$ , so $Δ τ (r_{1}) = \frac{Δ t}{\sqrt{2}}, Δ τ (r_{2}) = \frac{\sqrt{3}}{2} Δ t, \frac{Δ τ (r_{1})}{Δ τ (r_{2})} = \sqrt{\frac{2}{3}} = \frac{\sqrt{6}}{3} < 1.$
Monotonicity in the radius. The function $r \mapsto \sqrt{f (r)} = \sqrt{1 - s / r}$ is smooth and strictly increasing on $(s, \infty)$ with derivative $\frac{d}{d r} \sqrt{f (r)} = \frac{s}{2 r^{2} \sqrt{f (r)}} > 0$ ; consequently a static observer at the larger radius accumulates strictly more proper time over the same coordinate interval: $Δ τ (r_{2}) > Δ τ (r_{1})$ for $s < r_{1} < r_{2}$ , and the ratio of clause 1 is the exact instance at $(r_{1}, r_{2}) = (2 s, 4 s)$ .
Large-radius limit. $\sqrt{f (r)} \to 1$ as $r \to + \infty$ ; the ratios $Δ τ (r_{1}) / Δ τ (r_{2})$ are invariant under the common scaling of $Δ t$ and tend to $1$ as $\min (r_{1}, r_{2}) \to + \infty$ with $r_{2} > r_{1}$ .
The static observers are accelerated. At $r_{1} = 2 s$ the acceleration of the congruence is $a = \frac{s}{2 r^{2}} \partial_{r}$ (The static observer congruence of the Schwarzschild exterior model: unit field, integral curves, acceleration and clock-rate ratios clause (e)), whose coefficient at $r_{1} = 2 s$ is $\frac{s}{2 (2 s)^{2}} = \frac{1}{8 s} > 0$ : the observer held at $r_{1} = 2 s$ has nonzero acceleration pointing in the direction of increasing $r$ , so it is not freely falling.

Facts & Assumptions

Given: The exterior datum with $s > 0$ and $f = 1 - s / r$ , a fixed $Δ t > 0$ , the radii $r_{1} = 2 s$ , $r_{2} = 4 s$ , and the static observer congruence $n = f^{- 1 / 2} \partial_{0}$ .

[L1]

The static congruence $n = f^{- 1 / 2} \partial_{0}$ is a smooth future-directed unit timelike field, its integral curves are the worldlines at constant $r$ , and along each such worldline $Δ τ = \sqrt{f (r_{0})} Δ t$ with $Δ t = Δ x^{0} / c$ ; for two radii over the same nonzero coordinate interval, $Δ τ_{1} / Δ τ_{2} = \sqrt{f (r_{1}) / f (r_{2})}$ (The static observer congruence of the Schwarzschild exterior model: unit field, integral curves, acceleration and clock-rate ratios clauses (a)-(d), Observer congruences, their observer curves and adapted charts, The Schwarzschild exterior model datum: domain, metric, mass parameter and time orientation).

[L2]

The acceleration of the congruence is $a = \nabla_{n} n = \frac{s}{2 r^{2}} \partial_{r}$ (The static observer congruence of the Schwarzschild exterior model: unit field, integral curves, acceleration and clock-rate ratios clause (e)).

[L3]

The function $f (r) = 1 - s / r$ is smooth and positive on $(s, \infty)$ , $f (2 s) = 1 / 2$ , $f (4 s) = 3 / 4$ , and $\sqrt{\cdot}$ is smooth with derivative $\frac{1}{2 \sqrt{x}}$ on $(0, \infty)$ ; sums, products and compositions of smooth functions are smooth (The Schwarzschild exterior datum is a smooth time-oriented Lorentzian four-manifold, The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , Rational powers $a^{r}$ of a positive base, Continuity and derivatives of positive-base real powers, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L4]

For $s < r_{1} < r_{2}$ one has $0 < s / r_{2} < s / r_{1} < 1$ , hence $0 < f (r_{1}) < f (r_{2}) < 1$ by direct subtraction, $f (r_{2}) - f (r_{1}) = s (r_{2} - r_{1}) / (r_{1} r_{2}) > 0$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

A function continuous on $[a, b]$ and differentiable on $(a, b)$ , for $a < b$ , satisfies $h (b) - h (a) = h^{'} (ξ) (b - a)$ for some $ξ \in (a, b)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct; evaluate the clock identity at the two explicit radii, differentiate the square root to get monotonicity, and substitute $r_1=2s$ in the acceleration coefficient

1.1L1L3algebra

(Values at $2 s$ and $4 s$ .) By [L3], $f (2 s) = 1 - \frac{s}{2 s} = \frac{1}{2}$ and $f (4 s) = 1 - \frac{s}{4 s} = \frac{3}{4}$ , both positive, so [L1] gives $Δ τ (r_{1}) = \sqrt{1 / 2} Δ t = \frac{Δ t}{\sqrt{2}}$ and $Δ τ (r_{2}) = \sqrt{3 / 4} Δ t = \frac{\sqrt{3}}{2} Δ t$ . The ratio is $\sqrt{\frac{1 / 2}{3 / 4}} = \sqrt{\frac{2}{3}} = \frac{\sqrt{6}}{3}$ , and $\sqrt{6} / 3 < 1$ because $6 < 9$ . This is clause 1.

2.1L1L3L4L5step 1.1algebra

(Monotonicity.) On $(s, \infty)$ the chain rule gives $\frac{d}{d r} \sqrt{f (r)} = \frac{f^{'} (r)}{2 \sqrt{f (r)}} = \frac{s / r^{2}}{2 \sqrt{f (r)}} = \frac{s}{2 r^{2} \sqrt{f (r)}}$ , using $f^{'} (r) = s / r^{2}$ and $\sqrt{f} > 0$ by [L3]. The numerator and denominator are positive, so the derivative is positive. On every $[a, b] \subset (s, \infty)$ with $a < b$ , $\sqrt{f}$ is continuous and differentiable by [L3], and [L5] gives $\sqrt{f (b)} - \sqrt{f (a)} = (b - a) s / (2 ξ^{2} \sqrt{f (ξ)}) > 0$ for some $ξ \in (a, b)$ . Thus $\sqrt{f}$ , hence $r \mapsto Δ τ (r)$ at fixed $Δ t > 0$ , is strictly increasing; with $f (r_{1}) < f (r_{2})$ by [L4], $r_{1} < r_{2}$ gives $Δ τ (r_{1}) < Δ τ (r_{2})$ and the ratio of clause 1 is the instance $r_{1} = 2 s$ , $r_{2} = 4 s$ . This is clause 2 and the inequality $Δ τ (r_{2}) > Δ τ (r_{1})$ of clause 1.

2.2L1L3step 1.1algebra

(Large-radius limit.) As $r \to + \infty$ , $s / r \to 0$ , so $f (r) \to 1$ and $\sqrt{f (r)} \to 1$ by [L3]; hence $Δ τ (r) = \sqrt{f (r)} Δ t \to Δ t$ and the ratio $Δ τ (r_{1}) / Δ τ (r_{2}) = \sqrt{f (r_{1}) / f (r_{2})} \to 1$ whenever $\min (r_{1}, r_{2}) \to + \infty$ with the radii positive. The ratio does not involve $Δ t$ , since the common factor cancels. This is clause 3.

3.1L1L2L3algebra∎

(Acceleration at $2 s$ .) By [L2] the acceleration field is $a = \frac{s}{2 r^{2}} \partial_{r}$ , whose coefficient function is smooth and positive on $(s, \infty)$ ; at $r_{1} = 2 s$ it is $\frac{s}{2 (2 s)^{2}} = \frac{1}{8 s} > 0$ . Since the coefficient is nonzero, the worldlines of the congruence do not satisfy the geodesic equation, so the observer held at radius $2 s$ is accelerated with the stated outward-coefficient $1 / (8 s)$ in the coordinate basis $(\partial_{0}, \partial_{r}, \partial_{ϑ}, \partial_{φ})$ . This is clause 4.

Remarks

What the example computes. All four clauses are exact evaluations of the clock identity and the acceleration formula of the cited lemma at explicit radii; the coordinate-time increment $Δ t$ is an arbitrary positive coordinate difference, not a measurement, and no value of $c$ , $G_{N}$ , $m_{*}$ or $s$ in any unit system is asserted. In particular clause 1 does not report a clock comparison or a redshift observation; it is the conditional identity of the model evaluated at two radii.

Explicit static clock-rate ratios of the Schwarzschild exterior at r = 2s and r = 4s

Example

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources