Alphabeta Math
Pipeline-generated
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.

Cosmological dynamics and anisotropic shear — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

Nonflat anisotropic Kasner exponents

Example

On any nonempty open interval I⊆(0,∞), the exponents (p1,p2,p3)=(−1/3,2/3,2/3) with ai=Ai(t/t0)pi, Ai>0 lengths in metres and t0>0 a time in seconds, give a nonstatic Ricci-flat diagonal Bianchi I metric. Its directional expansion rates are unequal, the scalar σ2:=12∑i(Hi−H)2 equals 1/(3t2), and its curvature component R0101=−4a12/(9t2) is nonzero. Thus the Riemann tensor is nonzero and the metric is not flat.

Facts & Assumptions

Given: The stated power-law Bianchi I metric with Ai>0, t0>0, and t∈I⊆(0,∞), in the inherited ACω context.

[A1]

The Bianchi I product and quotient construction carries ACω and no stronger choice principle (Diagonal Bianchi I model).

[F1]

The rates, mean expansion, volume and shear scalar are Hi=a˙i/ai, H=13∑iHi, V=∏iai and σ2=12∑i(Hi−H)2 (Diagonal Bianchi I model).

[F2]

The C2 connection and curvature use the coordinate order Rabcd and the definitions of Ric⁡ and G stated on this page (C2 curvature for the diagonal Bianchi I quotient metric).

[F3]

R0i0i=−ai2(H˙i+Hi2) and Ric⁡00,Ric⁡ii have the explicit component formulas in the curvature lemma (Curvature components of the diagonal Bianchi I metric).

[F4]

For a nonstatic power-law Bianchi I metric, Ric⁡=0 exactly when ∑ipi=∑ipi2=1 (Kasner vacuum constraints).

[F5]

With isotropic diagonal source, V(Hi−Hj) is constant and σ2=C V−2, where C has units m6s−2; the zero source is isotropic (Diagonal-source shear equation and isotropic-source decay).

Verification

technique · direct finite substitution and one explicit curvature component
1.1givenA1F4algebra

Work under the inherited ACω context [A1]. For p=(−1/3,2/3,2/3), ∑ipi=1 and ∑ipi2=1/9+4/9+4/9=1; none of the exponents is zero, so [F4] gives the Ricci-flat conclusion.

2.1step 1.1F1F2F5algebra

The rates are H1=−1/(3t) and H2=H3=2/(3t), so H=1/(3t), V=A1A2A3(t/t0) and σ2=12(4/9+1/9+1/9)t−2=1/(3t2). By Ricci-flatness from step 1.1 and the definition in [F2], R=0 and Gii=0 for every i. Thus the spatial equations in [F5] hold with Λ=0 and isotropic source Qi=0, giving V2σ2=(A1A2A3)2/(3t02).

3.1step 1.1F2F3algebra∎

From [F3], R0101=−a12(H˙1+H12)=−a12(1/(3t2)+1/(9t2))=−4a12/(9t2)≠0 throughout I. Thus the metric has nonzero curvature and is not flat, while step 1.1 established Ricci-flatness.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

A locally flat Kasner coordinate branch

Example

For lengths Ai>0 in metres and a time t0>0 in seconds, set I=(0,∞) and take the exponents (p1,p2,p3)=(1,0,0), so a1=A1(t/t0) and a2=A2, a3=A3. They satisfy ∑ipi=1 and ∑ipi2=1, and the corresponding diagonal Bianchi I metric is Ricci-flat with identically zero Riemann tensor on I. Define the open coordinate domain D:={(T,X,z2,z3)∈R4:T>∣X∣} and its Minkowski metric η:=−dT2+dX2+dz22+dz32, with all four coordinates measured in metres. In any local quotient chart with lifted dimensionless angular coordinates x1,x2,x3, let α:=A1/(ct0) and define

Φ(t,x1,x2,x3):=(ctcosh⁡(αx1),  ctsinh⁡(αx1),  A2x2,  A3x3).

This map is a local isometry from the chart domain, with the Bianchi I metric, onto an open subset of (D,η). Its scale factor a1 tends to zero as t↓0, but that excluded coordinate boundary alone does not establish curvature blowup or a global extension on the torus quotient.

Facts & Assumptions

Given: The stated power-law Bianchi I metric on I=(0,∞) with Ai>0 lengths in metres and t0>0 seconds, a local lift of the periodic angular coordinates, and the inherited ACω context.

[A1]

The Bianchi I product and quotient construction carries ACω and no stronger choice principle (Diagonal Bianchi I model).

[F1]

Hi=a˙i/ai, H=13∑iHi, V=∏iai, and σ2=12∑i(Hi−H)2 (Diagonal Bianchi I model).

[F2]

The local C2 curvature convention defines the Riemann tensor from the displayed connection coefficients and uses the stated sign/index order (C2 curvature for the diagonal Bianchi I quotient metric).

[F3]

The curvature components are R0i0i=−ai2(H˙i+Hi2) and Rijij=ai2aj2HiHj/c2; all other independent index patterns vanish (Curvature components of the diagonal Bianchi I metric).

[F4]

In a nonstatic power-law branch, Ricci-flatness is equivalent to the two Kasner sums; the all-zero exponent case is separately flat (Kasner vacuum constraints).

[F5]

For isotropic diagonal source, each V(Hi−Hj) is constant and V2σ2 is constant with units m6s−2 (Diagonal-source shear equation and isotropic-source decay).

Verification

technique · direct component substitution followed by an explicit local coordinate change
1.1givenA1F4algebra

Work under the inherited ACω context [A1]. The exponents have ∑ipi=1 and ∑ipi2=1, so [F4] gives the Ricci-flat conclusion for this nonstatic branch.

2.1step 1.1F1F2F3F5algebra

The directional rates are H1=1/t and H2=H3=0. Thus every H˙i+Hi2 is zero and every product HiHj with i≠j is zero; [F3] makes every independent Riemann component vanish, hence the full curvature tensor vanishes on I. Also H=1/(3t), V=A1A2A3(t/t0) and σ2=1/(3t2). Since step 1.1 and [F2] give R=0 and Gii=0, the equations in [F5] hold with Λ=0 and Qi=0, yielding V2σ2=(A1A2A3)2/(3t02).

3.1step 2.1F2algebra∎

On the lifted chart, put r=ct>0 and θ=αx1. Then (T,X)=(rcosh⁡θ,rsinh⁡θ) satisfies T>∣X∣, and the inverse in its image is t=T2−X2/c, x1=artanh⁡(X/T)/α, x2=z2/A2, and x3=z3/A3. Thus Φ is a diffeomorphism onto an open subset of D. The identities −dT2+dX2=−dr2+r2dθ2=−c2dt2+a1(t)2(dx1)2 and (dz2)2+(dz3)2=a22(dx2)2+a32(dx3)2 give Φ∗η=g. The local lift does not define a global coordinate transformation of the periodic torus. Since all curvature components already vanish for every t>0, the collapse of a1 at the excluded endpoint t=0 alone proves no curvature blowup.

Sources