{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R67",
  "content_hash": null,
  "slug": "bdr1m-claim-cutoff-lower-bound",
  "type": "claim",
  "title": "A certified cutoff-scale coefficient gives a 16,113-digit lower bound",
  "summary": "The exact factorization of \\(\\binom{1000000}{499985}\\) gives a 16,113-digit divisor-count lower bound; no matching upper bound or complete sweep over \\(1\\le k<n\\le10^6\\) is recorded, so the exact maximum remains open.",
  "relevance": "For Most divisors of a binomial coefficient with top at most 10^6, record bdr1m-claim-cutoff-lower-bound (“A certified cutoff-scale coefficient gives a 16,113-digit lower bound”) records a bound, answer, status fact, or structural consequence. The record states: The exact factorization of \\(\\binom{1000000}{499985}\\) gives a 16,113-digit divisor-count lower bound; no matching upper bound or complete sweep over \\(1\\le k<n\\le10^6\\) is recorded, so the exact maximum remains open.",
  "relevance_source": "recorded",
  "body": "At the admissible pair\n\\[\n(n,k)=(1000000,499985),\n\\]\nthe coefficient has 53,478 distinct prime factors. Its exponent histogram is\n\\[\n(1:53413),(2:56),(3:3),(4:2),(5:2),(8:1),(12:1).\n\\]\nConsequently\n\\[\n\\max_{1\\leq k<n\\leq10^6}\\tau\\binom nk\n\\geq 2^{53413}3^{56}4^3 5^2 6^2\\cdot9\\cdot13.\n\\]\nThis exact integer has 16,113 decimal digits. Its first 64 digits are `2901061995181429015403180177031159054152063659198892515558624106`, its final 64 digits are `0248962087137382083803874069801496392268550388351507391473254400`, and its SHA-256 digest is `37e6b0aec8c146fa82e6e8d0eb776dbb1504fb2fff80e5fa74bff8eaddfee951`.\n\nFor complete factorization data, the artifact computes\n\\[\nv_p\\binom nk=\\sum_{j\\geq1}\\left(\\left\\lfloor\\frac n{p^j}\\right\\rfloor-\\left\\lfloor\\frac k{p^j}\\right\\rfloor-\\left\\lfloor\\frac{n-k}{p^j}\\right\\rfloor\\right)\n\\]\nfor every prime \\(p\\leq10^6\\). Joining the 53,478 nonzero pairs as ascending `p^e` terms gives SHA-256 digest `fb3db7328c0c940f68d88e873c6554c9ec65616c825f5b933fd2e55e492e1be2`. This certifies the lower bound without asserting that this pair is globally optimal.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "the single admissible pair (n,k)=(1000000,499985)",
    "bounds": {
      "n": {
        "min": 1000000,
        "max": 1000000
      },
      "k": {
        "min": 499985,
        "max": 499985
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1134/S0001434613010331",
      "locator": "Exact Legendre-valuation replay in bdr1m-artifact-factorization-replay"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1134/S0001434613010331",
    "locator": "Exact Legendre-valuation replay in bdr1m-artifact-factorization-replay"
  },
  "models": [],
  "relations": [
    {
      "slug": "R65",
      "title": "Legendre factorization and divisor-count replay",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "binomial-divisor-record-1e6",
      "title": "binomial divisor record 1e6",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}