theorem
proved
possibility_actualization_adjoint
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 392.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
389def possibility_actualization_adjoint_hypothesis (p : ConfigProp) (c : Config) : Prop :=
390 (◇p) c ↔ p (A c)
391
392theorem possibility_actualization_adjoint (p : ConfigProp) (c : Config)
393 (h : possibility_actualization_adjoint_hypothesis p c) :
394 (◇p) c ↔ p (A c) :=
395 h
396
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