{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R859",
  "content_hash": null,
  "slug": "zsf7s-claim-witness-is-inclusion-maximal",
  "type": "claim",
  "title": "The 13-point witness is inclusion-maximal",
  "summary": "Its nonempty subset sums cover all 342 nonzero vectors of F_7^3.",
  "relevance": "For Zero-sum-free subsets of the unit sphere over F_7, record zsf7s-claim-witness-is-inclusion-maximal (“The 13-point witness is inclusion-maximal”) records a bound, answer, status fact, or structural consequence. The record states: Its nonempty subset sums cover all 342 nonzero vectors of F_7^3.",
  "relevance_source": "recorded",
  "body": "The 8191 nonempty subsets of \\(A\\) produce every member of \\(\\mathbb F_7^3\\setminus\\{0\\}\\) and never produce zero. For any \\(v\\in\\mathbb F_7^3\\setminus A\\) with \\(v\\ne0\\), some nonempty subset of \\(A\\) sums to \\(-v\\). Adjoining \\(v\\) then creates a zero-sum subset. Thus the witness cannot be enlarged, even when new points may be chosen outside the sphere. This maximality property concerns the displayed witness. It does not prove that every zero-sum-free spherical set has at most 13 points.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "the displayed 13-point subset of the unit sphere in F_7^3",
    "bounds": {
      "cardinality": {
        "min": 13,
        "max": 13
      },
      "nonzero_group_elements": {
        "min": 342,
        "max": 342
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1016/0022-314X(69)90021-3",
      "locator": "Exact subset-sum image computed by zsf7s-artifact-thirteen-point-verifier"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/0022-314X(69)90021-3",
    "locator": "Exact subset-sum image computed by zsf7s-artifact-thirteen-point-verifier"
  },
  "models": [],
  "relations": [
    {
      "slug": "R856",
      "title": "Exhaustive verifier for the 13-point construction",
      "object_type": "artifact",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "zero-sum-free-f7-sphere",
      "title": "zero sum free f7 sphere",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}