有限扩展型代数结构中表示、分类与组合的两两独立性

具有S和K的非平凡组合子代数必须是无限的。在有限扩展型代数中，将分类器与撤回器配对与可交换性相冲突。这些障碍排除了许多标准设置从有限扩展框架中，最显著的是非平凡的有限S+K风格组合子代数以及携带分类器和撤回器配对的可交换结构（半群、单子、群、环）。剩下的代数结构是什么样的：有限的、非可交换的、全的？我们识别了三种有限扩展型2点指示代数结构的性质：自表示(R)、分类器二分法(D)和内部组合属性(H)。我们证明它们两两独立。大小为4至10的Lean验证有限反例确立了所有六种不蕴含关系，其中四种具有可证明的紧界。最小的共存见证为N=5，这是最优的：ICP要求3个两两不同的核心元素，所以N≥5。由D引起的三分类分解是同构不变量，ICP在逻辑上等价于标准的Compose+Inert公理。所有结果均在Lean 4中形式化，无sorry。