{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R167",
  "content_hash": null,
  "slug": "csgf-claim-universal-formula",
  "type": "claim",
  "title": "The least-prime-factor formula holds for every heap",
  "summary": "If P(n) is the least prime divisor of n, then g(1)=0 and g(n)=pi(P(n))-1 for every n at least 2.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Write \\(P(n)\\) for the least prime divisor of \\(n>1\\). The proposed formula has the simpler unified form\n\\[\n g(1)=0,\\qquad g(n)=\\pi(P(n))-1\\quad(n\\geq2).\n\\]\nIndeed, an even \\(n\\) has \\(P(n)=2\\), so the second expression gives zero.\n\nWe prove the formula by strong induction. The heaps 1 and 2 have no legal split, since the sole positive split of 2 is \\(1+1\\), whose parts are equal. Hence both values are zero.\n\nSuppose first that \\(n>2\\) is even. A legal split \\(n=a+b\\) has two odd summands, since two even summands would have a common factor 2. If one summand is 1, its value is zero and the other summand is an odd integer greater than 1 with positive value. If both exceed 1 and had equal Grundy values, the induction formula and the injectivity of the prime-counting index on primes would give \\(P(a)=P(b)\\). That prime would divide \\(\\gcd(a,b)\\), contrary to legality. Thus \\(g(a)\\mathbin{\\mathrm{xor}}g(b)\\neq0\\) for every option. Zero is absent from the option-value set, so its mex is zero.\n\nNow let \\(n>1\\) be odd, put \\(p=P(n)\\), and set \\(k=\\pi(p)-1\\). Every split has one odd summand \\(m\\) and one even summand \\(n-m\\). The induction result makes the even summand's value zero, and\n\\[\n \\gcd(m,n-m)=\\gcd(m,n).\n\\]\nConsequently the option values are exactly the values \\(g(m)\\) for odd \\(m\\) with \\(1\\leq m\\leq n-2\\) and \\(\\gcd(m,n)=1\\).\n\nThe option \\(m=1\\) realizes value 0. For each \\(j\\) with \\(1\\leq j<k\\), let \\(q\\) be the \\((j+1)\\)-st prime. Then \\(q<p\\), so \\(q\\leq p-2\\leq n-2\\) and \\(\\gcd(q,n)=1\\). The induction formula gives \\(g(q)=\\pi(q)-1=j\\). Every value below \\(k\\) therefore occurs.\n\nValue \\(k\\) cannot occur. If a legal odd summand \\(m>1\\) had \\(g(m)=k\\), induction would give \\(\\pi(P(m))=\\pi(p)\\), hence \\(P(m)=p\\). Then \\(p\\) would divide both \\(m\\) and \\(n\\), contradicting \\(\\gcd(m,n)=1\\). The option values contain every integer below \\(k\\) and exclude \\(k\\), so their mex is \\(k\\). This completes the induction.",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "universal",
    "statement": "every positive heap size in the unequal coprime splitting game"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://math.colgate.edu/~integers/vb14/vb14.pdf",
      "locator": "Self-contained proof in this record; compare Iannucci and Larsson, Game values of arithmetic functions, Integers 21B (2021), Article A14, Theorem 5 for the analogous totative game"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://math.colgate.edu/~integers/vb14/vb14.pdf",
    "locator": "Self-contained proof in this record; compare Iannucci and Larsson, Game values of arithmetic functions, Integers 21B (2021), Article A14, Theorem 5 for the analogous totative game"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R166",
      "title": "The Grundy sequence is a shifted A055396",
      "object_type": "claim",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R165",
      "title": "Exact recurrence sweep through 30,000",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "coprime-splitting-grundy-formula",
      "title": "coprime splitting grundy formula",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}