{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R655",
  "content_hash": null,
  "slug": "rls12-claim-rigorous-bracket",
  "type": "claim",
  "title": "A rigorous elementary bracket contains the estimate",
  "summary": "Published lower and divisibility theorems plus a direct row-choice bound give 4410573106297854867267286926659737440 <= R_12 <= (11!)^11.",
  "relevance": "For Number of reduced Latin squares of order 12, record rls12-claim-rigorous-bracket (“A rigorous elementary bracket contains the estimate”) records a bound, answer, status fact, or structural consequence. The record states: Published lower and divisibility theorems plus a direct row-choice bound give 4410573106297854867267286926659737440 <= R_12 <= (11!)^11.",
  "relevance_source": "recorded",
  "body": "The standard van der Waerden permanent bound quoted by McKay and Wanless gives\n\\[\nL_n\\ge\\frac{(n!)^{2n}}{n^{n^2}}.\n\\]\nAfter dividing by \\(12!11!\\), the order-12 reduced count is at least the ceiling of the resulting rational number:\n\\[\nR_{12}\\ge4410573106297854867267286926659737034.\n\\]\nTheir Theorem 2 also proves that \\(R_{2m}\\) is divisible by \\(m!\\). Thus \\(R_{12}\\) is divisible by \\(6!=720\\), and rounding the preceding lower bound to the next multiple gives\n\\[\nR_{12}\\ge4410573106297854867267286926659737440.\n\\]\nFor an elementary upper bound, fix the first row and column. Each of the remaining 11 rows has at most \\(11!\\) possible fillings once its first entry is fixed. Ignoring the column restrictions can only increase the count, so\n\\[\nR_{12}\\le(11!)^{11}=409933016554924328182440935903164918932547530146724293451448320000000000000000000000.\n\\]\nThe published estimate \\(1.62\\times10^{44}\\) lies inside this broad rigorous interval.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "all reduced Latin squares of order 12",
    "bounds": {
      "order": {
        "min": 12,
        "max": 12
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1007/s00026-005-0261-7",
      "locator": "McKay and Wanless, On the Number of Latin Squares, Theorem 2 and the standard lower bound quoted in Section 7; arithmetic replayed in rls12-artifact-small-order-replay"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1007/s00026-005-0261-7",
    "locator": "McKay and Wanless, On the Number of Latin Squares, Theorem 2 and the standard lower bound quoted in Section 7; arithmetic replayed in rls12-artifact-small-order-replay"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R651",
      "title": "Exact small-order enumeration and order-12 arithmetic replay",
      "object_type": "artifact",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R652",
      "title": "The exact enumeration record ends at order 11",
      "object_type": "claim",
      "relation": "bounds",
      "direction": "outgoing"
    },
    {
      "slug": "reduced-latin-squares-order-12",
      "title": "reduced latin squares order 12",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}