Boundary: A Four-Agent Interaction-Style Rewriting Kernel with a Lean 4 Reference Semantics Rich

Abstract

We present Boundary (∂ ), a small interaction-style graph-rewriting language built from exactly four agent kinds and ve reduction rules. The kernel inherits the structural discipline of Lafont's interaction combinators (principal-port active pairs, one rule per unordered agent pair, local rewrites) while introducing generation-bearing endpoint identity, a total dispatch table over all ten unordered active-pair combinations, and a locality- rst staged parallelism model. We deliver a Lean 4 reference semantics (707 lines of kernel code, zero sorry) in which dispatch determinism, mode preservation, and interface-arity laws are proved, together with a detailed speci cation for a Rust executable runtime connected to the reference by dierential testing against a canonically deterministic reference mode. The intended denotational reading of the four agents is bi-Heyting (negation, conjunction, coHeyting subtraction, nucleus/boundary veri cation). The bi-Heyting algebraic substrate for this reading is largely complete: ve boundary-operator properties are proved via Mathlib, the nucleus/re-entry theorem is proved, and the NOTW term algebra on an ICC carrier with a non-trivial three-element witness is proved. The bridging theorem connecting the operational kernel to this substrate is an explicitly tracked conjecture, currently blocked after two compatible-closure semantics were formally refuted by machine-checked counterexamples. We describe a methodological discipline of eight named anti-hack gates that prevent common failure modes in interaction-net implementations, and we argue that this discipline, together with the Lean/Rust dierential bridge, constitutes a reusable methodology for proof-assistant- rst interaction-net design. Published by The Institute for Applied Ontological Mathematics.