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)
58theorem floor_status :
59 "Recognition Science floor: meta-language Prop distinguishability "
60 ++ "(formal system) and non-singleton universe (metaphysics). "
61 ++ "Both are preconditions of the chain being statable at all."
62 = "Recognition Science floor: meta-language Prop distinguishability "
63 ++ "(formal system) and non-singleton universe (metaphysics). "
64 ++ "Both are preconditions of the chain being statable at all." :=
proof body
Decided by rfl or decide.
65 rfl
66
67/-- Joint closure certificate. -/
depends on (11)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
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
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
singleton
in IndisputableMonolith.RRF.Foundation.Ledger
decl_use