PAPER → PROOF → CODE
Stack Theory (Bennett 2026)
Lean 4 formalization of hard combinatorial bounds on what multi-layer delegation can achieve, with bridge theorems connecting weakness ordering to Heyting nucleus fixed-point 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
36
Theorems
38
Definitions
861
Lines
15
Modules
0
sorry
2
Bridge (novel)
Paper ↔ Proof Correspondence
| PAPER | RESULT | LEAN NAME | STATUS |
|---|---|---|---|
| ESM §9.1 | Lemma 1: |Lv| ≤ 2^|v| | language_card_le_pow | PROVED |
| ESM §9.2 | Lemma 2: Ext(π) ⊆ Lv | ext_subset_language | PROVED |
| ESM §9.3 | Lemma 3: ε(γ)+|O| ≤ |Lv| | utility_le_language | PROVED |
| ESM §9.4 | Lemma 4: |f(v,π)| ≤ |Ext(π)| | abstractor_card_le_ext | PROVED |
| §5 | Theorem 5.1: Law of the Stack | law_of_the_stack | PROVED |
| ESM §9.5 | W-maxing = FE minimization | wmaxing_eq_fe_min | PROVED |
| ESM §9.5 | Dyadic exactness refinement | wmaxing_eq_fe_min_of_power_of_two | PROVED |
| §5 Cor. | Delegation bottleneck | delegation_bottleneck_fe | PROVED |
| §6 Prop 6.1 | Splintering under over-constraint | overconstraint_implies_splintering | PROVED |
| §6 Prop 6.1 | Splinter construction | overconstraint_yields_splinter | PROVED |
| Bridge infra | Weakness monotone on Ω_R | weakness_monotone_on_fixed_points | PROVED |
| Bridge infra | Fixed-policy contravariance | fixedPolicyEncoding_contravariant | PROVED |
| Bridge infra | Weakness on fixed policies | weakness_monotone_on_fixed_policies | PROVED |
| Novel | Collective ↔ nontrivial meet | collective_identity_yields_nontrivial_meet_in_fixed_locus | PROVED |
| Bridge infra | Stable policy inf-closure | stable_policy_closed_inf | PROVED |
| Novel | Abstractor through nucleus | abstractorThroughNucleus_eq_abstractor_of_fixed | PROVED |
Key Mathematics
Law of the Stack (Theorem 5.1)
Adaptability at layer i+1 bounded by extension cardinality
W-maxing = FE Minimization
Ordering by viability width ↔ ordering by counting free energy
Cancer-Analogue Splintering (Prop 6.1)
Over-constraint causes loss of collective policy
Collective ↔ Nontrivial Meet (Novel)
Collective identity equivalent to nontrivial meet in Heyting Ω_R
Formalization Discoveries
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 — log_two_order_exact_on_powers_of_two. This tightness result is not in the original paper.
Hostile Audit Remediation
Internal adversarial audit (using automated J-Group probes, not independent external review) identified 5 minimal-passing patterns (ceremony theorems whose proofs were tautological). Post-remediation: all application theorems do genuine domain reasoning.
Lean 4 Modules
“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.