pith. sign in

arxiv: 2603.27007 · v2 · submitted 2026-03-27 · 💻 cs.LO

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

Stefano Palmieri This is my paper

Pith reviewed 2026-05-14 22:30 UTC · model grok-4.3

classification 💻 cs.LO
keywords finite magmasextensional magmaspairwise independencecombinatory algebrasinternal compositionclassifier dichotomyLean formalization
0
0 comments X

The pith

Self-representation, classifier dichotomy and internal composition are pairwise independent in finite extensional 2-pointed magmas.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper isolates three properties—self-representation (R), classifier dichotomy (D), and internal composition property (H)—within finite extensional 2-pointed magmas. It shows that none of these properties implies any other by exhibiting explicit finite counterexamples for every non-implication. Lean 4 verifies all six directions with models ranging from size 4 to 10, four of which achieve provably minimal cardinality. The smallest magma realizing all three properties at once has exactly five elements, a bound shown to be tight because H demands three distinct core elements. This separation maps out the possible combinations of algebraic features that survive in the finite non-associative setting.

Core claim

In finite extensional 2-pointed magmas the properties R (self-representation), D (classifier dichotomy) and H (internal composition property) are pairwise independent. Lean-verified models of cardinalities 4 through 10 witness all six non-implications, with four bounds tight. The smallest model satisfying R, D and H simultaneously has cardinality 5, which is optimal because H requires three pairwise distinct core elements. The three-category decomposition induced by D is an isomorphism invariant, and H is logically equivalent to the standard Compose+Inert axioms.

What carries the argument

The three properties self-representation (R), classifier dichotomy (D) and internal composition property (H), together with the three-category decomposition induced by D, inside the class of finite extensional 2-pointed magmas.

If this is right

  • Any two of the three properties can coexist without the third in structures of small finite size.
  • The three-category decomposition induced by D is preserved under isomorphism.
  • The internal composition property is logically equivalent to the Compose+Inert axioms.
  • The minimal cardinality of a structure satisfying R, D and H together is exactly five.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Dependencies among the properties may appear once associativity is restored, consistent with known obstructions for semigroups and combinatory algebras.
  • The explicit small models supply concrete test cases for exploring further combinations of algebraic axioms in the finite setting.
  • The Lean formalization supplies a verified base that can be extended to study related retraction or representation properties.

Load-bearing premise

The independence results hold only inside the restricted class of finite, total, non-associative, extensional 2-pointed magmas.

What would settle it

A magma of size less than 5 that satisfies all three properties simultaneously, or a counterexample of any size inside the finite extensional class in which one property implies another.

Figures

Figures reproduced from arXiv: 2603.27007 by Stefano Palmieri.

Figure 1
Figure 1. Figure 1: Full independence structure. All six pairwise non [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper examines finite extensional 2-pointed magmas and isolates three properties—self-representation (R), classifier dichotomy (D), and Internal Composition Property (H). It proves pairwise independence of R, D, and H by exhibiting Lean 4 formalizations of all six non-implications, using explicit finite counterexamples of sizes 4–10 (four with provably tight bounds). The minimum size permitting coexistence of all three is shown to be N=5, which is optimal because ICP requires three distinct core elements. The D-induced three-category decomposition is proved to be an isomorphism invariant, and H is shown to be logically equivalent to the standard Compose+Inert axioms. All theorems and counterexamples are machine-checked in Lean 4 with zero 'sorry' statements.

Significance. If the results hold, the work supplies a precise map of the remaining finite non-associative extensional landscape after the known obstructions from associativity and infinitude are removed. The machine-checked counterexamples and tight bounds constitute strong, reproducible evidence for the independence claims; the explicit minimal coexistence size N=5 and the isomorphism invariance of the D-decomposition are concrete, falsifiable contributions that can guide subsequent classification efforts in this restricted algebraic setting.

minor comments (2)
  1. [§2.2] §2.2: the definition of the classifier dichotomy (D) would benefit from an explicit enumeration of the three categories for one of the size-5 examples to make the subsequent invariance claim easier to verify by inspection.
  2. [Table 1] Table 1: the column headers for the six non-implication witnesses could include the exact cardinalities alongside the Lean file references for quicker cross-reference with the text.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the manuscript. The summary accurately captures the main contributions regarding the pairwise independence of R, D, and H in finite extensional 2-pointed magmas, the Lean 4 formalizations, the tight bounds on counterexamples, and the optimality of the N=5 coexistence witness.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines three properties (self-representation R, classifier dichotomy D, Internal Composition Property H) directly from the structure of finite extensional 2-pointed magmas and establishes their pairwise independence via exhaustive Lean 4 counterexamples of sizes 4-10. These are machine-checked formal verifications with zero sorry, not fitted parameters renamed as predictions, self-referential equations, or load-bearing self-citations. The scope is explicitly restricted to the finite non-associative case where such counterexamples exist, and the results are self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper rests on standard definitions of magmas, extensionality, and 2-pointed structures from algebraic logic; no free parameters are fitted, no new entities are postulated, and the Lean formalization uses only the standard Lean 4 kernel axioms.

axioms (2)
  • standard math Extensionality: two elements are equal iff they agree under the binary operation for all arguments
    Invoked as the definition of extensional magma throughout the paper.
  • standard math Totality of the binary operation in a magma
    Standard background assumption for all magmas considered.

pith-pipeline@v0.9.0 · 5506 in / 1407 out tokens · 42721 ms · 2026-05-14T22:30:05.722619+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [1]

    Reflection and semantics in Lisp

    Brian Cantwell Smith. Reflection and semantics in Lisp. InPOPL, pages 23–35, 1984

    work page 1984

  2. [2]

    Efficient self-interpretation in lambda calculus.Journal of Functional Programming, 2(3):279–291, 1992

    Torben Mogensen. Efficient self-interpretation in lambda calculus.Journal of Functional Programming, 2(3):279–291, 1992

    work page 1992

  3. [3]

    Breaking through the normalization barrier: A self-interpreter for F-omega

    Matt Brown and Jens Palsberg. Breaking through the normalization barrier: A self-interpreter for F-omega. InPOPL, pages 5–17, 2016

    work page 2016

  4. [4]

    Springer, 1971

    Saunders Mac Lane.Categories for the Working Mathematician. Springer, 1971

    work page 1971

  5. [5]

    Johnstone.Sketches of an Elephant: A Topos Theory Compendium, vol

    Peter T. Johnstone.Sketches of an Elephant: A Topos Theory Compendium, vol. 1. Oxford University Press, 2002

    work page 2002

  6. [6]

    Springer, 2004

    Leonid Libkin.Elements of Finite Model Theory. Springer, 2004

    work page 2004

  7. [7]

    Stanley Burris and H. P. Sankappanavar.A Course in Universal Algebra. Springer, 1981

    work page 1981

  8. [8]

    https://www.cs.unm.edu/~mccune/prover9/, 2005–2010

    William McCune.Prover9 and Mace4. https://www.cs.unm.edu/~mccune/prover9/, 2005–2010

    work page 2005

  9. [9]

    The Lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. InCADE, pages 625–635, 2021

    work page 2021

  10. [10]

    Studies in Logic and the Foundations of Mathematics 152, Elsevier, 2008

    Jaap van Oosten.Realizability: An Introduction to its Categorical Side. Studies in Logic and the Foundations of Mathematics 152, Elsevier, 2008

    work page 2008

  11. [11]

    Theory and Applications of Computability, Springer, 2015

    John Longley and Dag Normann.Higher-Order Computability. Theory and Applications of Computability, Springer, 2015. , , Stefano Palmieri

    work page 2015

  12. [12]

    PhD thesis, Universiteit van Amsterdam, 1988

    Ingemarie Bethke.Notes on Partial Combinatory Algebras. PhD thesis, Universiteit van Amsterdam, 1988

    work page 1988

  13. [13]

    Collapsing partial combinatory algebras

    Ingemarie Bethke and Jan Willem Klop. Collapsing partial combinatory algebras. InHigher-Order Algebra, Logic, and Term Rewriting (HOA 1995), LNCS 1074, pages 16–48, Springer, 1996.doi: 10.1007/3-540-61254-8_18

    work page doi:10.1007/3-540-61254-8_18 1995

  14. [14]

    J. Robin B. Cockett and Pieter Hofstra. Introduction to Turing categories.Annals of Pure and Applied Logic, 156(2–3):183–209, 2008.doi: 10.1016/j.apal.2008.04.005. A Cayley Tables All tables are extracted from the Lean source files and verified by lake build. Element𝑖’s row is row𝑖; entry(𝑖, 𝑗)is𝑖·𝑗. 𝑁= 4: Minimal R+D witness ( 𝑠=𝑟 ).Roles:0 =𝑧 1,1 =𝑧 2,2...

    work page doi:10.1016/j.apal.2008.04.005 2008