pith. machine review for the scientific record. sign in
def definition def or abbrev

actualization_status

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 400def actualization_status : String :=

proof body

Definition body.

 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

depends on (20)

Lean names referenced from this declaration's body.