Pairwise Independence of Representation, Classification, and Composition in Finite Extensional Magmas

TL;DR

This paper investigates the independence of key properties in finite extensional magmas, proving their pairwise independence and establishing minimal sizes for counterexamples with formal verification.

Contribution

It identifies three independent properties in finite extensional magmas and provides minimal counterexamples, formalized in Lean 4, to clarify their relationships.

Findings

Three properties (R, D, H) are pairwise independent.

Minimal counterexamples have size N=5, which is proven optimal.

The internal composition property is equivalent to standard axioms.

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.