Stack Theory (Bennett 2026)
Formally verified delegation bounds for multi-layer intelligence architectures, with novel bridge theorems connecting weakness ordering to Heyting nucleus algebras.
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Stack Theory (Bennett 2026) • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Are there hard mathematical limits on what a multi-layer delegation architecture can achieve? If so, what do those limits look like — and what goes wrong when you try to push past them?
Bennett answers yes: the Law of the Stack imposes an exponential ceiling (2|Ext(πᵢ)|) on each layer's adaptability, and over-constraining the system to exceed this bound causes structural fragmentation (splintering). We machine-checked these claims and discovered a novel algebraic characterization: Bennett's sociological concept of “collective identity” is equivalent to a nontrivial meet in the Heyting fixed-point algebra.
Context & Discovery
Dyadic Exactness Refinement
Bennett's Corollary 5.1 uses Nat.log which introduces discretization. We proved that on dyadic continuation counts (powers of 2), the discrete ordering is exact. This tightness result is not in the original paper.
Bridge Theorems (2 Novel + 4 Infrastructure)
We connected Bennett's combinatorial framework to HeytingLean's nucleus operator infrastructure. The central new result: collective identity is equivalent to nontrivial meet in the Heyting fixed-point algebra Ω_R. Four supporting infrastructure lemmas (one-line, definitional) complete the bridge.
Hostile Audit Remediation
Internal adversarial audit (automated J-Group probes) identified 5 minimal-passing patterns. All remediated with genuine domain reasoning.
Formal–Empirical Boundary
Formally Proved
- • Delegation bounds (Law of the Stack, Theorem 5.1)
- • Free energy equivalence (Corollary 5.1)
- • Cancer-analogue splintering (Proposition 6.1)
- • Bridge: collective ↔ nontrivial meet in Ω_R
- • Dyadic exactness refinement
Engineering / Application
- • AgentHALO: toy 2-layer model demonstrating bounds apply
- • Mapping to real container-agent architectures
- • RLHF splintering interpretation (empirical analogy)
Implementation Phases
Primitives
Programs, vocabularies, truth sets, language, extensions, weakness, tasks, utility. ESM Lemmas 1–3.
Stack Architecture
Abstractors (ESM Lemma 4), multi-layer architecture, Law of the Stack (Theorem 5.1).
Free Energy + Exactness
Viability weakness, free energy, w-maxing = FE min, dyadic exactness, delegation bottleneck.
Collective Identity + Splintering
Collective policies, boundary conditions, over-constraint, cancer-analogue splintering (Prop 6.1).
Bridge Theorems
2 novel bridge theorems + 4 infrastructure lemmas connecting Bennett to Core.Nucleus: collective ↔ Ω_R meet (novel), abstractor through nucleus (novel), plus definitional monotonicity/closure lemmas.
Applications + Audit
AgentHALO concrete stack, weak boundary design, hostile audit with J-Group probes, remediation.
Links
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
MENTAT Contribution Certificates
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerIntelligence as Delegation-Bounded Multi-Layer Architecture
Contributor
Matthew T. Bennett
Australian National University (paper in press, Phil. Trans. B)
Core insight that biological and artificial intelligence can be modeled as multi-layer delegation architectures where each layer's adaptability faces hard combinatorial ceilings. The question 'Are biological systems more intelligent than AI?' is reframed as a question about which architectures can navigate these bounds more effectively.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerStack Theory: Programs, Vocabularies, Extensions, Weakness, and Stacks
Contributor
Matthew T. Bennett
Australian National University (paper in press, Phil. Trans. B)
Complete mathematical framework: programs as finite state sets, vocabularies, truth sets with distributive properties, language as powerset filter, extensions as policy completions, weakness as extension cardinality, multi-layer architecture with abstractor-mediated vocabulary chains, collective identity, boundary conditions, and the splintering failure mode under over-constraint.
Builds Upon
MENTAT Contribution Record
APPLICATION
Applied Contribution
CONTRIBUTION LEVEL: APPLICATION
Ontological EngineerApplication to Biological vs Artificial Intelligence Comparison
Contributor
Matthew T. Bennett
Australian National University (paper in press, Phil. Trans. B)
Applied contribution: concrete delegation bounds for agent architectures, free energy formulation as an equivalent ordering principle, the cancer-analogue where over-constraining a collective causes structural fragmentation (splintering). Analogous to AI alignment failure modes: specification gaming and reward hacking as potential instances of over-constraint (empirical connection unproved).
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization: 15 Modules, 36 Theorems, 2 Novel Bridge Theorems + 4 Infrastructure Lemmas
Contributor
Apoth3osis Labs
Apoth3osis
Lean 4 formalization of Bennett's Stack Theory across 15 source modules with 861 lines and zero sorry gaps. The 4-lemma ESM chain (Lemmas 1–4), Law of the Stack (Theorem 5.1), w-maxing = FE minimization (Corollary 5.1), cancer-analogue splintering (Proposition 6.1), plus 2 novel bridge theorems and 4 infrastructure lemmas connecting Bennett's framework to Heyting algebra nucleus theory. Crown jewel: collective identity in Bennett's sense is equivalent to nontrivial meet in the fixed-point algebra Ω_R.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerKernel Verification + Hostile Audit + Transpilations
Contributor
Apoth3osis Labs
Apoth3osis
Kernel-level verification by the Lean 4 type checker. Internal hostile audit (automated J-Group probes, not independent external review) identifying and remediating 5 minimal-passing patterns (ceremony theorems). Verified C transpilation (7 files, gcc -std=c11 -Wall -Wextra -Werror clean). Safe Rust transpilation (no unsafe, 9 tests passing). IPFS-pinned archives with SHA-256 content hashes.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerProduction Integration: HeytingLean Core.Nucleus Bridge + PPC Page
Contributor
Apoth3osis Labs
Apoth3osis
Bridge-level contribution: integration with HeytingLean's Core.Nucleus operator infrastructure. The bridge theorems connect Bennett's combinatorial framework to the Heyting fixed-point algebra, enabling future connections to CNCC circuit-level nucleus structure. PPC page with AccordionModules, KaTeX rendering, and downloadable artifacts. Research project page with MENTAT certificates.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026