theorem
proved
boundary_unreachable
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Modal.ModalGeometry on GitHub at line 266.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
263def PossibilityBoundary : Set ℝ := {x : ℝ | x = 0}
264
265/-- The boundary is unreachable at finite cost. -/
266theorem boundary_unreachable :
267 ∀ c : Config, c.value ≠ 0 := by
268 intro c
269 exact ne_of_gt c.pos
270
271/-! ## Summary -/
272
273/-- Status report for Modal Geometry module. -/
274def modal_geometry_status : String :=
275 "╔══════════════════════════════════════════════════════════════╗\n" ++
276 "║ MODAL GEOMETRY: SHAPE OF POSSIBILITY SPACE ║\n" ++
277 "╠══════════════════════════════════════════════════════════════╣\n" ++
278 "║ TOPOLOGY: ║\n" ++
279 "║ • Star topology: all configs connect to identity ║\n" ++
280 "║ • Dimension = 2 (value + time) ║\n" ++
281 "║ • Boundary at x → 0 (J → ∞) ║\n" ++
282 "╠══════════════════════════════════════════════════════════════╣\n" ++
283 "║ METRIC STRUCTURE: ║\n" ++
284 "║ • d(x,y) = J_transition(x,y) ║\n" ++
285 "║ • Curvature κ(c) = 1/c² + 1/c⁴ ║\n" ++
286 "║ • κ(1) = 2 (curvature at identity) ║\n" ++
287 "╠══════════════════════════════════════════════════════════════╣\n" ++
288 "║ MODAL NYQUIST: ║\n" ++
289 "║ • 8-tick period limits modal resolution ║\n" ++
290 "║ • Finest distinction = 1 tick ║\n" ++
291 "║ • Modal bandwidth = 4 per octave ║\n" ++
292 "╠══════════════════════════════════════════════════════════════╣\n" ++
293 "║ INTERFERENCE: ║\n" ++
294 "║ • Paths with similar cost can interfere ║\n" ++
295 "║ • Constructive when in phase ║\n" ++
296 "║ • Destructive when out of phase ║\n" ++