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.

Direct check of the flat power-law data against the Friedmann-system equations

Example

Fix real constants $c > 0$ , $G_{N} > 0$ , $A > 0$ , $t_{*} > 0$ , $t_{0} \in R$ and $w > - 1$ , and put

$q : = \frac{2}{3 (1 + w)}, I : = (t_{0}, \infty), a (t) : = A (\frac{t - t_{0}}{t_{*}})^{q}, ε (t) : = \frac{3 c^{2} q^{2}}{8 π G_{N} (t - t_{0})^{2}}, p (t) : = w ε (t),$

with real powers in the sense of Real powers for positive bases, with the zero-base positive-exponent convention. Then:

The functions $a, ε, p$ are smooth on $I$ , $a (t) > 0$ and $ε (t) > 0$ for every $t \in I$ , and on $I$

$H (t) = \frac{q}{t - t_{0}}, \frac{\ddot{a} (t)}{a (t)} = \frac{q (q - 1)}{(t - t_{0})^{2}} .$

The Friedmann-system datum $(c, G_{N}, 0, I, 0, a, ε, p)$ satisfies the Friedmann equation (F), the acceleration equation (A), the continuity equation (C) and the spatial-component equation (S) of The Friedmann, acceleration and continuity equations of an FLRW model datum on $I$ . In particular $w = 0$ gives $q = \frac{2}{3}$ and $w = \frac{1}{3}$ gives $q = \frac{1}{2}$ .

Facts & Assumptions

Given: The constants $c, G_{N}, A, t_{*}, t_{0}, w$ with $c > 0$ , $G_{N} > 0$ , $A > 0$ , $t_{*} > 0$ , $w > - 1$ , the interval $I = (t_{0}, \infty)$ , the functions $a, ε, p$ of the example, and the equations (F), (A), (C), (S) of The Friedmann, acceleration and continuity equations of an FLRW model datum.

[L1]

For $x > 0$ and real $α$ the real power $x^{α} = \exp (α \log x)$ is strictly positive, continuous and differentiable on $(0, \infty)$ with $(x^{α})^{'} = α x^{α - 1}$ , and $(x^{α})^{β} = x^{α β}$ for real $β$ (Real powers for positive bases, with the zero-base positive-exponent convention, Continuity and derivatives of positive-base real powers, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents). Smoothness on an open real interval means that derivatives of every finite order exist and are continuous; it will be established locally in step 1.1.

[L2]

Smooth functions on intervals satisfy the sum, product, quotient and chain rules; in particular, if $u$ is smooth and strictly positive and $α$ is real, then $\frac{d}{d t} u^{α} = α u^{α - 1} \dot{u}$ , and the derivative of a constant function is $0$ (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 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, For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).

[L3]

The equations of The Friedmann, acceleration and continuity equations of an FLRW model datum with $k = Λ = 0$ read

$H^{2} = \frac{8 π G_{N}}{3 c^{2}} ε, \frac{\ddot{a}}{a} = - \frac{4 π G_{N}}{3 c^{2}} (ε + 3 p), \dot{ε} + 3 H (ε + p) = 0, - \frac{2 a \ddot{a} + {\dot{a}}^{2}}{c^{2}} = \frac{8 π G_{N}}{c^{4}} p a^{2},$

where the first display is (F), the second (A), the third (C) and the fourth (S), each required at every point of $I$ .

[L4]

The defining relations $q = 2 / (3 (1 + w))$ and $w > - 1$ give $q > 0$ and $3 (1 + w) q = 2$ ; equivalently $1 + w = 2 / (3 q)$ and $3 q (1 + w) = 2$ .

Verification

1.1L1L2L4givenalgebra

(Smoothness and positivity.) Put $u (t) : = (t - t_{0}) / t_{*} > 0$ on $I$ . For every real $α$ and integer $m \geq 0$ , repeated application of [L1] and [L2] gives $\frac{d^{m}}{d t^{m}} u (t)^{α} = t_{*}^{- m} (\prod_{r = 0}^{m - 1} (α - r)) u (t)^{α - m}$ , with empty product $1$ : at $m = 0$ this is the function itself, and differentiating the formula at $m$ introduces the factor $(α - m) / t_{*}$ and lowers the exponent by one, proving the formula at $m + 1$ . Each derivative is continuous by [L1] and continuity of the affine function $u$ , so $u^{α}$ is smooth. Taking $α = q$ proves smoothness of $a = A u^{q}$ ; the same argument with the positive affine function $v (t) = t - t_{0}$ , whose derivative is $1$ , and $α = - 2$ proves smoothness of $ε = 3 c^{2} q^{2} v^{- 2} / (8 π G_{N})$ and hence of $p = w ε$ . Finally $a > 0$ by [L1] and $A > 0$ , and $ε > 0$ because $c, G_{N} > 0$ , $q > 0$ by [L4], and $v > 0$ .

2.1L1L2step 1.1algebra

(Derivatives and the Hubble parameter.) By [L2], $\dot{u} = 1 / t_{*}$ and $\dot{a} = A q u^{q - 1} \dot{u} = A q u^{q - 1} / t_{*}$ . Since $u^{q} / (t - t_{0}) = u^{q - 1} / t_{*}$ , this is $\dot{a} = q a / (t - t_{0})$ , so $H = \dot{a} / a = q / (t - t_{0})$ . Differentiating $\dot{a} = q a / (t - t_{0})$ by the product and quotient rules gives $\ddot{a} = q (\dot{a} (t - t_{0}) - a) / (t - t_{0})^{2} = q (q - 1) a / (t - t_{0})^{2}$ , hence $\ddot{a} / a = q (q - 1) / (t - t_{0})^{2}$ . Also $\dot{ε} = - 6 c^{2} q^{2} / (8 π G_{N} (t - t_{0})^{3}) = - 2 ε / (t - t_{0})$ . This proves claim 1.

3.1L3step 2.1algebra

(Friedmann equation.) By [L3], (F) with $k = 0$ is $H^{2} = 8 π G_{N} ε / (3 c^{2})$ . By step 2.1, $H^{2} = q^{2} / (t - t_{0})^{2}$ ; by the definition of $ε$ , $\frac{8 π G_{N}}{3 c^{2}} ε = \frac{8 π G_{N}}{3 c^{2}} \cdot \frac{3 c^{2} q^{2}}{8 π G_{N} (t - t_{0})^{2}} = \frac{q^{2}}{(t - t_{0})^{2}}$ . The two sides agree at every point of $I$ .

3.2L3L4step 2.1algebra

(Acceleration equation.) By [L3], (A) with $Λ = 0$ is $\ddot{a} / a = - 4 π G_{N} (ε + 3 p) / (3 c^{2})$ . By step 2.1 and $p = w ε$ , the left-hand side is $q (q - 1) / (t - t_{0})^{2}$ and the right-hand side is $- \frac{4 π G_{N}}{3 c^{2}} (1 + 3 w) \frac{3 c^{2} q^{2}}{8 π G_{N} (t - t_{0})^{2}} = - \frac{(1 + 3 w) q^{2}}{2 (t - t_{0})^{2}}$ . Since $q > 0$ by [L4], the needed identity $q (q - 1) = - \frac{1}{2} (1 + 3 w) q^{2}$ is equivalent to $2 q - 2 = - (1 + 3 w) q$ , that is, to $3 (1 + w) q = 2$ , which is [L4]. Hence (A) holds.

3.3L3L4step 2.1algebra

(Continuity equation.) By step 2.1, $\dot{ε} = - 2 ε / (t - t_{0})$ ; by steps 2.1 and [L4], $3 H (ε + p) = 3 \frac{q}{t - t_{0}} (1 + w) ε$ and $3 q (1 + w) = 2$ , so $3 H (ε + p) = 2 ε / (t - t_{0})$ . Hence $\dot{ε} + 3 H (ε + p) = 0$ on $I$ , which is (C).

3.4L3L4step 2.1algebra

(Spatial-component equation.) By [L3], (S) with $k = Λ = 0$ is $- (2 a \ddot{a} + {\dot{a}}^{2}) / c^{2} = 8 π G_{N} p a^{2} / c^{4}$ . By step 2.1, $2 a \ddot{a} + {\dot{a}}^{2} = (2 q (q - 1) + q^{2}) a^{2} / (t - t_{0})^{2} = (3 q^{2} - 2 q) a^{2} / (t - t_{0})^{2}$ ; the right-hand side is $\frac{8 π G_{N}}{c^{4}} w \frac{3 c^{2} q^{2}}{8 π G_{N} (t - t_{0})^{2}} a^{2} = \frac{3 w q^{2} a^{2}}{c^{2} (t - t_{0})^{2}}$ . Equality of the two displayed expressions is equivalent to $- (3 q^{2} - 2 q) = 3 w q^{2}$ , that is, to $2 q = 3 q^{2} (1 + w)$ , which holds because $3 q (1 + w) = 2$ by [L4]; hence (S) holds.

4.1step 1.1step 2.1step 3.1step 3.2step 3.3step 3.4∎

(Conclusion.) Steps 1.1 and 2.1 establish claim 1, and steps 3.1, 3.2, 3.3 and 3.4 establish (F), (A), (C) and (S) at every point of $I$ , which is claim 2; the last sentence of claim 2 is the substitution $w = 0$ , $w = \frac{1}{3}$ in $q = 2 / (3 (1 + w))$ . No equation of state beyond $p = w ε$ , no field equation and no physical premise was used.

Remarks

What is checked. The example verifies the displayed data against all four scalar equations of The Friedmann, acceleration and continuity equations of an FLRW model datum by direct differentiation; in particular it does not invoke the equivalence proposition of the A page, so it independently exhibits data satisfying (F), (A), (C) and (S) simultaneously. The physically interpreted field-equation reading of these data belongs to the physics theorem on the A page and is not asserted here.
What is not claimed. No uniqueness, no statement about the limit $t ↓ t_{0}$ , no extension beyond $I$ and no numerical value of any constant is asserted; $A$ , $t_{*}$ and $t_{0}$ are arbitrary real model data with $A > 0$ , $t_{*} > 0$ .

Direct check of the flat power-law data against the Friedmann-system equations

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources