def
definition
possibility_status
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Modal.Possibility on GitHub at line 416.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
413/-! ## Summary and Status -/
414
415/-- Status report for Grammar of Possibility formalization. -/
416def possibility_status : String :=
417 "╔══════════════════════════════════════════════════════════════╗\n" ++
418 "║ GRAMMAR OF POSSIBILITY / RS MODAL LOGIC ║\n" ++
419 "╠══════════════════════════════════════════════════════════════╣\n" ++
420 "║ CORE CONCEPTS: ║\n" ++
421 "║ • Possibility P(c) = finite-cost reachable configs ║\n" ++
422 "║ • Actualization A = J-minimizing selection ║\n" ++
423 "║ • J_stasis = cost of staying the same ║\n" ++
424 "║ • J_change = cost of transition ║\n" ++
425 "╠══════════════════════════════════════════════════════════════╣\n" ++
426 "║ MODAL OPERATORS: ║\n" ++
427 "║ • □p (Necessary) = holds in all possible futures ║\n" ++
428 "║ • ◇p (Possible) = holds in some possible future ║\n" ++
429 "║ • Duality: □p ⟺ ¬◇¬p ║\n" ++
430 "╠══════════════════════════════════════════════════════════════╣\n" ++
431 "║ KEY THEOREMS: ║\n" ++
432 "║ • identity_prefers_stasis: x=1 is unique fixed point ║\n" ++
433 "║ • identity_always_possible: 1 ∈ P(c) for all c ║\n" ++
434 "║ • actualize_decreases_cost: A drives toward identity ║\n" ++
435 "║ • why_anything_happens: stasis costs more for x ≠ 1 ║\n" ++
436 "╠══════════════════════════════════════════════════════════════╣\n" ++
437 "║ STATUS: FOUNDATION COMPLETE ║\n" ++
438 "╚══════════════════════════════════════════════════════════════╝"
439
440#check possibility_status
441
442end IndisputableMonolith.Modal