{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R336",
  "content_hash": null,
  "slug": "gocb-claim-infinite-injective",
  "type": "claim",
  "title": "The recurrence always has a next term",
  "summary": "Every current term has infinitely many eligible neighbors, so the construction gives an infinite sequence of distinct integers.",
  "relevance": "For Does the greedy one-common-bit sequence visit every positive integer?, record gocb-claim-infinite-injective (“The recurrence always has a next term”) records a bound, answer, status fact, or structural consequence. The record states: Every current term has infinitely many eligible neighbors, so the construction gives an infinite sequence of distinct integers.",
  "relevance_source": "recorded",
  "body": "Let \\(x\\) be the current term and choose a set bit \\(2^j\\) of \\(x\\). For every bit position \\(k\\) outside the support of \\(x\\), the integer\n\\[\ny=2^j+2^k\n\\]\nshares exactly the bit \\(2^j\\) with \\(x\\). There are infinitely many choices of \\(k\\), while only finitely many integers have been used at any finite stage. An unused eligible \\(y\\) therefore exists, and the well-ordering of the positive integers supplies the least one. The recurrence continues forever. Its explicit unused condition also makes all terms distinct.\n\nThis argument settles nontermination and injectivity. Surjectivity requires a separate argument.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "every finite stage of the greedy recurrence"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://oeis.org/A226077",
      "locator": "Elementary direct proof recorded and checked for this entry on 2026-07-24"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://oeis.org/A226077",
    "locator": "Elementary direct proof recorded and checked for this entry on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R334",
      "title": "The universal permutation claim remains open in the sources checked",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "greedy-one-common-bit-permutation",
      "title": "greedy one common bit permutation",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}