{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R454",
  "content_hash": null,
  "slug": "levine-claim-borel-value-equals-finite-limit",
  "type": "claim",
  "title": "Borel infinite-stack strategies have the same supremum as finite-stack strategies",
  "summary": "The supremum over Borel strategies equals the increasing limit of the finite-stack optima, so the coin formulation and the standard Levine value use the same convention.",
  "relevance": "For The value of Levine's two-player coin-index game, record levine-claim-borel-value-equals-finite-limit (“Borel infinite-stack strategies have the same supremum as finite-stack strategies”) records a bound, answer, status fact, or structural consequence. The record states: The supremum over Borel strategies equals the increasing limit of the finite-stack optima, so the coin formulation and the standard Levine value use the same convention.",
  "relevance_source": "recorded",
  "body": "Let \\(\\Omega=\\{0,1\\}^{\\mathbb N_{>0}}\\) carry its fair product measure, and let \\(V_h\\) be the optimum when both strategies read the first \\(h\\) bits and output an index in \\(\\{1,\\ldots,h\\}\\). The sequence \\(V_h\\) is nondecreasing because a strategy may ignore extra bits and indices.\n\nHere is a direct approximation argument for the reverse comparison. If \\(f:\\Omega\\to\\mathbb N_{>0}\\) is Borel and \\(\\varepsilon>0\\), choose \\(M\\) so that \\(\\Pr(f>M)<\\varepsilon\\). The finite measurable partition formed by the fibers \\(f^{-1}(1),\\ldots,f^{-1}(M)\\), together with the tail, can be approximated in measure by a partition measurable with respect to the first \\(d\\) coordinates. Equivalently, finite-coordinate simple maps are dense in probability among measurable maps to a countable discrete space. This gives a map \\(f_{d,M}\\), depending on the first \\(d\\) bits and taking values at most \\(M\\), with \\(\\Pr(f_{d,M}\\ne f)<2\\varepsilon\\). For \\(h\\ge\\max(d,M)\\), it is an \\(h\\)-strategy.\n\nApply this construction to both members \\(f,g\\) of a Borel strategy pair. The two win indicators can differ only on the event where at least one approximating strategy differs from its target, so their winning probabilities differ by at most the sum of the two mismatch probabilities. Every Borel pair can therefore be approximated arbitrarily closely by finite strategies. Conversely, every finite strategy is Borel. Hence\n\\[\n\\sup_{f,g\\ {\rm Borel}}\\Pr\\bigl(A_{g(B)}=B_{f(A)}=1\\bigr)\n=\\lim_{h\\to\\infty}V_h.\n\\]\nThis independently supplies the cylinder-approximation step for Borel fibers that may have empty interior.",
  "status": "supported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "universal",
    "statement": "all pairs of Borel maps from the fair-bit product space to the positive integers"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/2508.01737",
      "locator": "Bouquet et al., Sections 2.1-2.2, Lemmas 6-9, and Theorem 10"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2508.01737",
    "locator": "Bouquet et al., Sections 2.1-2.2, Lemmas 6-9, and Theorem 10"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R455",
      "title": "The checked interval is 7/20 through 81/224, and equality at 7/20 remains open",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R451",
      "title": "The 2026 source audit retains the exact two-player value as an open conjecture",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "levine-two-player-seven-twentieths",
      "title": "levine two player seven twentieths",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}