Mathematics Differential Geometry From Rs Rs Spacetime Dim Lorentzian

The spacetime dimension

Spacetime in modern physics is a four-dimensional continuum: three of space and one of time. This is the setting of Einstein's theories, where events are located by four coordinates and the geometry of this continuum is described by a pseudo-Riemannian metric, a rule for measuring intervals that treats time differently from space. The number four is so familiar that it is easy to forget it is an assumption built into the standard equations.

Recognition Science (RS) is a framework that attempts to derive physical structure from a single starting point: reality keeps a ledger, a discrete record of recognition events, and the cost of recognition is forced, not chosen. Within this framework, the spatial dimension is not assumed but derived. The framework's machine-checked library of formal theorems establishes that the recognition manifold, the smooth space of possible recognition states, has dimension 3. From this, the framework defines spacetime dimension as the spatial dimension plus one, and its library proves the resulting number is 4.

The specific declaration rsSpacetimeDim_lorentzian is a theorem in this library. It states that the RS spacetime dimension equals 4, and it does so by referencing the earlier proof that the spatial dimension is 3. The name "lorentzian" signals the intended interpretation: a 3+1 dimensional spacetime with a pseudo-Riemannian metric, the signature used in general relativity. The theorem itself, however, only establishes the dimension count. It does not construct the metric, derive the Einstein field equations, or prove that the resulting geometry is Lorentzian in the full physical sense.

In Recognition Science, the framework models five canonical differential geometric structures: smooth manifold, Riemannian, pseudo-Riemannian, Kähler, and symplectic. The count of these structures is also proved to be 5 in the library. The framework's claim is that the recognition manifold is a smooth 3-manifold, and that the natural spacetime setting is the pseudo-Riemannian one, giving 4 dimensions. This is a derivation within the framework, not an independent measurement of the universe's dimension.

What the declaration does not claim is important. It does not prove that the universe is four-dimensional in the sense of an empirical measurement; it derives this number from the framework's axioms and definitions. It does not establish the signature of the metric (the distinction between time and space coordinates) beyond the naming convention. And it does not connect this dimension count to any physical prediction that could be tested against observation. The theorem is a formal result about the framework's own definitions, a step in a larger chain of derivations, not a standalone statement about the cosmos.

def rsDimension : ℕ := 3

theorem rsSpacetimeDim_lorentzian : rsSpacetimeDim = 4 := rsSpacetimeDim_eq_4

inductive DiffGeoStructure where
  | smoothManifold | riemannian | pseudoRiemannian | kahler | symplectic
  deriving DecidableEq, Repr, BEq, Fintype

theorem diffGeoStructureCount : Fintype.card DiffGeoStructure = 5 := by decide

What this page does not claim

The theorem does not prove that the universe is four-dimensional as an empirical fact. It does not derive the metric signature or the Einstein field equations. It does not connect the dimension count to any testable physical prediction.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/DifferentialGeometryFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: