/* Direct check of the construction, independent of the Lean proof: for each m in [lo, hi], walk
 * from 000 under the bump rule and confirm that the walk visits m^3 distinct vertices and is back
 * at 000 after exactly m^3 steps. Usage: cc -O2 -o check_cycles check_cycles.c && ./check_cycles 2 500
 */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

static int bump(int m, int y, int z) {
  int k = m / 2 + 1;
  if (m % 2 == 1 && m >= 7 && z == 1 && y >= k + 1) return 1;
  if (y >= k && z < k) return 0;
  if (y == 0 && z != 0) return 0;
  if (z == 1 && y >= 2) return 0;
  return 1;
}

int main(int argc, char **argv) {
  int lo = argc > 1 ? atoi(argv[1]) : 2, hi = argc > 2 ? atoi(argv[2]) : 200, failures = 0;
  for (int m = lo; m <= hi; m++) {
    long n = (long)m * m * m;
    unsigned char *seen = calloc(n, 1);
    unsigned char *b = malloc((size_t)m * m);
    for (int y = 0; y < m; y++) for (int z = 0; z < m; z++) b[y * m + z] = (unsigned char)bump(m, y, z);
    int x = 0, y = 0, z = 0, ok = 1;
    for (long t = 0; t < n; t++) {
      long v = ((long)x * m + y) * m + z;
      if (seen[v]) { ok = 0; break; }
      seen[v] = 1;
      int nz = (x + b[y * m + z]) % m;
      x = y; y = z; z = nz;
    }
    if (ok && (x | y | z)) ok = 0;
    if (!ok) { failures++; printf("m=%d: not a Hamiltonian cycle\n", m); }
    free(seen); free(b);
  }
  printf("m=%d..%d: %d failures\n", lo, hi, failures);
  return failures != 0;
}