Rectangular dimonoids as pairs of partition refinements, an abelian collapse for g-dimonoids, and new entries in the enumeration of dimonoids, g-dimonoids and doppelsemigroups of small order
Abstract
Three recent papers of V. M. Gavrylkiv count, up to isomorphism, the dimonoids, the g-dimonoids and the doppelsemigroups of small order, together with their commutative, abelian, rectangular and strong subclasses, and each closes with one problem asking for the next entries of its tables. We prove two structure theorems, settle a published disagreement about the three-element case, and fill twenty of the entries those problems ask for. The first structure theorem describes the rectangular case completely. For a pair of rectangular semigroups ⊣, ⊢ on one set — rectangular meaning x * y * z = x * z — Loday's axiom (D₁) holds if and only if the partition of the carrier into columns of ⊢ refines the partition into columns of ⊣, and (D₃) holds if and only if the partition into rows of ⊣ refines the partition into rows of ⊢. A rectangular g-dimonoid is therefore exactly a pair of rectangular semigroups with these two opposite refinements, and the sections that make up the rest of the data of a rectangular semigroup play no part: replacing ⊢ by any rectangular semigroup with the same rows and columns preserves the axioms. The second is that an abelian g-dimonoid is automatically a dimonoid, so that agdm(n) = adm(n) for every n and two of the problems' clauses are one clause; this statement is also proved, independently and earlier, in a companion paper of ours, and the corresponding statements for dimonoids and for doppelsemigroups are due to A. V. Zhuchok and to Zhuchok and Knauer. We also record an arithmetic consequence of the known count of 3-nilpotent semigroups: the abelian layer, which looks thin for n ≤ 6, is 79.8 of all semigroups of order 7 and 99.74 Two published classifications of the three-element doppelsemigroups disagree, one giving 75 classes in 41 commutative ones and 17 dual pairs and the later one giving 77 and 18. We certify the later count inside a proof assistant, directly from the axioms and over all 3⁹ multiplication tables, together with the whole duality structure of that order: the 18 dual pairs listed one by one, the iso-dual classes being exactly the commutative ones, and 31 iso-opposite and 15 iso-cross-dual classes, two counts the sources do not print. We also prove, inside the proof assistant, that there are at least 1364 pairwise non-isomorphic rectangular dimonoids of order 7 — a lower bound matching the value rdm(7) = 1364 that our search returns. By exhaustive computation we determine dm(6) = 212 193 607, gdm(6) = 559 338 535, ds(6) = 212 886 176, sds(6) = 212 396 016, adm(7) = agdm(7) = 1 299 527, ads(7) = 1 258 518, adm(8) = agdm(8) = 3 674 424 652, ads(8) = 3 672 523 869, rdm(7) = 1364, rgdm(7) = 14 710, rds(7) = 571, cdm(7) = 83 580 226, cgdm(7) = 242 117 995, cds(7) = 84 998 302, and, two and three orders beyond the published tables, rdm(8) = 3903, rdm(9) = 10 599, rgdm(8) = 81 905, rgdm(9) = 472 836. The structural results, the order-3 census and the lower bound for rdm(7) are machine-checked in Lean 4; the computed values of Section [sec:new] are not, and are labelled as such throughout.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 2 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
0363d47869d156894f39b30ef2c51479c092837a55c92fb1f3cdf33fc6f6ffec
Claim ledger
Stated results
DC1known2026-09-03
Abelianness of a pair of operations is exactly ⊢ = ⊣ᵈ (abelianᵢff_dual), and a homomorphism for ⊣ is a homomorphism for ⊣ᵈ (map_dual), so the collapse is equivariant and descends to isomorphism classes
DC2known2026-09-03
(D,⊣,⊣ᵈ) is a dimonoid iff ⊣ is associative and right commutative, x(yz)=x(zy); each of (D₁),(D₂),(D₃) becomes that one identity
DC3known2026-09-03
(D,⊣,⊣ᵈ) is a doppelsemigroup iff ⊣ is associative, right commutative and left commutative
DC4candidate2026-09-03
An abelian g-dimonoid is a dimonoid: axiom (D₂) follows from (D₁),(D₃) and abelianness; hence agdm(n) = adm(n) for every n, as sets of structures and up to isomorphism
DC5known2026-09-03
The abelian structures on a carrier are exactly the pairs (l, lᵈ) with l in the appropriate identity variety (abelian_dimonoidᵢff, abelian_doppelᵢff)
DC6known2026-09-03
Every abelian doppelsemigroup is an abelian dimonoid, so ads(n) ≤ adm(n); and in an abelian dimonoid (x⊣y)⊣z = (x⊣z)⊣y
DC7candidate2026-09-03
Every semigroup all of whose triple products are equal is left and right commutative (nil3ᵢdA, nil3ᵢdB), so every 3-nilpotent semigroup of order n carries an abelian dimonoid and an abelian doppelsemigroup; with Distler-Mitchell's Table 3 and A027851(9) this gives the unconditional interval 105931872028455 <= ads(9) <= adm(9) = agdm(9) <= 105978177936292 (relative width 0.0437 percent), and the unconditional ratios adm(7)/s(7) = 0.7984, adm(8)/s(8) = 0.99739; the limit adm(n)/s(n) -> 1 is conditional on the presumed asymptotic that Distler-Mitchell state is NOT a consequence of Kleitman-Rothschild-Spencer 1976
This ledger entry is reported in prose and is not bound to a Lean theorem.DC8known2026-09-03
A semigroup is rectangular iff it satisfies both (xy)z = xz and x(yz) = xz; then x*y = (x*x)*(y*y) and the diagonal values are idempotent
DC9known data2026-09-03
The order-3 row of every table of the three sources, computed in the kernel from the axioms over all 3⁹ tables: s=24, cs=12, rs=5, dm=52, cdm=14, rdm=18, gdm=78, cgdm=22, rgdm=27, ds=77, cds=41, sds=65, rds=7, and 113 labelled semigroups
DC10known data2026-09-03
The order-3 abelian layer computed twice in the kernel and agreeing: adm(3)=agdm(3)=17 from the dimonoid axioms and 17 as isomorphism classes of right commutative semigroups; ads(3)=12 both ways; with the controls 52 < 78 and 12 < 17
DC11candidate2026-09-03
adm(7) = agdm(7) = 1299527
This ledger entry is reported in prose and is not bound to a Lean theorem.DC12candidate2026-09-03
ads(7) = 1258518
This ledger entry is reported in prose and is not bound to a Lean theorem.DC13candidate2026-09-03
adm(8) = agdm(8) = 3674424652
This ledger entry is reported in prose and is not bound to a Lean theorem.DC14candidate2026-09-03
ads(8) = 3672523869
This ledger entry is reported in prose and is not bound to a Lean theorem.DC15candidate2026-09-03
rdm(7) = 1364
This ledger entry is reported in prose and is not bound to a Lean theorem.DC16candidate2026-09-03
rgdm(7) = 14710
This ledger entry is reported in prose and is not bound to a Lean theorem.DC17candidate2026-09-03
rds(7) = 571
This ledger entry is reported in prose and is not bound to a Lean theorem.DC18known2026-09-03
rs(7) = 36, and the rectangular-semigroup sequence is OEIS A390162 with a b-file to n = 200
This ledger entry is reported in prose and is not bound to a Lean theorem.DC19measurement2026-09-03
Cost of the n = 6 pair search: the four open cells dm(6), gdm(6), ds(6), sds(6) reduce to a constraint DFS over the 36 cells of the second operation, one representative per isomorphism class of order-6 semigroup, with Burnside inside Aut; validated at n = 3,4,5 on all four sequences; the cost is concentrated in the 2660 degree-3 nilpotent classes
This ledger entry is reported in prose and is not bound to a Lean theorem.DC20candidate2026-09-03
dm(6) = 212193607: the number of dimonoids of order 6 up to isomorphism
This ledger entry is reported in prose and is not bound to a Lean theorem.DC21candidate2026-09-03
gdm(6) = 559338535: the number of g-dimonoids of order 6 up to isomorphism
This ledger entry is reported in prose and is not bound to a Lean theorem.DC22candidate2026-09-03
ds(6) = 212886176: the number of doppelsemigroups of order 6 up to isomorphism
This ledger entry is reported in prose and is not bound to a Lean theorem.DC23candidate2026-09-03
sds(6) = 212396016: the number of strong doppelsemigroups of order 6 up to isomorphism; and sds(6)/ds(6) = 0.9977 against 0.828 at n = 5, the nilpotent-dominated regime making almost every doppelsemigroup strong
This ledger entry is reported in prose and is not bound to a Lean theorem.DC24measurement2026-09-03
Measured cost of the four n = 6 cells: 1403 s (dm), 3419 s (gdm), 3133 s (ds), 3431 s (sds), 3.16 CPU-h in total, with the cost concentrated in Smallsemi's diag = 111111 block and one outlier (the null semigroup O₆ alone costs 637 s in the ds mode and 780 s in the sds mode)
This ledger entry is reported in prose and is not bound to a Lean theorem.DC25candidate2026-09-03
For rectangular ⊣ and ⊢ on one carrier, (D₁) holds iff the column partition of ⊢ refines that of ⊣, and (D₃) holds iff the row partition of ⊣ refines that of ⊢; hence a rectangular g-dimonoid is exactly a pair of rectangular semigroups with those two opposite refinements, in which the sections play no part at all (gdimonoidₛections_free)
DC26known data2026-09-03
The order-3 duality census, from the axioms over all 3⁹ tables: ds(3) = 77 = 41 + 2*18 with the 18 dual pairs of noncommutative classes listed literally in the kernel, the iso-dual classes exactly the 41 commutative ones, 24 trivial, 65 strong, 12 abelian, 7 rectangular with the source's own split 1 + 2*2 + 1*2 – adjudicating Gavrylkiv-Rendziak 2019's published 75 = 41 + 2*17
DC27routine2026-09-03
At order 3 there are 31 iso-opposite and 15 iso-cross-dual doppelsemigroup classes against 24 trivial and 12 abelian ones, so the smallest nonabelian iso-cross-dual doppelsemigroups have three elements and there are exactly three of them; and every iso-dual class of order 3 is commutative
DC28candidate2026-09-03
cdm(7) = 83580226: the number of commutative dimonoids of order 7 up to isomorphism
This ledger entry is reported in prose and is not bound to a Lean theorem.DC29candidate2026-09-03
cgdm(7) = 242117995: the number of commutative g-dimonoids of order 7 up to isomorphism
This ledger entry is reported in prose and is not bound to a Lean theorem.DC30candidate2026-09-03
cds(7) = 84998302: the number of commutative doppelsemigroups of order 7 up to isomorphism
This ledger entry is reported in prose and is not bound to a Lean theorem.DC31candidate2026-09-03
rdm(8) = 3903 and rdm(9) = 10599, with rdm(7) = 1364 re-derived by a second, algorithmically independent program
This ledger entry is reported in prose and is not bound to a Lean theorem.DC32candidate2026-09-03
rgdm(8) = 81905 and rgdm(9) = 472836, with rgdm(7) = 14710 re-derived by the same second program
This ledger entry is reported in prose and is not bound to a Lean theorem.DC33candidate2026-09-03
rdm(7) >= 1364 inside the kernel: 1364 structures on 0,...,6, each proved a rectangular dimonoid in the sense of Defs.lean, no two of them isomorphic
DC34measurement2026-09-03
Measured prices from the order-7 rectangular pull: rgdm(7) >= 14710 in the kernel is 10.8x the rdm file (about 1.0 CPU-h, needing 4 chunk modules to stay under the 30-minutes-per-file rule); n = 10 is over the 10 GB cap before any search runs (A389829(10) = 48071832 labelled rectangular semigroups, 24 GB for the table and its index); the exact rdm(7) = 1364 in the kernel needs a proved-complete enumeration of the 31117 labelled rectangular semigroups plus about 5e10 relabellings for an isomorphism-class count; and dimonoid-counts is now a DYLIB family
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- A dimonoid (D, ⊣, ⊢) (Loday) is a set with two *associative* binary operations satisfying
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7