n(5,4,2)=24, and twenty-four cells of the edge-girth-regular table settled without exhaustive search
Abstract
An egr(v,k,g,λ) graph is a k-regular graph on v vertices of girth exactly g in which every edge lies on exactly λ cycles of length g; n(k,g,λ) denotes the least order of such a graph. Goedgebeur and Jooken tabulate n(k,g,λ) by exhaustive generation and leave many cells of the table with a two-sided gap. We exhibit a 5-regular triangle-free graph on 24 vertices in which every edge lies on exactly two 4-cycles. It improves the published upper bound n(5,4,2) ≤ 32 to 24 and, together with a matching lower bound proved here, gives n(5,4,2)=24. The lower bound uses no search: it is a codegree count of the kind used by Araujo-Pardo, Kiss and Porupsánszki, combined with the divisibility 2g | vkλ. We derive both from the definition of an edge-girth-regular graph, along with the counting parts of the Jajcay–Kiss–Miklavič proposition at girths 3 and 4 and the Drglin–Filipovski–Jajcay–Raiman lower bound, and we deduce the exact value of n(k,g,λ) at twenty-four cells of the table — twenty-three of them published values, whose two halves rest here on no unformalized computation. All statements below are 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
c6d44457d1f84057153575e9e52ae31980fbbf6ae77ddf59b2a0765fc550f70c
Claim ledger
Stated results
EGR1known data2026-08-22
82 kernel-checked egr(v,k,g,lambda) certificates covering cells of the n(k,g,lambda) table, 56 of them at cells with a published exact value
EGR2routine2026-08-22
IsEGR implies k-regularity as a SimpleGraph and the handshake identity v*k = 2|E|, hence Goedgebeur-Jooken's parity condition 2 | v*k, for all parameters
EGR3routine2026-08-22
Negative controls: the data, every parameter, and the two easily-forgotten clauses of IsEGR are each load-bearing
EGR4known data2026-08-22
Three Cayley-graph witnesses found by this repository's own search, two of them non-isomorphic to the published witnesses at the same parameters
EGR5known2026-08-22
The frontier: the smallest open cells of the table, recorded as unproved statements
EGR6routine2026-08-22
The girth-4 local picture: pathCount in closed form, and hence that λ counts the edges between the two (k-1)-neighbourhoods of an edge
EGR7routine2026-08-22
λ ≤ (k-1)² for girth 4, and the nonexistence statements it gives at every order simultaneously
EGR9candidate2026-08-23
n(5,4,2) = 24: an egr(24,5,4,2) graph found by this repository's SAT search, meeting Goedgebeur-Jooken's lower bound and improving their upper bound from 32
EGR8routine2026-08-22
The one degenerate order: IsEGR 0 k g lam is vacuously true, so EgrExists is a statement about n(k,g,λ) only for positive v
EGR10routine2026-08-28
All four parts of Jajcay–Kiss–Miklavič's Proposition 1 at girth 4, including the 8 ∣ v·k·λ and 2 ∣ k·λ divisibility conditions the published tables are indexed by
EGR11routine2026-08-28
The order tests as the published generation protocol uses them: which orders a cell of the table can have, and the two open cells they decide
EGR12routine2026-08-28
The literature lower bound for n(k,g,λ) at girth 3 and 4 — Drglin–Filipovski–Jajcay–Raiman's Theorem 2.3, the formula that generates that column of the published tables
EGR13routine2026-08-28
Twenty cells of the n(k,g,λ) table with both bounds kernel-checked, the family's first exact values that rest on no unformalized computation
EGR14routine2026-08-28
Proposition 1 at girth 3: 6 ∣ v·k·λ by a three-way rotation partition, and the two cells it closes
EGR15routine2026-08-28
The codegree bound v ≥ k² + 1 − kλ/2 at girth 4, and n(5,4,2) = 24 closed on both sides
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- n(k,g,lambda) — edge-girth-regular graphs: the least order of a k-regular graph of girth exactly g in which every edge lies on exactly lambda cycles of length g.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7