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 explicit null geodesic in an exponentially expanding flat FLRW datum: constant aV^t and the observer-energy ratio

Example

Fix real constants $c > 0$ , $A > 0$ , $H > 0$ , $t_{0} \in R$ , $r_{0} \in R$ . Let $(I, Σ, γ, k, a)$ be the FLRW model datum with $I = R$ , $Σ = R^{3}$ carrying the standard Euclidean metric $γ$ in the standard coordinates $x = (x^{1}, x^{2}, x^{3})$ , $k = 0$ and $a (t) : = A \exp (H (t - t_{0}))$ (FLRW model data: warped product metric, cosmic time, comoving congruence, scale factor and Hubble parameter, Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model). On the spacetime $M = I \times Σ$ define the curve $η : (0, \infty) \to M$ ,

$η (s) : = (t (s), (r_{0} + \frac{c}{A H^{2} s}, 0, 0)), t (s) : = t_{0} + \frac{1}{H} \log (H s),$

and let $V : = η^{'}$ with components $V^{t} = d t / d s$ , $V^{1}, V^{2}, V^{3}$ . Then:

The curve $η$ is smooth and its tangent $V$ is a future-directed null vector, $g (V, V) = 0$ and $V^{t} > 0$ , at every point of $(0, \infty)$ ; moreover $η$ is a geodesic of the metric-selected connection with affine parameter $s$ , in the sense of Geodesic of an affine connection.
Along $η$ the product $a (t (s)) V^{t} (s)$ is the constant $A$ ; in particular $a V^{t}$ is preserved by the flow of the null geodesic.
For $0 < s_{E} < s_{R}$ let $t_{E} = t (s_{E})$ , $t_{R} = t (s_{R})$ , let $n = c^{- 1} \partial_{t}$ be the comoving congruence of the datum and let $E (s) : = - c g_{η (s)} (V (s), n (η (s)))$ be the observer energy of Observer-relative energy, spatial momentum and rest mass of a tangent vector clause (a). Then $E (s) = c^{2} / (H s) > 0$ and

$\frac{E (s_{R})}{E (s_{E})} = \frac{a (t_{E})}{a (t_{R})} = \frac{s_{E}}{s_{R}} .$

Facts & Assumptions

Given: The constants $c, A, H, t_{0}, r_{0}$ with $c > 0$ , $A > 0$ , $H > 0$ , the FLRW model datum of the example, its spacetime $M = R \times R^{3}$ , metric $g$ , comoving congruence $n = c^{- 1} \partial_{t}$ and metric-selected connection $\nabla$ , and the curve $η$ with tangent $V$ .

[L1]

In the product chart $(x^{0}, x^{1}, x^{2}, x^{3}) = (t, x^{1}, x^{2}, x^{3})$ the Christoffel symbols of $\nabla$ are $Γ^{0}_{i j} = (a \dot{a} / c^{2}) γ_{i j}$ , $Γ^{i}_{0 j} = Γ^{i}_{j 0} = H_{F L} δ^{i}_{j}$ with $H_{F L} = \dot{a} / a$ , $Γ^{i}_{j k} =^{(3)} Γ^{i}_{j k}$ , and all others vanish; here $γ$ is the Euclidean metric in the standard coordinates, so $^{(3)} Γ^{i}_{j k} = 0$ (Christoffel symbols of the FLRW metric in product charts, Metric compatibility, torsion freedom and the metric-selected connection class).

[L2]

In a chart a smooth curve is a geodesic with affine parameter $s$ if and only if ${\dot{V}}^{a} + \sum_{b, c} Γ^{a}_{b c} V^{b} V^{c} = 0$ for $a = 0, 1, 2, 3$ on every parameter subinterval lying in the chart (Coordinate geodesic equation, Geodesic of an affine connection).

[L3]

The comoving congruence $n = c^{- 1} \partial_{t}$ is a smooth future-directed unit timelike field, $g (n, n) = - 1$ ; a nonzero vector $V$ is future-directed exactly when $g (V, \partial_{t}) < 0$ , and null exactly when $g (V, V) = 0$ (The FLRW metric is smooth Lorentzian; the comoving field is unit timelike and cosmic time parametrizes comoving curves by proper time; the slices carry the scaled spatial metric, Timelike, null, spacelike and causal vectors of a Lorentz vector space, Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L4]

The observer energy is $E_{n} (P) = - c g_{p} (P, n_{p})$ , and for the unit field $n = c^{- 1} \partial_{t}$ the pairing with a vector $V$ is $g (V, n) = - c V^{t}$ , where $V^{t} = d t (V)$ in the product chart (Observer-relative energy, spatial momentum and rest mass of a tangent vector, The FLRW metric is smooth Lorentzian; the comoving field is unit timelike and cosmic time parametrizes comoving curves by proper time; the slices carry the scaled spatial metric).

[L5]

On $(0, \infty)$ the functions $s \mapsto 1 / (H s)$ and $s \mapsto r_{0} + c / (A H^{2} s)$ are smooth with derivatives $- 1 / (H s^{2})$ and $- c / (A H^{2} s^{2})$ . The exponential is smooth with $\exp^{'} = \exp$ and the natural logarithm is its inverse on $(0, \infty)$ with $\log^{'} (x) = 1 / x$ (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$ , 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)$ , The real exponential function and the number $e$ by a power series, The exponential function is smooth and $(\exp)^{'} = \exp$ , The natural logarithm as the inverse of the exponential function, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

Verification

1.1L5algebra

(Tangents.) By [L5] the curve $η$ is smooth on $(0, \infty)$ and its tangent has components $V^{t} (s) = \frac{1}{H s} > 0, V^{1} (s) = - \frac{c}{A H^{2} s^{2}}, V^{2} (s) = V^{3} (s) = 0.$

2.1L3L5step 1.1algebra

(Nullness and future direction.) By [L5], $a (t (s)) = A \exp (H (t (s) - t_{0})) = A \cdot H s$ , so $a (t (s)) V^{1} (s) = A H s \cdot (- c / (A H^{2} s^{2})) = - c / (H s) = - c V^{t} (s)$ . Hence $a^{2} (V^{1})^{2} = c^{2} (V^{t})^{2}$ , and since $V^{2} = V^{3} = 0$ the metric pairing is $g (V, V) = - c^{2} (V^{t})^{2} + a^{2} (V^{1})^{2} = 0$ : $V$ is null. Since $V^{t} (s) > 0$ , [L3] gives $g (V, \partial_{t}) = - c^{2} V^{t} < 0$ , so $V$ is future-directed.

2.2L1L2L5step 1.1algebra

(Geodesic equations.) By [L1] the nonvanishing symbol families in the product chart are $Γ^{0}_{i j} = a \dot{a} δ_{i j} / c^{2}$ and $Γ^{i}_{0 j} = Γ^{i}_{j 0} = H_{F L} δ^{i}_{j}$ , where $\dot{a} = H a$ gives $H_{F L} = H$ . Since $V^{2} = V^{3} = 0$ , only $Γ^{0}_{11} = H a^{2} / c^{2}$ contributes to the time-component equation, while the two symmetric mixed symbols give the factor $2$ in the spatial equations. The $t$ -equation of [L2] reads ${\dot{V}}^{t} + \frac{H a^{2}}{c^{2}} (V^{1})^{2} = 0$ : by step 1.1 and [L5], ${\dot{V}}^{t} = - 1 / (H s^{2})$ and $\frac{H a^{2}}{c^{2}} (V^{1})^{2} = \frac{H (A H s)^{2}}{c^{2}} \cdot \frac{c^{2}}{A^{2} H^{4} s^{4}} = \frac{1}{H s^{2}}$ , so the equation holds. The $x^{1}$ -equation reads ${\dot{V}}^{1} + 2 H V^{t} V^{1} = 0$ : by step 1.1, ${\dot{V}}^{1} = 2 c / (A H^{2} s^{3})$ and $2 H V^{t} V^{1} = 2 H \frac{1}{H s} (- \frac{c}{A H^{2} s^{2}}) = - \frac{2 c}{A H^{2} s^{3}}$ , so the equation holds. For $a = 2$ the equation of [L2] reads ${\dot{V}}^{2} + 2 H V^{t} V^{2} = 0$ , and it holds because $V^{2} = 0$ and ${\dot{V}}^{2} = 0$ ; the $a = 3$ equation is identical with $V^{3} = 0$ . Hence $η$ is a geodesic with affine parameter $s$ .

3.1L5step 1.1step 2.1step 2.2algebra

(The conserved product.) By step 1.1 and the identity $a (t (s)) = A H s$ of [L5], $a (t (s)) V^{t} (s) = A H s \cdot \frac{1}{H s} = A$ for every $s \in (0, \infty)$ : $a V^{t}$ is constant along the ray with value $A$ . This proves claims 1 and 2.

4.1L4step 1.1step 3.1algebra

(Observer energies and their ratio.) By [L4], $E (s) = - c g (V (s), n) = - c \cdot (- c V^{t} (s)) = c^{2} V^{t} (s) = \frac{c^{2}}{H s} > 0$ . Hence $\frac{E (s_{R})}{E (s_{E})} = \frac{s_{E}}{s_{R}}$ , and since $a (t (s)) = A H s$ we also have $\frac{a (t_{E})}{a (t_{R})} = \frac{s_{E}}{s_{R}}$ ; combining the two equalities proves the displayed energy ratio.

5.1step 1.1step 2.1step 2.2step 3.1step 4.1∎

(Conclusion.) Steps 1.1, 2.1 and 2.2 exhibit a smooth future-directed null geodesic with affine parameter $s$ , step 3.1 verifies the conservation law $a V^{t} = constant$ in this explicit family, and step 4.1 verifies the observer-energy ratio $\frac{E (s_{R})}{E (s_{E})} = \frac{a (t_{E})}{a (t_{R})}$ between comoving observers. The verification used only the metric, its Christoffel symbols and the observer-energy definition; no field equation and no matter model was used, and no physical claim about a measured wavelength is made.

Remarks

Independence from the field equations. The family $η$ exists for every exponential scale factor, whatever the matter content or the value of the cosmological parameter, because the computation uses only the metric geometry. It is a special case of the general conservation law of the A page, verified here by explicit coordinates.
Physical reading. The relation $\frac{E (s_{R})}{E (s_{E})} = \frac{a (t_{E})}{a (t_{R})}$ is a model prediction about ideal observer energies of an ideal null geodesic; identifying $E$ with an observed frequency requires the light propagation and measurement model of the framework, and no such identification or measurement is asserted here.
Choice of zero. The parameter $s$ ranges over $(0, \infty)$ and $t (s) \to \pm \infty$ as $s \to 0^{+}, \infty$ ; the ray is defined on the whole cosmic time axis. Only the ratio of energies is asserted, so the additive freedom in the affine parameter and the constant $r_{0}$ do not enter.

An explicit null geodesic in an exponentially expanding flat FLRW datum: constant aV^t and the observer-energy ratio

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources