Based on: "Closing the Loop"
This formalization is a machine-checked verification of the theoretical framework presented in:
"Closing the Loop: How Semantic Closure Enables Open-Ended Evolution"
Amahury J. Lopez-Diaz and Carlos Gershenson
School of Systems Science and Industrial Engineering, Binghamton University
Journal of the Royal Society Interface, 2025 (arXiv:2404.04374)
Click to expand
Semantic Closure Theory
Lopez-Diaz and Gershenson's work explores how semantic closure—the self-referential mechanism through which symbols actively construct and interpret their own functional contexts—emerges in evolutionary systems. By integrating concepts from relational biology, physical biosemiotics, and ecological psychology, they develop a unified computational enactivist framework.
The paper extends Hofmeyr's (Fabrication, Assembly)-systems—a continuation of Rosen's (Metabolism, Repair)-systems—with temporal parametrization, capturing critical properties of life including autopoiesis, anticipation, and adaptation.
Central to the theory is the closure operator: a mathematical structure where self-reference stabilizes into fixed points, enabling meaning to emerge from pure syntax.
Visualization of the proof dependency lattice. Each node represents a verified theorem, with edges showing logical dependencies in the formalization.
Machine-Verified Implementation
This Lean 4 formalization provides machine-checked proofs of the core mathematical structures from the original paper. Every equation and theorem has been formally verified, ensuring the theoretical framework is logically sound and computationally realizable.
All equations from the paper formally verified
Proofs compile to C via Lambda IR
Computation + Dynamics unified
| PAPER EQ. | CONTENT | LEAN THEOREM |
|---|---|---|
| 2.1 | A -> B -> H(A,B) | Metabolism, Selector |
| 2.3 | Injectivity condition | InjectiveEvalAt |
| 2.4 | Beta inverse | RightInverseAt, EvalImage.betaOnImage |
| 2.5 | Closure loop idempotence | closeSelector.idem |
| S(G) | Admissibility restriction | Admissible subtype |
Executable Code Generation
Proofs compile to C code via Lambda IR, enabling simulation and embedding in larger models (Python, Julia, MATLAB).
Honest Assumptions
Explicitly distinguishes weak (injectivity), medium (choice-free), and strong (classical choice) proof versions.
Eigencomputable Extension
Optional "Noneism" layer grounds nonconstructive choices in stabilizing dynamics rather than pure axioms.
Two-Track Architecture
Unifies computation (Lambda IR to C pipeline) with dynamics (ReachSystem, Nucleus framework) through relational realizability.