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
- Absolute and Conditional Convergence; Rearrangement; Products
- Approximation and Compactness in C(K)
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Connectedness
- Connections And Free Fall
- Connections Levi Civita and Parallel Transport
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Convergence: Nets and Filters
- Cosets, Index and Lagrange's Theorem
- Cosmological dynamics and anisotropic shear
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Curvature And Tides
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Framework And Geometry
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Geodesics, the Exponential Map, Completeness, and Hopf–Rinow
- Gr14 Full High Regularity Symmetric Hyperbolic Proof
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Hereditary and Productive Behaviour of the Separation Axioms
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Rank Theorems and Embedded Submanifolds
- Relations, Functions, and Quotients
- Riemann Curvature and Riemannian Submanifolds
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Smooth Vector Bundles and Sections
- Spacetime Primitives
- Stone–Weierstrass in General
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tensor Fields Exterior Algebra and Differential Forms
- Tensors And Observers
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Fields Flows and Lie Derivatives
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Derivatives and Sobolev Spaces
2 · Summary
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Nonflat anisotropic Kasner exponents
Example
On any nonempty open interval , the exponents with , lengths in metres and a time in seconds, give a nonstatic Ricci-flat diagonal Bianchi I metric. Its directional expansion rates are unequal, the scalar equals , and its curvature component is nonzero. Thus the Riemann tensor is nonzero and the metric is not flat.
Example references
Facts & Assumptions
Given: The stated power-law Bianchi I metric with , , and , in the inherited context.
The Bianchi I product and quotient construction carries and no stronger choice principle (Diagonal Bianchi I model).
The rates, mean expansion, volume and shear scalar are , , and (Diagonal Bianchi I model).
The C2 connection and curvature use the coordinate order and the definitions of and stated on this page (C2 curvature for the diagonal Bianchi I quotient metric).
and have the explicit component formulas in the curvature lemma (Curvature components of the diagonal Bianchi I metric).
For a nonstatic power-law Bianchi I metric, exactly when (Kasner vacuum constraints).
With isotropic diagonal source, is constant and , where has units ; the zero source is isotropic (Diagonal-source shear equation and isotropic-source decay).
Verification
Work under the inherited context [A1]. For , and ; none of the exponents is zero, so [F4] gives the Ricci-flat conclusion.
The rates are and , so , and . By Ricci-flatness from step 1.1 and the definition in [F2], and for every . Thus the spatial equations in [F5] hold with and isotropic source , giving .
From [F3], throughout . Thus the metric has nonzero curvature and is not flat, while step 1.1 established Ricci-flatness.
A locally flat Kasner coordinate branch
Example
For lengths in metres and a time in seconds, set and take the exponents , so and , . They satisfy and , and the corresponding diagonal Bianchi I metric is Ricci-flat with identically zero Riemann tensor on . Define the open coordinate domain and its Minkowski metric , with all four coordinates measured in metres. In any local quotient chart with lifted dimensionless angular coordinates , let and define
This map is a local isometry from the chart domain, with the Bianchi I metric, onto an open subset of . Its scale factor tends to zero as , but that excluded coordinate boundary alone does not establish curvature blowup or a global extension on the torus quotient.
Example references
Facts & Assumptions
Given: The stated power-law Bianchi I metric on with lengths in metres and seconds, a local lift of the periodic angular coordinates, and the inherited context.
The Bianchi I product and quotient construction carries and no stronger choice principle (Diagonal Bianchi I model).
, , , and (Diagonal Bianchi I model).
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).
The curvature components are and ; all other independent index patterns vanish (Curvature components of the diagonal Bianchi I metric).
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).
For isotropic diagonal source, each is constant and is constant with units (Diagonal-source shear equation and isotropic-source decay).
Verification
Work under the inherited context [A1]. The exponents have and , so [F4] gives the Ricci-flat conclusion for this nonstatic branch.
The directional rates are and . Thus every is zero and every product with is zero; [F3] makes every independent Riemann component vanish, hence the full curvature tensor vanishes on . Also , and . Since step 1.1 and [F2] give and , the equations in [F5] hold with and , yielding .
On the lifted chart, put and . Then satisfies , and the inverse in its image is , , , and . Thus is a diffeomorphism onto an open subset of . The identities and give . The local lift does not define a global coordinate transformation of the periodic torus. Since all curvature components already vanish for every , the collapse of at the excluded endpoint alone proves no curvature blowup.