def definition def or abbrev

`Spacetime`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  47def Spacetime : Manifold := { dim := 4 }

Definition body.

  48
  49/-- Coordinate indices for spacetime. -/

From the project-wide theorem graph. These declarations reference this one in their body.

RealityCertificate in IndisputableMonolith.Foundation.RealityFromDistinction decl_use
comparisonTable in IndisputableMonolith.QFT.UVCutoff decl_use
cutoff_above_lhc in IndisputableMonolith.QFT.UVCutoff decl_use
UVCutoffFalsifier in IndisputableMonolith.QFT.UVCutoff decl_use
implications in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
IsSmoothRecognitionGeometry in IndisputableMonolith.RecogGeom.Charts decl_use
dimension_status in IndisputableMonolith.RecogGeom.Dimension decl_use
independent_strict_refines in IndisputableMonolith.RecogGeom.Dimension decl_use
latticeSpacing_tendsto_zero in IndisputableMonolith.Relativity.Geometry.DiscreteBridge decl_use
lorentzian_from_det in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
mass_gap_bounds in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
signature_unique in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spacetime_dim in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
SpacetimeEmergenceCert in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spacetime_emergence_cert_nonempty in IndisputableMonolith.Unification.SpacetimeEmergence decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
dim in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
Manifold in IndisputableMonolith.Relativity.Geometry.Manifold decl_use