{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R56",
  "content_hash": null,
  "slug": "bbmb-attempt-complement-carry-criterion",
  "type": "attempt",
  "title": "A carry-free criterion reduces part of the search to popcounts",
  "summary": "Inside the interval ka<=2^m, balancedness is equivalent to an exact difference of two binary digit sums.",
  "relevance": "For Sharp multipliers for balanced binary products, record bbmb-attempt-complement-carry-criterion (“A carry-free criterion reduces part of the search to popcounts”) documents a concrete method, search boundary, or failed route. The record states: Inside the interval ka<=2^m, balancedness is equivalent to an exact difference of two binary digit sums.",
  "relevance_source": "recorded",
  "body": "Write an odd \\(m\\)-bit input as \\(n=2^m-a\\), where \\(a\\) is odd. For \\(k\\geq2\\) with \\(ka\\leq2^m\\), direct subtraction gives\n\\[\nkn=(k-1)2^m+(2^m-ka).\n\\]\nThe low block is the \\(m\\)-bit complement of \\(ka-1\\). Put \\(t=\\operatorname{bitlength}(k-1)\\) and let \\(s_2\\) denote popcount. The ordinary product has \\(m+t\\) bits and\n\\[\ns_2(kn)=s_2(k-1)+m-s_2(ka-1).\n\\]\nConsequently, \\(kn\\) is balanced exactly when\n\\[\n2\\bigl(s_2(ka-1)-s_2(k-1)\\bigr)=m-t.\n\\]\nFor \\(a=1\\), the two popcounts agree and the criterion yields the Mersenne proof. For general odd \\(a\\), the digit-sum difference has no monotonicity that would force a solution before \\(2^{m-1}+1\\). Multipliers with \\(ka>2^m\\) also introduce a quotient carry into the high block. These two gaps prevent this criterion from proving the universal claim.",
  "status": "partial",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "family",
    "statement": "odd m-bit inputs n=2^m-a and multipliers k satisfying k at least 2 and ka at most 2^m",
    "family": "the carry-free complement-block interval for n=2^m-a"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://arxiv.org/abs/1909.08849",
      "locator": "Exact block decomposition derived by TheoremDB entry research on 2026-07-24"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1909.08849",
    "locator": "Exact block decomposition derived by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R58",
      "title": "Every Mersenne input attains the proposed bound",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R59",
      "title": "The bound and equality characterization hold through 100 million",
      "object_type": "claim",
      "relation": "attempts",
      "direction": "outgoing"
    },
    {
      "slug": "R57",
      "title": "The focused literature search found broader digit-sum results",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "balanced-binary-multiplier-bound",
      "title": "balanced binary multiplier bound",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}