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)
50theorem count_eq : crossDomainModuleCount = 27 := rfl
proof body
Term-mode proof.
51
52/-- 27 = 3³ (cube of D_spatial). Coincidence? -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.
-
cert
in IndisputableMonolith.Archaeology.UrbanDensityFromPhiLadder
decl_use
-
UrbanDensityCert
in IndisputableMonolith.Archaeology.UrbanDensityFromPhiLadder
decl_use
-
metaTheoremCountCert
in IndisputableMonolith.CrossDomain.MetaTheoremCount
decl_use
-
cert
in IndisputableMonolith.Meteorology.HurricaneCategoryFromPhiLadder
decl_use
-
HurricaneCategoryCert
in IndisputableMonolith.Meteorology.HurricaneCategoryFromPhiLadder
decl_use
depends on (6)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
crossDomainModuleCount
in IndisputableMonolith.CrossDomain.MetaTheoremCount
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use