def
definition
dimension_status
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogGeom.Dimension on GitHub at line 151.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
148
149/-! ## Module Status -/
150
151def dimension_status : String :=
152 "╔════════════════════════════════════════════════════════════════╗\n" ++
153 "║ RECOGNITION DIMENSION THEORY ║\n" ++
154 "╠════════════════════════════════════════════════════════════════╣\n" ++
155 "║ ║\n" ++
156 "║ DEFINITIONS ║\n" ++
157 "║ ✓ IsSeparating: recognizer distinguishes all configs ║\n" ++
158 "║ ✓ PairSeparates: two recognizers together separate ║\n" ++
159 "║ ✓ IndependentRecognizers: non-redundant information ║\n" ++
160 "║ ║\n" ++
161 "║ THEOREMS ║\n" ++
162 "║ ✓ isSeparating_iff: characterization ║\n" ++
163 "║ ✓ separating_quotient_bijective: quotient ≅ C ║\n" ++
164 "║ ✓ separating_singleton_cells: cells are singletons ║\n" ++
165 "║ ✓ pairSeparates_iff: characterization ║\n" ++
166 "║ ✓ independent_strict_refines: composition strictly refines ║\n" ++
167 "║ ║\n" ++
168 "║ PHYSICAL INTERPRETATION ║\n" ++
169 "║ Spacetime dimension = 4 independent coordinate recognizers ║\n" ++
170 "║ Quantum dimension = independent observable count ║\n" ++
171 "║ Recognition dimension explains geometric dimension ║\n" ++
172 "║ ║\n" ++
173 "╚════════════════════════════════════════════════════════════════╝\n"
174
175#eval dimension_status
176
177end RecogGeom
178end IndisputableMonolith