The order of a counterexample: two problems of Kinyon and Phillips on loops with left nuclear squares
Abstract
Kinyon and Phillips study loops in which every square lies in two of the three nuclei, and leave three problems open; each of the three asks for a loop with left nuclear squares. We prove that two of them have no counterexample of prime order and none of order twice an odd prime. The theorem behind this is a statement about a single nucleus: a finite loop with left nuclear squares and endomorphic squaring whose order is a prime, or twice an odd prime, has middle nuclear squares and has the automorphic inverse property. Commuting squares, which one of the two problems assumes, is never used. The proof is arithmetic rather than a search: the squaring map is an endomorphism, so the order of the loop is the number of squares times the number of elements of square e; both factors are at least two for a counterexample; and at order 2p the two surviving factorizations are killed by a fixed-point-free involution and by the centrality of a two-element kernel. The exclusion is sharp in the sense that it cannot be widened to composite, or even to even, orders: the authors' own Example 5.10 has the hypotheses and fails middle nuclear squares at order 8=2 · 4. We also reproduce one direction of their Theorem 5.4, verify the property profiles of their six example loops, and record an exhaustive search that leaves no counterexample of order 5 or 6. Every theorem below is machine-checked in Lean 4.
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 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
0b52512b818a3a0aab84e5f28a5f236c0161b0a97022df83370df00b7bbbe81f
Claim ledger
Stated results
Q1known2026-08-22
The source's Theorem 5.4: in a loop with squares in two nuclei, endomorphic squaring forces every square to commute with every element
Q2known data2026-08-22
Validation: all six example loops of the source, machine-verified, every property profile matching the paper's claim
Q3routine2026-08-22
No counterexample to any of the three problems has order 5 or 6, by an in-Lean exhaustion whose completeness is proved
Q4routine2026-08-22
Structural constraints on any counterexample: squares in the left nucleus only, and associativity holding modulo the kernel of squaring
Q5routine2026-08-22
Negative controls: the two definition traps, a too-small structure and a too-large one
Q6routine2026-08-22
External frontier: no counterexample of order <= 9 by SAT, and Problem 5.11 closed at order 8 by two strictly weaker statements
This ledger entry is reported in prose and is not bound to a Lean theorem.Q7known2026-08-28
The homomorphism theorem for the squaring map: in any finite loop with endomorphic squaring, (number of squares) x (number of elements of square e) = the order of the loop
Q8routine2026-08-28
Structural constraints on a counterexample: an involution among the squares makes both counts even; a two-element squaring kernel is central, and if its involution is not a square the loop is a group; hence 4 divides n, or both counts are at least 3
Q9candidate2026-08-28
No counterexample to Problem 5.8 or Problem 5.11 has prime order or order twice an odd prime – infinitely many orders excluded by a proof, with no search
Q10routine2026-08-28
Controls for the order theorems: endomorphic squaring is load-bearing three times over, the hypotheses are not vacuous, and the source's own Example 5.10 shows the exclusion cannot be widened to even or composite orders
Q11candidate2026-08-30
Problem 5.8 of Kinyon-Phillips answered YES: an explicit loop of order 12 with left nuclear squares and endomorphic squaring that fails the automorphic inverse property – and no smaller order is possible
Q12candidate2026-08-30
Problem 5.11 of Kinyon-Phillips answered YES at order 16 – and both of the strictly weaker statements the previous dispatches proposed as the route to proving it are false
Q13candidate2026-08-30
Problem 5.6 of Kinyon-Phillips answered YES at order 32, so all three of the source's open problems now have explicit kernel-checked answers
Q14routine2026-08-30
Controls for the three answers, and the complete central-extension sweep that produced them: every abelian G with |G| <= 32, i.e. every loop order up to 64
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Three open problems from Michael Kinyon and J. D. Phillips, "Loops with squares in two nuclei", arXiv:2510.19961, 22 Oct 2025 (0 citations as of 2026-08-22).
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7