{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R58",
  "content_hash": null,
  "slug": "bbmb-claim-mersenne-sharpness",
  "type": "claim",
  "title": "Every Mersenne input attains the proposed bound",
  "summary": "For every m at least 1, k(2^m-1)=2^(m-1)+1.",
  "relevance": "For Sharp multipliers for balanced binary products, record bbmb-claim-mersenne-sharpness (“Every Mersenne input attains the proposed bound”) records a bound, answer, status fact, or structural consequence. The record states: For every m at least 1, k(2^m-1)=2^(m-1)+1.",
  "relevance_source": "recorded",
  "body": "Fix \\(m\\geq1\\), put \\(n=2^m-1\\), and let \\(u=k-1\\). The identity\n\\[\nk(2^m-1)=u2^m+(2^m-1-u)\n\\]\nexpresses the product as two binary blocks of width \\(m\\): the padded \\(m\\)-bit expansion of \\(u\\), followed by its bitwise complement. The padded word has length \\(2m\\) and exactly \\(m\\) ones.\n\nIf \\(1\\leq k\\leq2^{m-1}\\), then \\(u<2^{m-1}\\). Its padded block begins with at least one zero. Ordinary binary notation removes those leading zeros while retaining all \\(m\\) ones in the two-block word. The resulting word has fewer than \\(2m\\) bits and still has \\(m\\) ones, so it is unbalanced.\n\nFor \\(k=2^{m-1}+1\\), one has \\(u=2^{m-1}\\). The first block now begins with 1, so the ordinary expansion has all \\(2m\\) bits. The two complementary blocks contain \\(m\\) ones in total, making the product balanced. Every smaller positive multiplier has already been excluded, which proves\n\\[\nk(2^m-1)=2^{m-1}+1.\n\\]\nThis proves the sharp family in the candidate and covers the forward direction of its equality statement.",
  "status": "supported",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "family",
    "statement": "every integer n=2^m-1 with m at least 1",
    "family": "Mersenne inputs n=2^m-1"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/1909.08849",
      "locator": "Complete elementary complement-block proof supplied in this record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1909.08849",
    "locator": "Complete elementary complement-block proof supplied in this record"
  },
  "models": [],
  "relations": [
    {
      "slug": "R59",
      "title": "The bound and equality characterization hold through 100 million",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "R56",
      "title": "A carry-free criterion reduces part of the search to popcounts",
      "object_type": "attempt",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "balanced-binary-multiplier-bound",
      "title": "balanced binary multiplier bound",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}