TheoremDB
R584claimStatus: supportedEvidence: ReproducedReplay: source only

[#R584] The minimum tap weight lies between 8 and 186

claim. Exact replay proves feasibility at weight 186 and excludes every candidate of weight at most 7.

View evidenceOpen source ↗

1Summary

Write \[ v_j=(s_j,s_{j+1},\ldots,s_{j+423})\in\mathbf F_2^{424}. \] Since the endpoint coefficients are fixed at one, an internal tap set \(T\subseteq\{1,\ldots,599\}\) is feasible exactly when \[ \bigoplus_{j\in T}v_j=v_0\oplus v_{600}. \] The exact verifier forms all 599 internal columns and all 179,101 pairwise xor values. It tests internal subsets of sizes zero through four with singleton and pair tables. For size five, it checks all 35,641,099 triples against the pair table. If the two sides of one of these table identities share an index, cancellation gives a smaller solution already excluded. The sweep finds no solution with at most five internal taps. Every admissible vector has two endpoint taps, so its total weight is at least 8.

For the upper bound, interpret the hexadecimal integer ``` 104020000042401000000000000100000010004020001702093a81120945a122179a133c52f6f5d7860361026a5b18b00f8b704122171b46d22ccedce3191b108a19415c43e921a850ae209 ``` with coefficient \(c_j\) in bit \(j\), starting at the least significant bit. It has 601 bits, both endpoint bits are one, and its Hamming weight is 186. Exact substitution gives zero violations among all 424 recurrence equations.

Reproduced evidence. Recorded scope: the stated 601 binary coefficients, 424 recurrence equations, and prime-indicator prefix of length 1024.

2Evidence

Evidence package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: doi.org ↗, Exact standard-library computation in pirw600-artifact-subset-and-incumbent-certificate, executed on 2026-07-25

3Overview

Row reduction of the 424 recurrence rows together with the two endpoint rows gives rank 426 and affine dimension 175. The exact minimum inside the certified interval \[ 8\leq w_{\min}\leq186 \] remains open. A two-minute pseudo-Boolean solver probe at threshold 150 ended without a model or an unsatisfiability proof and contributes no further bound.

4What was measured

Certified lower bound
8
Certified upper bound
186
Exact optimum known
no
Constraint rank
426
Affine dimension
175
Incumbent encoding
coefficient c_j is bit j of the hexadecimal integer, with c_0 least significant
Incumbent hex
104020000042401000000000000100000010004020001702093a81120945a122179a133c52f6f5d7860361026a5b18b00f8b704122171b46d22ccedce3191b108a19415c43e921a850ae209

Uncertified probe

solverZ3 5.0.0threshold150timeout seconds2 minutesresultunknowninferencenone

5How it connects

Supported by

Contextualizes (incoming)

Recorded for

6Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R584",
  "content_hash": null,
  "slug": "pirw600-claim-certified-weight-interval",
  "type": "claim",
  "title": "The minimum tap weight lies between 8 and 186",
  "summary": "Exact replay proves feasibility at weight 186 and excludes every candidate of weight at most 7.",
  "relevance": "For Sparsest degree-600 recurrence for a prime-indicator prefix, record pirw600-claim-certified-weight-interval (“The minimum tap weight lies between 8 and 186”) records a bound, answer, status fact, or structural consequence. The record states: Exact replay proves feasibility at weight 186 and excludes every candidate of weight at most 7.",
  "relevance_source": "recorded",
  "body": "Write\n\\[\n v_j=(s_j,s_{j+1},\\ldots,s_{j+423})\\in\\mathbf F_2^{424}.\n\\]\nSince the endpoint coefficients are fixed at one, an internal tap set \\(T\\subseteq\\{1,\\ldots,599\\}\\) is feasible exactly when\n\\[\n \\bigoplus_{j\\in T}v_j=v_0\\oplus v_{600}.\n\\]\nThe exact verifier forms all 599 internal columns and all 179,101 pairwise xor values. It tests internal subsets of sizes zero through four with singleton and pair tables. For size five, it checks all 35,641,099 triples against the pair table. If the two sides of one of these table identities share an index, cancellation gives a smaller solution already excluded. The sweep finds no solution with at most five internal taps. Every admissible vector has two endpoint taps, so its total weight is at least 8.\n\nFor the upper bound, interpret the hexadecimal integer\n```\n104020000042401000000000000100000010004020001702093a81120945a122179a133c52f6f5d7860361026a5b18b00f8b704122171b46d22ccedce3191b108a19415c43e921a850ae209\n```\nwith coefficient \\(c_j\\) in bit \\(j\\), starting at the least significant bit. It has 601 bits, both endpoint bits are one, and its Hamming weight is 186. Exact substitution gives zero violations among all 424 recurrence equations.\n\nRow reduction of the 424 recurrence rows together with the two endpoint rows gives rank 426 and affine dimension 175. The exact minimum inside the certified interval\n\\[\n8\\leq w_{\\min}\\leq186\n\\]\nremains open. A two-minute pseudo-Boolean solver probe at threshold 150 ended without a model or an unsatisfiability proof and contributes no further bound.",
  "status": "supported",
  "evidence_grade": "computational",
  "scope": {
    "kind": "bounded",
    "statement": "the stated 601 binary coefficients, 424 recurrence equations, and prime-indicator prefix of length 1024",
    "bounds": {
      "degree": {
        "min": 600,
        "max": 600
      },
      "prefix_length": {
        "min": 1024,
        "max": 1024
      },
      "recurrence_equations": {
        "min": 424,
        "max": 424
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1109/TIT.1969.1054260",
      "locator": "Exact standard-library computation in pirw600-artifact-subset-and-incumbent-certificate, executed on 2026-07-25"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/TIT.1969.1054260",
    "locator": "Exact standard-library computation in pirw600-artifact-subset-and-incumbent-certificate, executed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R582",
      "title": "Exact lower-bound and incumbent replay certificate",
      "object_type": "artifact",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R583",
      "title": "The fixed-degree tap objective is a syndrome-decoding instance",
      "object_type": "attempt",
      "relation": "contextualizes",
      "direction": "incoming"
    },
    {
      "slug": "prime-indicator-recurrence-weight-600",
      "title": "prime indicator recurrence weight 600",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

7Provenance

View source, identifiers, and projection details
Project
prime-indicator-recurrence-weight-600
Locator
Exact standard-library computation in pirw600-artifact-subset-and-incumbent-certificate, executed on 2026-07-25
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R584
Stable alias
pirw600-claim-certified-weight-interval
Projection
Reproduction fields are derived from the immutable record.

A statement this project treats as settled at the recorded evidence grade, with the work that backs it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.