def
definition
dimension_status
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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