{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R651",
  "content_hash": null,
  "slug": "rls12-artifact-small-order-replay",
  "type": "artifact",
  "title": "Exact small-order enumeration and order-12 arithmetic replay",
  "summary": "Standard-library Python enumerates R_2 through R_6 and checks the order-11 identity, lower bound, divisibility rounding, and elementary upper bound.",
  "relevance": "For Number of reduced Latin squares of order 12, record rls12-artifact-small-order-replay (“Exact small-order enumeration and order-12 arithmetic replay”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python enumerates R_2 through R_6 and checks the order-11 identity, lower bound, divisibility rounding, and elementary upper bound.",
  "relevance_source": "recorded",
  "body": "The row-by-row backtracker fixes the natural first row and first column. Bit masks enforce that every symbol occurs once per row and once per column. A minimum-remaining-values choice selects the next column inside each row. The complete searches reproduce \\(1,1,4,56,9408\\) for orders 2 through 6.\n\nThe same program checks \\(L_{11}=11!10!R_{11}\\), evaluates the van der Waerden rational lower bound with `Fraction`, rounds it upward, applies the published factor \\(6!\\), and computes \\((11!)^{11}\\). Its complete standard output has SHA-256 digest `8c167454c650bc023b4ea8f3c237fa06fb595ede7def12744d31b4e89ebc8696`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all reduced Latin squares of orders 2 through 6, the published order-11 normalization identity, and exact order-12 bound arithmetic",
    "bounds": {
      "enumerated_order": {
        "min": 2,
        "max": 6
      },
      "arithmetic_order": {
        "min": 11,
        "max": 12
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "save code as check.py and run python3 check.py",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.1007/s00026-005-0261-7",
      "locator": "Inline CPython standard-library replay written and executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": "from fractions import Fraction\nfrom hashlib import sha256\nfrom math import factorial\n\n\ndef count_reduced(n):\n    full = (1 << n) - 1\n    columns = [1 << column for column in range(n)]\n\n    def fill_rows(row):\n        if row == n:\n            return 1\n        fixed = 1 << row\n        columns[0] |= fixed\n        total = fill_row(row, fixed, tuple(range(1, n)))\n        columns[0] ^= fixed\n        return total\n\n    def fill_row(row, used, pending):\n        if not pending:\n            return fill_rows(row + 1)\n        best_column = None\n        best_available = 0\n        best_size = n + 1\n        for column in pending:\n            available = full & ~used & ~columns[column]\n            size = bin(available).count('1')\n            if size == 0:\n                return 0\n            if size < best_size:\n                best_column = column\n                best_available = available\n                best_size = size\n        rest = tuple(column for column in pending if column != best_column)\n        total = 0\n        available = best_available\n        while available:\n            bit = available & -available\n            available -= bit\n            columns[best_column] |= bit\n            total += fill_row(row, used | bit, rest)\n            columns[best_column] ^= bit\n        return total\n\n    return fill_rows(1)\n\nknown = {2: 1, 3: 1, 4: 4, 5: 56, 6: 9408}\nreplayed = {n: count_reduced(n) for n in known}\nassert replayed == known\nr11 = 5363937773277371298119673540771840\nl11 = 776966836171770144107444346734230682311065600000\nassert factorial(11) * factorial(10) * r11 == l11\nraw_lower = Fraction(factorial(12) ** 24, 12 ** 144 * factorial(12) * factorial(11))\nceiling = (raw_lower.numerator + raw_lower.denominator - 1) // raw_lower.denominator\nlower = ((ceiling + factorial(6) - 1) // factorial(6)) * factorial(6)\nupper = factorial(11) ** 11\nassert lower == 4410573106297854867267286926659737440\nassert upper == 409933016554924328182440935903164918932547530146724293451448320000000000000000000000\nlines = [\n    'reduced_counts=' + ','.join(str(n) + ':' + str(replayed[n]) for n in replayed),\n    'R11=' + str(r11),\n    'L11=' + str(l11),\n    'R12_vdw_ceiling=' + str(ceiling),\n    'R12_divisible_by=720',\n    'R12_rigorous_lower=' + str(lower),\n    'R12_elementary_upper=' + str(upper),\n]\nreport = '\\n'.join(lines) + '\\n'\nprint(report, end='')\nprint('report_sha256=' + sha256(report.encode()).hexdigest())\n",
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1007/s00026-005-0261-7",
    "locator": "Inline CPython standard-library replay written and executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R653",
      "title": "The order-11 exact count fixes the normalization",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "R655",
      "title": "A rigorous elementary bracket contains the estimate",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "reduced-latin-squares-order-12",
      "title": "reduced latin squares order 12",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}