{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R702",
  "content_hash": null,
  "slug": "sat-claim-density-zero",
  "type": "claim",
  "title": "Subtract-a-triangular losing positions have density zero",
  "summary": "The losing positions contain no pair at a positive triangular difference, so polynomial Szemerédi gives upper Banach density zero.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Let \\(P\\) be the set of losing positions. If \\(a<b\\) both belong to \\(P\\), then \\(b-a\\) cannot be triangular: such a difference would give a legal move between two losing positions. Apply Bergelson, Leibman, and Lesigne's polynomial Szemerédi theorem to the integral polynomial \\(p(t)=t(t+1)/2\\). Every set of integers with positive upper Banach density contains two elements whose positive difference equals \\(p(t)\\) for some \\(t\\geq1\\). Therefore \\(P\\) has upper Banach density zero. Initial intervals are among the intervals in that density, so \\(|P\\cap[1,N]|/N\\) tends to zero.\n\nThis settles the database question. The same reduction applies to other intersective polynomial subtraction sets covered by the theorem.",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "universal",
    "statement": "the full set of losing positions in the normal-play subtract-a-triangular-number game"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/0710.4862",
      "locator": "Bergelson, Leibman, and Lesigne, Intersective polynomials and the polynomial Szemerédi theorem, Theorem 1.3"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/0710.4862",
    "locator": "Bergelson, Leibman, and Lesigne, Intersective polynomials and the polynomial Szemerédi theorem, Theorem 1.3"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R703",
      "title": "The losing positions are OEIS A030194",
      "object_type": "claim",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R700",
      "title": "Exact subtract-a-triangular sweep through 200,000",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R701",
      "title": "Determine the growth order of the triangular-game P-positions",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "subtract-a-triangular-density",
      "title": "subtract a triangular density",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}