def
definition
possibility_actualization_adjoint_hypothesis
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Modal.Actualization on GitHub at line 389.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
386 **STATUS**: HYPOTHESIS - In the full theory, this is restricted to properties
387 that are cost-monotonic. Here we state it as a hypothesis to characterize the
388 relationship between the modal operators. -/
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 "╚══════════════════════════════════════════════════════════════╝"