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.

An exact observer-relative energy and momentum computation at relative speed c/2, with the expansion bounds of the low-velocity lemma checked by exact rational comparison

Example

Work on the flat model of The flat model spacetime: the Minkowski metric on R^4 and its inertial chart with inertial chart $x$ and let $c > 0$ and $m > 0$ . At $p$ with $x (p) = 0$ take the observer $n : = \partial_{0} ∣_{p}$ and the tangent vector

$P : = m c u, u : = \frac{2}{\sqrt{3}} \partial_{0} ∣_{p} + \frac{1}{\sqrt{3}} \partial_{1} ∣_{p},$

so that $g_{p} (u, u) = - 1$ and $P$ is future timelike with rest mass $m$ (Observer-relative energy, spatial momentum and rest mass of a tangent vector). Then the observer data of the low-velocity lemma are

$h_{n} (u) = \frac{1}{\sqrt{3}} \partial_{1} ∣_{p}, γ = \frac{2}{\sqrt{3}}, w = \frac{c}{2} \partial_{1} ∣_{p}, s = \frac{c}{2},$

and the exact energy and momentum are

$E_{n} (P) = \frac{2 m c^{2}}{\sqrt{3}}, q_{n} (P) = \frac{m c}{\sqrt{3}} \partial_{1} ∣_{p}, ∣ q_{n} (P) ∣ = \frac{m c}{\sqrt{3}} .$

With $v_{0} : = c / 2$ , $z_{0} = 1 / 4$ this realizes $s = v_{0} < c$ and the exact identities

$E_{n} (P) = m c^{2} (1 - \frac{s^{2}}{c^{2}})^{- 1 / 2}, ∣ q_{n} (P) ∣ = m s (1 - \frac{s^{2}}{c^{2}})^{- 1 / 2}$

of Low-velocity expansions of observer energy and momentum with uniform error bounds, and the two uniform error bounds of that lemma read

$∣ E_{n} (P) - m c^{2} - \frac{1}{2} m s^{2} ∣ = \frac{m c^{2} (16 - 9 \sqrt{3})}{8 \sqrt{3}} \leq \frac{m c^{2}}{12 \sqrt{3}}, ∣ ∣ q_{n} (P) ∣ - m s ∣ = \frac{m c (2 - \sqrt{3})}{2 \sqrt{3}} \leq \frac{m c}{6 \sqrt{3}},$

which are strict, finite checks of the bounds at the single relative speed $s = c / 2$ .

Facts & Assumptions

Given: The flat model with inertial chart $x$ , the point $p$ with $x (p) = 0$ , the observer $n = \partial_{0} ∣_{p}$ , the vector $u = \frac{2}{\sqrt{3}} \partial_{0} ∣_{p} + \frac{1}{\sqrt{3}} \partial_{1} ∣_{p}$ , and $P = m c u$ with $c, m > 0$ .

[L1]

An observer at $p$ is a future-directed vector $n$ with $g_{p} (n, n) = - 1$ ; the spatial projection is $h_{n} (v) = v + g_{p} (n, v) n$ (Observers, rest spaces and the spatial projection at an event clauses (a) and (c)). The projections satisfy $h_{n} (n) = 0$ , $h_{n} (v) = v$ for $g_{p} (v, n) = 0$ , and $g_{p} (h_{n} (v), h_{n} (v)) = g_{p} (v, v) + g_{p} (v, n)^{2}$ (The observer rest-space decomposition and the spatial projection clauses 1-2).

[L2]

For $P$ future timelike with rest mass $m > 0$ , $U = P / m$ , $u = U / c$ , $γ = - g_{p} (n, u)$ : $γ \geq 1$ , $E_{n} (P) = m c^{2} γ$ , $q_{n} (P) = m γ w$ , $g_{p} (q_{n}, q_{n}) = m^{2} c^{2} (γ^{2} - 1)$ with $w = c h_{n} (u) / γ$ , and $E_{n} (P) = - c g_{p} (P, n)$ , $q_{n} (P) = h_{n} (P)$ (Observer-relative energy, spatial momentum and rest mass of a tangent vector clauses (a)-(b), Positivity, relative-velocity identities and the mass shell of observer-relative energy and momentum clause 3).

[L3]

With $s : = \sqrt{g_{p} (w, w)}$ : $s < c$ , $γ = (1 - s^{2} / c^{2})^{- 1 / 2}$ , $E_{n} (P) = m c^{2} (1 - s^{2} / c^{2})^{- 1 / 2}$ , $∣ q_{n} (P) ∣ = m s (1 - s^{2} / c^{2})^{- 1 / 2}$ , and for every $0 \leq v_{0} < c$ with $z_{0} = v_{0}^{2} / c^{2} < 1$ and all $s \leq v_{0}$ the two error bounds of the statement of Low-velocity expansions of observer energy and momentum with uniform error bounds hold.

[L4]

In the inertial chart $g_{a b} = η_{a b} = diag (- 1, 1, 1, 1)$ ; $η (\partial_{0}, \partial_{0}) = - 1$ and $g_{p} (\partial_{1}, \partial_{1}) = 1$ (The flat model spacetime: the Minkowski metric on R^4 and its inertial chart, Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L5]

Arithmetic: $\sqrt{3}$ is the positive root of $3$ (Rational powers $a^{r}$ of a positive base) and $\frac{5}{3} < \sqrt{3} < 2$ , since $\frac{25}{9} < 3 < 4$ . Hence $\frac{2}{\sqrt{3}} = \frac{2 \sqrt{3}}{3}$ , $\frac{1}{\sqrt{3}} = \frac{\sqrt{3}}{3}$ , $\frac{1}{\sqrt{3}} - \frac{1}{2} = \frac{2 - \sqrt{3}}{2 \sqrt{3}} > 0$ , $9 \sqrt{3} < 16$ since $(9 \sqrt{3})^{2} = 243 < 256 = 16^{2}$ , and $27 \sqrt{3} > 46$ since $(27 \sqrt{3})^{2} = 2187 > 2116 = 46^{2}$ , both by squaring positive quantities; hence $\frac{16 - 9 \sqrt{3}}{8 \sqrt{3}} > 0$ .

Verification

technique · direct; evaluate the observer data and the mass-shell identities on the explicit vector $u$, then verify the two expansion bounds by exact algebraic comparison

1.1L1L2L4algebra

(Observer data.) By [L4], $g_{p} (n, n) = - 1$ , so $n$ is a unit future-directed timelike vector, i.e. an observer. Set $u$ as given; then $g_{p} (u, u) = \frac{4}{3} g_{p} (\partial_{0}, \partial_{0}) + \frac{1}{3} g_{p} (\partial_{1}, \partial_{1}) = - \frac{4}{3} + \frac{1}{3} = - 1$ , so $u$ is future timelike with $g_{p} (u, u) = - 1$ , and $P = m c u$ is future timelike with rest mass $m (P) = m$ by [L2]. Further $g_{p} (n, u) = - \frac{2}{\sqrt{3}}$ , so by [L1] $h_{n} (u) = u + g_{p} (n, u) n = \frac{2}{\sqrt{3}} \partial_{0} + \frac{1}{\sqrt{3}} \partial_{1} - \frac{2}{\sqrt{3}} \partial_{0} = \frac{1}{\sqrt{3}} \partial_{1}$ . Hence $γ = - g_{p} (n, u) = \frac{2}{\sqrt{3}} \geq 1$ , $w = c h_{n} (u) / γ = \frac{c}{2} \partial_{1}$ , and $s = \sqrt{g_{p} (w, w)} = \frac{c}{2}$ by [L4].

2.1step 1.1L1L2L4algebra

(Exact energy and momentum.) By [L2] and [L4]: $E_{n} (P) = - c g_{p} (P, n) = - m c^{2} g_{p} (u, \partial_{0}) = m c^{2} \cdot \frac{2}{\sqrt{3}}$ and $q_{n} (P) = h_{n} (P) = m c h_{n} (u) = \frac{m c}{\sqrt{3}} \partial_{1}$ , so $∣ q_{n} (P) ∣ = \sqrt{g_{p} (q_{n}, q_{n})} = \frac{m c}{\sqrt{3}}$ since $g_{p} (\partial_{1}, \partial_{1}) = 1$ .

3.1step 1.1step 2.1L3L5algebra

(Exact identities at $s = c / 2$ .) By step 1.1, $s = c / 2 < c$ and $1 - s^{2} / c^{2} = 3 / 4$ , so $(1 - s^{2} / c^{2})^{- 1 / 2} = 2 / \sqrt{3}$ ; step 2.1 gives $E_{n} (P) = m c^{2} \cdot \frac{2}{\sqrt{3}} = m c^{2} (1 - s^{2} / c^{2})^{- 1 / 2}$ and $∣ q_{n} (P) ∣ = \frac{m c}{\sqrt{3}} = m \cdot \frac{c}{2} \cdot \frac{2}{\sqrt{3}} = m s (1 - s^{2} / c^{2})^{- 1 / 2}$ , which are the exact identities of [L3].

4.1step 3.1L3L5algebra

(Energy bound.) By step 3.1, $∣ E_{n} (P) - m c^{2} - \frac{1}{2} m s^{2} ∣ = m c^{2} ∣ \frac{2}{\sqrt{3}} - 1 - \frac{1}{8} ∣ = m c^{2} (\frac{2}{\sqrt{3}} - \frac{9}{8}) = m c^{2} \frac{16 - 9 \sqrt{3}}{8 \sqrt{3}}$ , the sign being positive by [L5]. The bound of [L3] at $v_{0} = c / 2$ is $\frac{3}{8} (\frac{3}{4})^{- 5 / 2} m \frac{(c / 2)^{4}}{c^{2}} = \frac{3}{8} \cdot \frac{32}{9 \sqrt{3}} \cdot \frac{m c^{2}}{16} = \frac{m c^{2}}{12 \sqrt{3}}$ using $(\frac{4}{3})^{5 / 2} = \frac{16}{9} \cdot \frac{2}{\sqrt{3}}$ and $\sqrt{3} > 0$ . The inequality $\frac{16 - 9 \sqrt{3}}{8 \sqrt{3}} \leq \frac{1}{12 \sqrt{3}}$ is equivalent, upon multiplying by the positive $24 \sqrt{3}$ , to $3 (16 - 9 \sqrt{3}) \leq 2$ , i.e. $27 \sqrt{3} \geq 46$ , which holds by [L5].

5.1step 3.1step 4.1L3L5algebra∎

(Momentum bound.) By step 3.1, $∣ ∣ q_{n} (P) ∣ - m s ∣ = m c ∣ \frac{1}{\sqrt{3}} - \frac{1}{2} ∣ = m c (\frac{1}{\sqrt{3}} - \frac{1}{2}) = m c \frac{2 - \sqrt{3}}{2 \sqrt{3}}$ by [L5]. The bound of [L3] at $v_{0} = c / 2$ is $\frac{1}{2} (\frac{3}{4})^{- 3 / 2} m \frac{(c / 2)^{3}}{c^{2}} = \frac{1}{2} \cdot \frac{8}{3 \sqrt{3}} \cdot \frac{m c}{8} = \frac{m c}{6 \sqrt{3}}$ using $(\frac{4}{3})^{3 / 2} = \frac{4}{3} \cdot \frac{2}{\sqrt{3}}$ . The inequality $\frac{2 - \sqrt{3}}{2 \sqrt{3}} \leq \frac{1}{6 \sqrt{3}}$ is equivalent, upon multiplying by the positive $6 \sqrt{3}$ , to $3 (2 - \sqrt{3}) \leq 1$ , i.e. $3 \sqrt{3} \geq 5$ , which holds since $27 > 25$ and both sides are positive. Both bounds of the lemma are therefore satisfied strictly at the relative speed $s = c / 2$ , and the exact identities of step 3.1 verify its statements $s < c$ , $γ = (1 - s^{2} / c^{2})^{- 1 / 2}$ and the two displayed formulas.

Scope. The example is a finite algebraic check of the kinematic identities and error bounds at one relative speed; it involves no dynamics, no conservation law and no measurement. The choices $s = c / 2$ and the direction $\partial_{1}$ are arbitrary normalizations; the points checked are the exact identities and the two strict inequalities.

An exact observer-relative energy and momentum computation at relative speed c/2, with the expansion bounds of the low-velocity lemma checked by exact rational comparison

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources