{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R754",
  "content_hash": null,
  "slug": "ssm34-claim-pfaffian-rounded-upper-bound",
  "type": "claim",
  "title": "Every determinant is at most 6,876,227,375,063^2",
  "summary": "The general order 2 modulo 4 bound gives 65 times 31^16, and the odd-square constraint rounds it down.",
  "relevance": "For Maximum determinant of a skew Seidel matrix of order 34, record ssm34-claim-pfaffian-rounded-upper-bound (“Every determinant is at most 6,876,227,375,063^2”) records a bound, answer, status fact, or structural consequence. The record states: The general order 2 modulo 4 bound gives 65 times 31^16, and the odd-square constraint rounds it down.",
  "relevance_source": "recorded",
  "body": "Klanderman et al. define \\(M(n)=\\max\\sqrt{\\det S}\\). Their Theorem 5.4, which collects the skew Ehlich-Wojtas result, gives\n\\[\nM(n)\\leq\\sqrt{2n-3}\\,(n-3)^{(n-2)/4}\n\\]\nwhen \\(n\\equiv2\\pmod4\\). At \\(n=34\\), this says\n\\[\n\\det S\\leq65\\,31^{16}\n =47{,}282{,}502{,}913{,}567{,}042{,}148{,}851{,}265.\n\\]\nCayley's Pfaffian identity says \\(\\det S=\\operatorname{pf}(S)^2\\), and parity makes the Pfaffian odd. Exact integer square root gives\n\\[\n\\left\\lfloor\\sqrt{65\\,31^{16}}\\right\\rfloor\n =6{,}876{,}227{,}375{,}063.\n\\]\nThis integer is odd, while the next odd integer already has square larger than \\(65\\,31^{16}\\). Hence every admissible determinant is at most\n\\[\n6{,}876{,}227{,}375{,}063^2\n =47{,}282{,}502{,}913{,}565{,}795{,}274{,}253{,}969.\n\\]\nThe equality form in the unrounded bound would require \\(2n-3\\) to be a square. Here \\(65\\) is not a square, which independently rules out equality in that real-valued bound.",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "every 34 by 34 skew Seidel matrix",
    "bounds": {
      "matrix_order": {
        "min": 34,
        "max": 34
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/2406.09697",
      "locator": "Klanderman et al., Theorem 5.4(a,d); Greaves and Suda, arXiv:1601.02769, Theorem 1.1 and the skew EW matrix discussion; Cayley's Pfaffian identity"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2406.09697",
    "locator": "Klanderman et al., Theorem 5.4(a,d); Greaves and Suda, arXiv:1601.02769, Theorem 1.1 and the skew EW matrix discussion; Cayley's Pfaffian identity"
  },
  "relations": [
    {
      "slug": "R752",
      "title": "The maximum is between 35^16 and 6,876,227,375,063^2",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "skew-seidel-maxdet-34",
      "title": "skew seidel maxdet 34",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}