No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
71theorem spacetime_dim_eq_four : spacetime_dim = 4 := by
proof body
Term-mode proof.
72 unfold spacetime_dim temporal_dim spatial_dim D_physical; rfl
73
74/-- The 8-tick period matches 2^D for D = 3. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
Lean names referenced from this declaration's body.
-
period
in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
D_physical
in IndisputableMonolith.Foundation.DimensionForcing
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
spacetime_dim
in IndisputableMonolith.Gravity.Connection
decl_use
-
spacetime_dim
in IndisputableMonolith.Unification.SpacetimeEmergence
decl_use
-
spatial_dim
in IndisputableMonolith.Unification.SpacetimeEmergence
decl_use
-
temporal_dim
in IndisputableMonolith.Unification.SpacetimeEmergence
decl_use