{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R834",
  "content_hash": null,
  "slug": "wfci127-claim-complement-upper-bound",
  "type": "claim",
  "title": "Every inverse has weight at most 101",
  "summary": "The complement of an inverse must have at least 26 nonzero coefficients.",
  "relevance": "For Densest inverse of a weight-five binary cyclic polynomial, record wfci127-claim-complement-upper-bound (“Every inverse has weight at most 101”) records a bound, answer, status fact, or structural consequence. The record states: The complement of an inverse must have at least 26 nonzero coefficients.",
  "relevance_source": "recorded",
  "body": "Write\n\\[\nJ=1+x+\\cdots+x^{126}.\n\\]\nFor every weight-five \\(f\\), cyclic multiplication gives \\(fJ=J\\), because each coefficient of \\(fJ\\) is the parity of five. Suppose \\(fg=1\\), and set \\(h=J+g\\). Then\n\\[\nfh=fJ+fg=J+1,\n\\]\nwhose weight is 126.\n\nIf \\(t=\\operatorname{wt}(h)\\), the product \\(fh\\) is the xor of \\(t\\) cyclic shifts of the five-term polynomial \\(f\\). Hence\n\\[\n126=\\operatorname{wt}(fh)\\leq5t,\n\\]\nso \\(t\\geq26\\). Also \\(f(1)=1\\) and \\(fg=1\\) imply \\(g(1)=1\\), making \\(\\operatorname{wt}(g)\\) odd and \\(t=127-\\operatorname{wt}(g)\\) even. It follows that\n\\[\n\\operatorname{wt}(g)=127-t\\leq101.\n\\]\nFor the weight-85 witness, \\(h\\) has weight 42 and the verifier checks \\(fh=J+1\\) exactly.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "every invertible weight-five residue in F_2[x]/(x^127+1)"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://eprint.iacr.org/2012/409",
      "locator": "Elementary cyclic-convolution proof and exact witness replay in this fixture, 2026-07-25"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://eprint.iacr.org/2012/409",
    "locator": "Elementary cyclic-convolution proof and exact witness replay in this fixture, 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R833",
      "title": "The maximum inverse weight lies between 85 and 101",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "weight-five-cyclic-inverse-127",
      "title": "weight five cyclic inverse 127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}