{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R324",
  "content_hash": null,
  "slug": "gct45-artifact-rational-bound-certificate",
  "type": "artifact",
  "title": "Exact rational verifier for the certified interval",
  "summary": "Standard-library Python rebuilds the graph and checks every integer and rational used in the interval proof.",
  "relevance": "For Largest expected cover time on the four by five grid, record gct45-artifact-rational-bound-certificate (“Exact rational verifier for the certified interval”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python rebuilds the graph and checks every integer and rational used in the interval proof.",
  "relevance_source": "recorded",
  "body": "The program constructs the row-major 4 by 5 grid, checks its order, size, connectivity, diameter, and six reflection orbits, and performs the harmonic-number calculation with `Fraction`. Its graph payload lists each undirected edge as `u:v` in lexicographic order. The certificate uses the commute-time identity, the path resistance bound, and Matthews's inequality. The resulting interval is rigorous for every start.\n\nFor a future exact solve, let \\(F(S,v)\\) be the expected remaining time when the connected visited set is \\(S\\) and the walker is at \\(v\\in S\\). Set \\(F(V,v)=0\\). For each proper connected \\(S\\), solve the rational Dirichlet system\n\\[\n\\deg(v)F(S,v)-\\sum_{w\\sim v,\\,w\\in S}F(S,w)=\\deg(v)+\\sum_{w\\sim v,\\,w\\notin S}F(S\\cup\\{w\\},w).\n\\]\nProcessing sets by decreasing size supplies every right-hand side. The exact start values are \\(F(\\{v\\},v)\\). There are 116,166 connected nonempty vertex sets, with size histogram `[20,31,70,161,376,859,1870,3794,7028,11641,16872,20809,21090,16702,9692,3894,1050,186,20,1]`. This run reached the state-count check, but the full rational solve exceeded the entry time cap.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the exact rational lower and upper certificates for the maximum expected cover time on P_4 square P_5",
    "bounds": {
      "rows": {
        "min": 4,
        "max": 4
      },
      "columns": {
        "min": 5,
        "max": 5
      },
      "vertices": {
        "min": 20,
        "max": 20
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_rational_certificate",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.1214/aop/1176991686",
      "locator": "Self-contained CPython standard-library exact arithmetic certificate prepared on 2026-07-25"
    },
    "inline_source": [
      "from collections import deque",
      "from fractions import Fraction",
      "from hashlib import sha256",
      "import json",
      "R,C=4,5",
      "adj=[set() for _ in range(R*C)]",
      "for r in range(R):",
      " for c in range(C):",
      "  v=r*C+c",
      "  for dr,dc in ((1,0),(-1,0),(0,1),(0,-1)):",
      "   rr,cc=r+dr,c+dc",
      "   if 0<=rr<R and 0<=cc<C: adj[v].add(rr*C+cc)",
      "edges=sorted((v,w) for v in range(R*C) for w in adj[v] if v<w)",
      "assert len(adj)==20 and len(edges)==31",
      "diam=0",
      "for s in range(20):",
      " d=[-1]*20; d[s]=0; q=deque([s])",
      " while q:",
      "  v=q.popleft()",
      "  for w in adj[v]:",
      "   if d[w]<0: d[w]=d[v]+1; q.append(w)",
      " diam=max(diam,max(d))",
      "assert diam==7",
      "orbits={min((r,c),(R-1-r,c),(r,C-1-c),(R-1-r,C-1-c)) for r in range(R) for c in range(C)}",
      "assert len(orbits)==6",
      "h=sum((Fraction(1,k) for k in range(1,20)),Fraction())",
      "assert h==Fraction(275295799,77597520)",
      "upper=h*(2*len(edges)*diam)",
      "assert upper==Fraction(8534169769,5542680)",
      "graph_payload=''.join('%d:%d\\n'%e for e in edges).encode()",
      "report={'diameter':diam,'edges':len(edges),'graph_sha256':sha256(graph_payload).hexdigest(),'harmonic_19':str(h),'lower_bound':19,'start_orbits':len(orbits),'upper_bound':str(upper),'vertices':len(adj)}",
      "payload=json.dumps(report,sort_keys=True,separators=(',',':'))",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1214/aop/1176991686",
    "locator": "Self-contained CPython standard-library exact arithmetic certificate prepared on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R326",
      "title": "The maximum expected cover time lies in a certified rational interval",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "grid-cover-time-four-by-five",
      "title": "grid cover time four by five",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}