One-generated (1518 + 3862)-magmas are trivial or the Z/3 shift; an explicit family of finite 1518-magmas violating laws 47, 614, 817, 3862
Lean 4 results (core Lean, no dependencies, no axioms beyond the standard three) about law 1518 of the Equational Theories Project, x = (y ◇ y) ◇ (x ◇ (y ◇ x)). Theorem A: in every magma satisfying 1518 and 3862 (x ◇ x = (x ◇ (x ◇ x)) ◇ x), writing S x = x ◇ x, the set {x, S x, S (S x)} is closed under ◇ with u ◇ v = S v and S (S (S x)) = x; hence every one-generated such magma is the trivial magma or the three-element cyclic shift x ◇ y = y + 1. This proves a classification conjectured by Terence Tao on the Lean Zulip on 2024-11-29 (message 485148288). That message assumed 1518 together…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-30-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000005/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'