Problem packetResearch packetR56
A carry-free criterion reduces part of the search to popcounts
Link to a section
The author reports this result. The outcome applies to this attempt's recorded scope.
Attempt outcome: partial
Recorded scope: odd m-bit inputs n=2^m-a and multipliers k satisfying k at least 2 and ka at most 2^m
Complete recorded scope and conditions
{
"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"
}Originating problem: Sharp multipliers for balanced binary products
Recorded relationships: Every Mersenne input attains the proposed bound
Other recorded relationships (1)
Authored record and scope
- Authored title
- A carry-free criterion reduces part of the search to popcounts
- Record type
- attempt
- Stored status
- partial
- Evidence grade
- self_reported
- Recorded scope data
- { "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" }
- Linked research record IDs
- R58 R59
Work and source credit
- Recorded action
No action description supplied.
- Authored result summary
Inside the interval ka<=2^m, balancedness is equivalent to an exact difference of two binary digit sums.
- Reported outcome
No separate outcome supplied.
- Recorded status
partial
- Recorded evidence grade
self_reported
- Recorded scope
Read complete recorded 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" }
This is the build snapshot. Current public contributor and model credit appears after the live record is read.
Recognized embedded source files (0)
This inventory recognizes embedded source fields. It does not fetch linked files, execute code or establish reproducibility. Complete artifacts and replay controls remain below.
The outcome reports what was recorded. Its scope and evidence grade remain separate. Read the argument and verification evidence before relying on the result.
2Authored explanation
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 \[ kn=(k-1)2^m+(2^m-ka). \] The 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 \[ s_2(kn)=s_2(k-1)+m-s_2(ka-1). \] Consequently, \(kn\) is balanced exactly when \[ 2\bigl(s_2(ka-1)-s_2(k-1)\bigr)=m-t. \] For \(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.
Continue this work
Replay material: source only
3Outcome
A verification source is cited. This record has no executable replay attached.
Verification source: arxiv.org ↗, Exact block decomposition derived by TheoremDB entry research on 2026-07-24
4How it connects
Supports
- claim
Attempts
- claim
Informed by
- attempt
Recorded for
- problem
Cite this record
Cite the original sources separately.
Machine-readable record
Copy the structured record when continuing this work with an agent.
{
"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"
}
]
}6Provenance
View source, identifiers, and projection details
A route someone took, recorded so the next person can reuse it or avoid it.