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.

The radial proper-time maximum checked on an explicit family of wiggly curves in flat space

Example

Keep the flat model of Geodesics, proper time and parallel transport of the flat model: $M = R^{4}$ with the identity chart, $g = diag (- 1, 1, 1, 1)$ , the metric-selected connection with $Γ = 0$ , and $c > 0$ . Fix $0 \leq a < c / π$ and consider the piecewise smooth curve

$α_{a} : [0, 1] ⟶ R^{4}, α_{a} (t) : = (c t, a \sin (π t), 0, 0) .$

Its endpoints are $p = (0, 0, 0, 0)$ and $q = (c, 0, 0, 0)$ , it has nonzero future timelike tangents for every $t$ , and it stays in the exponential domain $R^{4}$ of $p$ , so The Lorentzian Gauss lemma and the radial maximum of proper time applies with $v_{q} = \exp_{p}^{- 1} (q) = (c, 0, 0, 0)$ . Then:

Its length is $L_{g} (α_{a}) = \int_{0}^{1} \sqrt{c^{2} - a^{2} π^{2} \cos^{2} (π t)} d t$ , and $L_{g} (α_{a}) < c = \sqrt{- g (v_{q}, v_{q})}$ for every $a \neq 0$ , while $L_{g} (α_{0}) = c$ .
Hence the curve is strictly below the radial maximum unless $a = 0$ , in which case $α_{0} (t) = (c t, 0, 0, 0)$ is the radial geodesic itself (a straight line through $p$ ); this exhibits the equality case of the theorem on an explicit family.

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart, a real $a$ with $0 \leq a < c / π$ , and the curve $α_{a} (t) = (c t, a \sin (π t), 0, 0)$ .

[L1]

In this model $\exp_{p} (v) = p + v$ on all of $T_{p} M$ , the geodesics are the affine lines, and $p = (0, 0, 0, 0)$ , $q = α_{a} (1) = (c, 0, 0, 0)$ give $v_{q} = (c, 0, 0, 0)$ (Geodesics, proper time and parallel transport of the flat model, The geodesic initial-value problem and the exponential map of the metric-selected connection).

[L2]

The tangent of $α_{a}$ is $(c, a π \cos (π t), 0, 0)$ , with $g (α_{a}^{'}, α_{a}^{'}) = - c^{2} + a^{2} π^{2} \cos^{2} (π t) < 0$ and $g (α_{a}^{'}, \partial_{0}) = - c < 0$ when $a < c / π$ ; hence the curve is a future timelike worldline and its length over $[0, 1]$ is as displayed (Timelike worldlines, proper time, length and four-velocity on a Lorentzian four-manifold, Proper time is well defined and reparametrization invariant; the four-velocity is its proper-time tangent).

[L3]

The radial maximum theorem applies to piecewise smooth future timelike curves with image in the exponential domain of $p$ and gives $L_{g} (α) \leq \sqrt{- g_{p} (v_{q}, v_{q})}$ , with equality exactly for monotone reparametrizations of the radial geodesic from $p$ to $q$ (The Lorentzian Gauss lemma and the radial maximum of proper time).

[L4]

If two continuous functions on $[0, 1]$ satisfy $f \leq c$ everywhere and $f < c$ on a nondegenerate subinterval, then $\int_{0}^{1} f < \int_{0}^{1} c = c$ ; this is monotonicity of the Darboux integral together with strict positivity of $\int (c - f)$ over a subinterval where $c - f > 0$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

Verification

technique · direct

1.1givenL2algebra

By [L2], $α_{a}$ is a piecewise smooth (indeed smooth) future timelike worldline with image in the exponential domain $R^{4}$ of $p$ , and its length is $L_{g} (α_{a}) = \int_{0}^{1} \sqrt{c^{2} - a^{2} π^{2} \cos^{2} (π t)} d t$ .

2.1step 1.1L1algebra

For $a = 0$ the integrand is the constant $c$ , so $L_{g} (α_{0}) = c$ ; and $α_{0} (t) = (c t, 0, 0, 0)$ is the straight affine line through $p$ with direction $(c, 0, 0, 0) = v_{q}$ , which by [L1] is the radial geodesic from $p$ to $q$ . Thus equality holds in the sense of [L3].

2.2step 1.1L1L3L4algebra

For $a \neq 0$ the integrand $f (t) = \sqrt{c^{2} - a^{2} π^{2} \cos^{2} (π t)}$ is continuous and satisfies $f (t) \leq c$ , with strict inequality $f (t) < c$ at every $t$ with $\cos (π t) \neq 0$ ; such points form a nondegenerate subinterval of $[0, 1]$ , for instance around $t = 0$ . By [L4], $\int_{0}^{1} f d t < c$ , so $L_{g} (α_{a}) < \sqrt{- g (v_{q}, v_{q})} = c$ ; moreover $α_{a}$ is not a reparametrization of the straight segment because its second coordinate $a \sin (π t)$ is not identically zero.

3.1step 2.1step 2.2L3algebra∎

Steps 2.1 and 2.2 verify both the inequality and the equality case of The Lorentzian Gauss lemma and the radial maximum of proper time on the family ${α_{a}}_{0 \leq a < c / π}$ : the length is maximized exactly by the radial geodesic, and every nonradial member of the family is strictly shorter, in agreement with the theorem's proper-time statement after division by $c$ .

The radial proper-time maximum checked on an explicit family of wiggly curves in flat space

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources