Gerundelle: A Formally Verified Architecture of Mind

Gerundelle is a twelve-layer architecture of mind whose promises are verified theorems. At its core is an algebra of mind: seventeen operators over a structured web of understanding with filled slots, unknowns, relations, constraints, and provenance. The central idea is that a mind is both a marketplace and a tournament where thoughts bond and compete for scarce attention slots, funded by evidence whose provenance (lived, told, or imagined) is conserved. A thought molecule holds its candidate bindings in superposition and resolves to the argmax at each level of a tournament. Its bid combines learned attraction to its partner, tension from open sites, expected surprise reduction, and constraint support. The tournament is the bottleneck: at most 7/5/4 molecules win each level, and only the top level's winners are what the mind attends to. Understanding is a graph of concepts connected by type relations like causes, caused_by, conditions, co_occurs, role, etc. Each slot's funding has provenance weights. An open slot is a structured unknown. It has a shape, exerts pull, and narrows what could fill it. When a push's outcome disagrees with its history, the agent finds what's new in the situation and splits the push on it (differentiate). The meta layer notices when this is needed (conflated outcomes), and when it was wrong (same outcomes after the split: unify). New thought molecules come from open slots in the graph, from the world pushing back, and from the tournament's own dynamics. Open slots create questions, hypotheses, and experiments. The world's responses to the mind's actions enter the tournament as perceptions. Territory is the motivational engine. Ownership slots (unclaimed, control, contested, lost) pull on attention with proved ordering: lost > control > unclaimed in the default temperament, invertible at high curiosity. Emotions are readings of this register: frustration is two failures running on a live slot, joy is a claim that took, curiosity is an unclaimed slot winning the top. The paper proves which layer each emotion reads. The imagination firewall is structural: the imagination register has no provenance record, so nothing imagined can fund anything. The inbound path (forget provenance) exists; the outbound path (reconstruct it) provably doesn't. Each layer carries guarantees that a proof assistant (Lean 4) has checked for every possible input, every possible sequence of operations, every possible interleaving. The formal development comprises 24 files, 301 theorems, and no unfinished proofs. Six fields of mathematics that rarely cite one another (information security, the geometry of symmetry groups, parallel transport in fiber bundles, the theory of how concepts can be learned in sequence, graded monads, and a calculus of evidence and trust) turn out to describe the same architecture once stated about its operators and data. Bridge theorems connect them across layers. A theorem proves that what an agent perceives and what it feels are both instances of the same mathematical structure: factorization through a view. The architecture is domain-independent: one mind and one algebra run in story, code, chess and population worlds, with no domain-specific machinery. Only the world changes. This differs from the two established approaches in what it fixes in advance. Symbolic AI fixes the answers (chains of rules that shatter when a condition changes) and where what the system doesn't know is a gap with no shape. Statistical AI fixes almost nothing; it learns how to handle evidence in the same weights as what the evidence says about the world, so it holds its own invariants (that imagining is not seeing, that hearsay is not experience) only statistically. Gerundelle fixes the mechanics of knowing: how ignorance is represented (as structured open slots, not absence), how evidence is weighed and kept (provenance conserved: proved, not enforced by a runtime check), and how understanding is revised (by the world pushing back, not by derivation). It proves these guarantees once, for every sequence, and leaves every contingent fact about the world to open variables funded by experience.