Mathematics Differential Geometry From Rs Diff Geo Structure

The five structures

Differential geometry is the branch of mathematics that studies smooth shapes and the ways to measure distances and angles on them. A smooth manifold is the basic object: a space that locally resembles ordinary Euclidean space, so that calculus can be done on it. A Riemannian manifold adds a positive-definite metric, giving a notion of distance. A pseudo-Riemannian manifold relaxes that to allow metrics with mixed signatures, which is the setting for general relativity. A Kähler manifold combines a complex structure with a Riemannian metric, and a symplectic manifold provides a structure used in Hamiltonian mechanics.

The Recognition Science framework, a research program that derives physical and mathematical structure from a discrete record of events called a ledger, encodes these five classical structures in a machine-checked library of formal theorems. Its declaration DiffGeoStructure is an inductive type listing exactly five cases: smoothManifold, riemannian, pseudoRiemannian, kahler, and symplectic. A theorem in the same file proves that the number of these structures is five. The framework also defines a recognition dimension of 3 and a spacetime dimension as that plus one, with a theorem proving that the result equals 4, and labels this the Lorentzian spacetime dimension.

What the declaration establishes is a formal counting and a dimensional claim. It proves that the list has five entries and that 3 plus 1 equals 4. It does not prove that these five structures exhaust all of differential geometry, nor that the recognition manifold itself is a Kähler or symplectic space. The declaration does not claim that the metric on the recognition manifold is uniquely determined, nor that the framework derives the Einstein field equations. It also does not claim that the recognition dimension of 3 is forced by the framework's own theorems; the value 3 is a definitional choice, not a derived result.

The value of this declaration is organizational. It gives a compact, machine-checked vocabulary for saying which classical geometric structures the framework intends to discuss, and it fixes the dimensional relationship between the recognition space and spacetime. A reader can now ask which of these five structures the recognition metric actually instantiates, and whether the framework's theorems force that choice. Those questions remain open targets, not settled facts.

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

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

theorem rsSpacetimeDim_eq_4 : rsSpacetimeDim = 4 := by decide

What this page does not claim

The declaration does not prove that the five listed structures exhaust all of differential geometry. The declaration does not claim that the recognition manifold is Kähler or symplectic. The recognition dimension of 3 is a definitional choice, not a theorem of the framework.

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: