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.
Finite Killing energy current and reference normalization — Examples
1 · Prerequisites
- Abelian Categories
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Categories, Functors and Natural Transformations
- Chain Complexes and Homology
- Cm Math Continuum
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- 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
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Einstein And Matter
- Euclidean Ordinary Differential Equations with Smooth Dependence
- Exterior Powers, Orientation and Hodge Duality
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Killing energy current and reference normalization
- Finite spacelike slab and normal flux charge
- Foundations of the Real Numbers for Analysis
- Framework And Geometry
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fubini and Change of Variables
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Geodesics, the Exponential Map, Completeness, and Hopf–Rinow
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Hereditary and Productive Behaviour of the Separation Axioms
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Integration of Forms and the General Stokes Theorem
- Limits and Colimits
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Manifolds with Boundary Collars and Orientations
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Picard-Lindelöf and First-Order Ordinary Differential Equations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Preadditive and Additive Categories and Biproducts
- Properties of the Integral and the Working FTC
- Rank Theorems and Embedded Submanifolds
- Relations, Functions, and Quotients
- Riemann Curvature and Riemannian Submanifolds
- Riemannian Metrics Length Distance and Volume
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Simplicial Complexes and Simplicial Homology
- Singular Chains and Singular Homology
- Singular Cochains Mayer Vietoris and Smooth Singular Comparison
- Singular Cohomology and Coefficient Theorems
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Smooth Vector Bundles and Sections
- Spacetime Primitives
- 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
- Tensor Products of Modules
- Tensors And Observers
- The De Rham Complex Homotopy and Mayer Vietoris
- The de Rham Theorem and Degree
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Exterior Derivative and Cartan Calculus
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Logarithm and General Powers
- 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 ℝ
- Vector Fields Flows and Lie Derivatives
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Volumes of Elementary Solids and Solids of Revolution
2 · Summary
The example chooses a finite cavity wall point as the reference for a future timelike Killing field. Rescaling the generator sets the reference lapse to one and divides the finite Killing charge, normalized temperature, and particle Killing energy by the same factor. The local proper-temperature and proper-energy ratios remain fixed by algebra; no asymptotic flatness or global equilibrium assumption is needed.
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Reference-wall normalization preserves proper thermal and particle ratios
Example
Use the static subcase, finite coordinate slab, and open chart domain of Finite Killing energy current and reference normalization. Adopt that lemma's SI convention: , the spatial coordinates are in metres, has units , and the metric components and length-normalized Killing field are dimensionless. Let be future timelike and orthogonal to the coordinate slices, and put and for . Let be a specified smooth embedded codimension-one submanifold whose induced metric has signature (a timelike cavity wall), and choose a reference event in the static region. Put , which is dimensionless in this convention. No asymptotically flat end is assumed. Supply a function assigned units kelvins and interpreted as the local proper temperature measured by observer field , and a covector field on whose components have units . When a particle-energy interpretation is used, supply a vector field on that is future-directed and causal and satisfies at each ; its components then have the same units as because the metric is dimensionless. Define, pointwise on , and . Rescale the generator by . The reference lapse is then , while the normalized temperature and particle-energy ratios at every are unchanged: For each slice charge defined in Finite Killing energy current and reference normalization, . This choice is meaningful in a finite cavity without an asymptotic normalization; it does not make spatially constant or assert that distinct reference-wall choices produce equal local temperatures.
Facts & Assumptions
Given: The exact finite static-slice current and rescaling clauses of Finite Killing energy current and reference normalization, its finite rectangular slab convention, a positive reference lapse at , and supplied fields and with the units and causal-momentum condition stated above.
Assume , the Axiom of Countable Choice, as required by the connection construction and recorded in The Axiom of Countable Choice ().
In its static subcase, Finite Killing energy current and reference normalization derives , , and for every dimensionless ; it defines the mechanical pairing . Its finite charge uses the open spatial rectangle with compact closure specified by MI01.
The SI reading of Finite Killing energy current and reference normalization takes with in , spatial coordinates in metres, dimensionless metric components, and normalized so that its flow parameter has units of length. Thus and are dimensionless, and the pairing factor in has units .
Finite spacelike slab and normal flux charge defines a positively oriented product slab with open spatial rectangle and compact closure with spacelike slices, future unit normal, and proper spatial volume . It assigns no physical units to its mathematical coordinates; this example's SI length convention is additional data.
is a specified smooth timelike embedded hypersurface, is the selected event in the static region, and . The supplied fields are and with the units in the Statement. For the particle-energy interpretation, is a future-directed causal vector field on and for every .
Verification
Since with , its norm satisfies , and . The normalized field is unchanged.
The temperature definition gives ; the mechanical pairing gives ; and [F1] gives the same scaling for the finite Killing charge. Dividing by proves both displayed ratio identities and the charge statement.
The right sides of the ratio identities are the supplied and the contraction . Neither definition imposes spatial constancy, so the normalization calculation proves neither thermal equilibrium nor equality between distinct wall choices.