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.