{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R517",
  "content_hash": null,
  "slug": "mgsl-artifact-word-and-group-verifier",
  "type": "artifact",
  "title": "Exact word-ball and full-group verifier",
  "summary": "A standard-library Python program proves generation, injectivity through radius eight, and a closing relation of length 17.",
  "relevance": "For Largest girth from two generators of SL(2,101), record mgsl-artifact-word-and-group-verifier (“Exact word-ball and full-group verifier”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program proves generation, injectivity through radius eight, and a closing relation of length 17.",
  "relevance_source": "recorded",
  "body": "Matrices are four-tuples \\((a,b,c,d)\\) with exact arithmetic modulo 101. The word-ball pass omits only immediate inverse steps. It checks the full free-tree layer vector through radius eight and rejects any repeated endpoint. It then scans the outer sphere for internal edges and verifies the lexicographically first resulting length-17 relation.\n\nThe generation pass encodes a matrix as\n\\[\na+101\\bigl(b+101(c+101d)\\bigr)\n\\]\nand uses a dense byte array for visited states. It reaches the full group order and checks the determinant of every reached matrix. The radius-eight endpoint table has SHA-256 digest `5a74202c3e18b637c5dbb63e89080cc4a4773101f13e1ecdf4fa0b64efba8bcb`. The portable little-endian BFS queue digest is `26d6373b5b6475e5d99ccf47a500d2b33ca00dd23793d80fed6893af0ba559a2`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all freely reduced words through length eight and all group elements reached by the displayed pair in SL_2(F_101)",
    "bounds": {
      "reduced_word_radius": {
        "min": 0,
        "max": 8
      },
      "word_ball_vertices": {
        "min": 13121,
        "max": 13121
      },
      "group_vertices": {
        "min": 1030200,
        "max": 1030200
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_verifier",
    "entrypoint": "Join source_lines with newline characters, save as check.py, and run python3 check.py",
    "runtime": "CPython 3, standard library only; 2.7 seconds on the entry-research host",
    "citation": {
      "url": "https://arxiv.org/abs/0707.1833",
      "locator": "Inline Python 3 computation executed on 2026-07-25"
    },
    "memory": "approximately 110 MB, chiefly a 101^4-byte visited array",
    "inline_source": [
      "from array import array",
      "from hashlib import sha256",
      "from json import dumps",
      "P=101",
      "A=(69,82,70,51)",
      "B=(41,48,47,92)",
      "I=(1,0,0,1)",
      "def mul(x,y):",
      "    a,b,c,d=x; e,f,g,h=y",
      "    return ((a*e+b*g)%P,(a*f+b*h)%P,(c*e+d*g)%P,(c*f+d*h)%P)",
      "def inv(x):",
      "    a,b,c,d=x",
      "    return d,(-b)%P,(-c)%P,a",
      "def enc(x):",
      "    a,b,c,d=x",
      "    return a+P*(b+P*(c+P*d))",
      "def dec(s):",
      "    a=s%P; s//=P",
      "    b=s%P; s//=P",
      "    c=s%P; d=s//P",
      "    return a,b,c,d",
      "gens=(A,inv(A),B,inv(B))",
      "names=('A','a','B','b')",
      "inverse_index=(1,0,3,2)",
      "assert all((x[0]*x[3]-x[1]*x[2])%P==1 for x in gens)",
      "assert len(set(gens))==4 and I not in gens",
      "seen={I:('',-1)}",
      "frontier=[(I,-1,'')]",
      "layers=[1]",
      "for depth in range(1,9):",
      "    next_frontier=[]",
      "    for x,last,word in frontier:",
      "        for gi,gen in enumerate(gens):",
      "            if last>=0 and gi==inverse_index[last]: continue",
      "            y=mul(x,gen)",
      "            new_word=word+names[gi]",
      "            assert y not in seen",
      "            seen[y]=(new_word,gi)",
      "            next_frontier.append((y,gi,new_word))",
      "    frontier=next_frontier",
      "    layers.append(len(frontier))",
      "expected_ball_layers=[1,4,12,36,108,324,972,2916,8748]",
      "assert layers==expected_ball_layers and len(seen)==13121",
      "outer={x:word for x,_,word in frontier}",
      "relations=[]",
      "for x,_,word in frontier:",
      "    for gi,gen in enumerate(gens):",
      "        y=mul(x,gen)",
      "        if y in outer: relations.append((word,names[gi],outer[y]))",
      "assert len(relations)==102",
      "left,edge,right=min(relations)",
      "inverse_name={'A':'a','a':'A','B':'b','b':'B'}",
      "closed=left+edge+''.join(inverse_name[ch] for ch in reversed(right))",
      "assert closed=='AAAABAbaabbaBBBBB' and len(closed)==17",
      "z=I",
      "for ch in closed: z=mul(z,gens[names.index(ch)])",
      "assert z==I",
      "ball_rows=sorted((enc(x),word) for x,(word,_) in seen.items())",
      "ball_payload='\\n'.join(f'{code}:{word}' for code,word in ball_rows).encode()",
      "ball_hash=sha256(ball_payload).hexdigest()",
      "assert ball_hash=='5a74202c3e18b637c5dbb63e89080cc4a4773101f13e1ecdf4fa0b64efba8bcb'",
      "space=P**4",
      "unseen=255",
      "dist=bytearray([unseen])*space",
      "start=enc(I)",
      "dist[start]=0",
      "queue=array('I',[start])",
      "group_layers=[1]",
      "head=0",
      "while head<len(queue):",
      "    state=queue[head]; head+=1",
      "    x=dec(state)",
      "    nd=dist[state]+1",
      "    for gen in gens:",
      "        code=enc(mul(x,gen))",
      "        if dist[code]==unseen:",
      "            dist[code]=nd",
      "            queue.append(code)",
      "            if nd==len(group_layers): group_layers.append(0)",
      "            group_layers[nd]+=1",
      "expected_group_layers=[1,4,12,36,108,324,972,2916,8748,25806,72666,186104,358712,322702,50899,188,2]",
      "order=P*(P*P-1)",
      "assert group_layers==expected_group_layers",
      "assert len(queue)==sum(group_layers)==order==1030200",
      "assert all((a*d-b*c)%P==1 for a,b,c,d in map(dec,queue))",
      "queue_digest=sha256()",
      "for state in queue: queue_digest.update(int(state).to_bytes(4,'little'))",
      "queue_hash=queue_digest.hexdigest()",
      "layers_hash=sha256(dumps(group_layers,separators=(',',':')).encode()).hexdigest()",
      "assert queue_hash=='26d6373b5b6475e5d99ccf47a500d2b33ca00dd23793d80fed6893af0ba559a2'",
      "assert layers_hash=='b69be1e5f368380aebd83f186ff384101b997baf0f404e9b6a810b6cd4b20d92'",
      "print('girth=17 relation='+closed)",
      "print('word_ball_vertices=13121 outer_internal_directed_edges=102')",
      "print('ball_sha256='+ball_hash)",
      "print('group_order='+str(order)+' diameter='+str(len(group_layers)-1))",
      "print('queue_sha256='+queue_hash)",
      "print('layers_sha256='+layers_hash)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/0707.1833",
    "locator": "Inline Python 3 computation executed on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R521",
      "title": "The displayed generating pair has girth exactly 17",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "max-girth-sl2-101-generators",
      "title": "max girth sl2 101 generators",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}