{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R197",
  "content_hash": null,
  "slug": "dclp-artifact-integer-prefix-certificate",
  "type": "artifact",
  "title": "Exact scaled-integer coefficient certificate",
  "summary": "A standard-library Python program expands the product with a common factorial denominator and checks every adjacent pair.",
  "relevance": "For Eventual decrease for distinct cycle lengths in random permutations, record dclp-artifact-integer-prefix-certificate (“Exact scaled-integer coefficient certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program expands the product with a common factorial denominator and checks every adjacent pair.",
  "relevance_source": "recorded",
  "body": "The program uses \\(D=5000!\\) as a common denominator. Its descending updates are exact divisions because each intermediate summand corresponds to a distinct-part set whose denominator divides \\(D\\). A reproduced run reports `exact_checked_through=5000 last_nondecrease_n=30`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all coefficients and adjacent comparisons through degree 5000",
    "bounds": {
      "degree": {
        "min": 0,
        "max": 5000
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "runnable",
    "kind": "inline_python_computation",
    "command": "python3 certificate.py",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://oeis.org/A007838",
      "locator": "Self-contained Python standard-library certificate reproduced by TheoremDB entry research on 2026-07-24"
    },
    "dependencies": "Python standard library only",
    "runtime_seconds": 33.74,
    "inline_source": "from math import factorial\nN = 5000\nD = factorial(N)\nc = [0] * (N + 1)\nc[0] = D\nfor k in range(1, N + 1):\n    for n in range(N, k - 1, -1):\n        quotient, remainder = divmod(c[n - k], k)\n        assert remainder == 0\n        c[n] += quotient\nnondecrease = [n for n in range(1, N + 1) if c[n] >= c[n - 1]]\nassert nondecrease[-1] == 30\nassert c[30] > c[29]\nassert all(c[n] < c[n - 1] for n in range(31, N + 1))\nprint(f'exact_checked_through={N} last_nondecrease_n={nondecrease[-1]}')",
    "missing": [
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://oeis.org/A007838",
    "locator": "Self-contained Python standard-library certificate reproduced by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R200",
      "title": "Strict decrease holds exactly through n=5000",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "distinct-cycle-length-probability-decreasing",
      "title": "distinct cycle length probability decreasing",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}