[
  {
    "local_id": "C1",
    "type": "theoretical",
    "core": true,
    "statement": "For every integer m ≥ 2, the following successor rule traces a Hamiltonian cycle of SB(m, 3), the digraph whose vertices are the strings xyz with 0 ≤ x, y, z < m and whose arcs go from xyz to yzx and to yz(x+1 mod m). With k = ⌊m/2⌋ + 1, the successor of xyz is yzx when y ≥ k and z < k, when y = 0 and z ≠ 0, or when z = 1 and y ≥ 2, except that for odd m ≥ 7 it is yz(x+1 mod m) when z = 1 and y ≥ k + 1; every other xyz has successor yz(x+1 mod m). Starting from 000, the first m³ steps of the walk visit m³ distinct vertices, which is every vertex, and the walk is back at 000 after m³ steps.",
    "evidence": [
      {
        "proof": "proofs/SB3.lean",
        "theorem": "SB.sb3_hamiltonian_cycle",
        "checker": "lean4"
      }
    ],
    "depends_on": [],
    "falsified_if": "For some m ≥ 2 the walk from 000 under this rule repeats a vertex within its first m³ steps, misses a vertex, or is not at 000 after m³ steps; or the definitions Bump and next in proofs/SB3.lean do not express the rule as stated.",
    "confidence": 0.99
  }
]