def
definition
actualization_status
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Modal.Actualization on GitHub at line 400.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
397/-! ## Summary -/
398
399/-- Status report for Actualization module. -/
400def actualization_status : String :=
401 "╔══════════════════════════════════════════════════════════════╗\n" ++
402 "║ ACTUALIZATION: SELECTION FROM POSSIBILITIES ║\n" ++
403 "╠══════════════════════════════════════════════════════════════╣\n" ++
404 "║ CORE CONCEPTS: ║\n" ++
405 "║ • A = Actualization operator (argmin J) ║\n" ++
406 "║ • Degeneracy = multiple cost-equivalent successors ║\n" ++
407 "║ • Contingency = could have been otherwise ║\n" ++
408 "║ • PathAction = total J-cost along trajectory ║\n" ++
409 "╠══════════════════════════════════════════════════════════════╣\n" ++
410 "║ KEY THEOREMS: ║\n" ++
411 "║ • every_config_actualizes: A is total ║\n" ++
412 "║ • A_toward_identity: A drives to J=0 ║\n" ++
413 "║ • collapse_automatic: C≥1 forces selection ║\n" ++
414 "║ • possibility_actualization_adjoint: P ⊣ A ║\n" ++
415 "╠══════════════════════════════════════════════════════════════╣\n" ++
416 "║ BORN RULE: ║\n" ++
417 "║ • P[γ] ∝ exp(-C[γ]) emerges from cost structure ║\n" ++
418 "║ • Not postulated, but derived ║\n" ++
419 "╚══════════════════════════════════════════════════════════════╝"
420
421#check actualization_status
422
423end
424
425end IndisputableMonolith.Modal