TheoremDB

Problem packetWorkR520

R520claimStatus: establishedEvidence: EstablishedReplay: source onlyexhaustive over its scope

[#R520] The Moore bound gives a universal ceiling of 24

claim. Girth 25 would require 1,062,881 vertices, which is 32,681 too many.

View evidenceOpen source ↗

1Summary

Suppose a 4-regular graph has girth at least 25. The nonbacktracking paths of length at most 12 starting at a fixed vertex have distinct endpoints. Otherwise two such paths would give a cycle of length at most 24. The graph therefore has at least \[ 1+4(1+3+\cdots+3^{11}) =1+2(3^{12}-1) =1{,}062{,}881 \] vertices. The Cayley graphs in this problem have 1,030,200 vertices, so their girth is at most 24.

Established evidence. Recorded scope: every simple 4-regular graph on 1,030,200 vertices, including every eligible Cayley graph in the problem.

2Evidence

Replay package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: arxiv.org ↗, Gamburd, Hoory, Shahshahani, Shalev, and Virag, On the girth of random Cayley graphs, Section 1 discusses the Moore counting bound; the numerical specialization is shown here

3What was measured

Hypothetical girth
25
Required vertices
1,062,881
Available vertices
1,030,200
Deficit
32,681
Certified upper bound
24

4How it connects

Recorded for

5Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R520",
  "content_hash": null,
  "slug": "mgsl-claim-moore-upper-bound",
  "type": "claim",
  "title": "The Moore bound gives a universal ceiling of 24",
  "summary": "Girth 25 would require 1,062,881 vertices, which is 32,681 too many.",
  "relevance": "For Largest girth from two generators of SL(2,101), record mgsl-claim-moore-upper-bound (“The Moore bound gives a universal ceiling of 24”) records a bound, answer, status fact, or structural consequence. The record states: Girth 25 would require 1,062,881 vertices, which is 32,681 too many.",
  "relevance_source": "recorded",
  "body": "Suppose a 4-regular graph has girth at least 25. The nonbacktracking paths of length at most 12 starting at a fixed vertex have distinct endpoints. Otherwise two such paths would give a cycle of length at most 24. The graph therefore has at least\n\\[\n1+4(1+3+\\cdots+3^{11})\n=1+2(3^{12}-1)\n=1{,}062{,}881\n\\]\nvertices. The Cayley graphs in this problem have 1,030,200 vertices, so their girth is at most 24.",
  "status": "established",
  "evidence_grade": "proved",
  "scope": {
    "kind": "bounded",
    "statement": "every simple 4-regular graph on 1,030,200 vertices, including every eligible Cayley graph in the problem",
    "bounds": {
      "vertices": {
        "min": 1030200,
        "max": 1030200
      },
      "degree": {
        "min": 4,
        "max": 4
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/0707.1833",
      "locator": "Gamburd, Hoory, Shahshahani, Shalev, and Virag, On the girth of random Cayley graphs, Section 1 discusses the Moore counting bound; the numerical specialization is shown here"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/0707.1833",
    "locator": "Gamburd, Hoory, Shahshahani, Shalev, and Virag, On the girth of random Cayley graphs, Section 1 discusses the Moore counting bound; the numerical specialization is shown here"
  },
  "models": [],
  "relations": [
    {
      "slug": "R519",
      "title": "The maximum girth is currently certified between 17 and 24",
      "object_type": "claim",
      "relation": "bounds",
      "direction": "outgoing"
    },
    {
      "slug": "max-girth-sl2-101-generators",
      "title": "max girth sl2 101 generators",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

6Provenance

View source, identifiers, and projection details
Project
max-girth-sl2-101-generators
Locator
Gamburd, Hoory, Shahshahani, Shalev, and Virag, On the girth of random Cayley graphs, Section 1 discusses the Moore counting bound; the numerical specialization is shown here
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R520
Stable alias
mgsl-claim-moore-upper-bound
Projection
Reproduction fields are derived from the immutable record.

A statement this project treats as settled at the recorded evidence grade, with the work that backs it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.