Pairwise Independence of Representation, Classification, and Composition in Finite Extensional Magmas
Stefano Palmieri
cs.LO
Mar 27, 2026 · v1
TL;DR
Formalizes pairwise-independence results for finite extensional magmas in Lean 4 with verified finite counterexamples, zero sorry.
Abstract
Nontrivial combinatory algebras with S and K must be infinite. Associativity is incompatible with combining a classifier and a retraction pair in a finite extensional magma. These obstructions exclude several standard settings from the finite extensional framework studied here, most notably nontrivial finite S+K-style combinatory algebras and associative structures (semigroups, monoids, groups, rings) carrying both a classifier and a retraction pair. What algebraic structure exists in the remaining landscape: finite, non-associative, total? We identify three properties of finite extensional 2-pointed magmas: self-representation (R), the classifier dichotomy (D), and the Internal Composition Property (H). We prove they are pairwise independent. Lean-verified finite counterexamples at sizes 4 through 10 establish all six non-implications, four with provably tight bounds. The minimum coexistence witness has N = 5, which is optimal: ICP requires 3 pairwise distinct core elements, so N \ge 5. The three-category decomposition induced by D is an isomorphism invariant, and the ICP is logically equivalent to the standard Compose+Inert axioms. All results are formalized in Lean 4 with zero sorry.
Problem
In finite extensional 2-pointed magmas, the algebraic independence of self-representation (R), classifier dichotomy (D), and internal composition property (H) was unknown. Standard settings like finite combinatory algebras and associative structures are excluded by known obstructions.
Approach
The authors prove pairwise independence of R, D, and H by constructing Lean-verified finite counterexamples at sizes 4 through 10 that establish all six non-implications. Universal theorems are proved by pure algebraic reasoning (no decide) and formalized in Lean 4. The three-category decomposition induced by D is shown to be an isomorphism invariant.
Results
All six non-implications are established with four having provably tight bounds. The minimum coexistence witness (a magma satisfying all three properties) has N=5, which is optimal since ICP requires 3 pairwise distinct core elements so N >= 5. All results are formalized in Lean 4 with zero sorry.
