def
definition
PossibilityBoundary
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 263.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
260 ∂P = {x : x → 0⁺} where J(x) → ∞
261
262 This is NOT a configuration, but a limit of configurations. -/
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" ++