{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R857",
  "content_hash": null,
  "slug": "zsf7s-attempt-literature-and-fourteen-point-search",
  "type": "attempt",
  "title": "Three symmetry cases remain in the 14-point search",
  "summary": "Two of five second-point orbits returned UNSAT, while the timebox ended before three cases were certified.",
  "relevance": "For Zero-sum-free subsets of the unit sphere over F_7, record zsf7s-attempt-literature-and-fourteen-point-search (“Three symmetry cases remain in the 14-point search”) documents a concrete method, search boundary, or failed route. The record states: Two of five second-point orbits returned UNSAT, while the timebox ended before three cases were certified.",
  "relevance_source": "recorded",
  "body": "A focused literature audit located the general zero-sum-free-set framework and the exact p-group Davenport constant, but no result for this 42-point quadratic sphere. Ordaz, Philipp, Santos, and Schmid define the small Olson constant and survey exact cases. Their exact elementary p-group results cover rank at most two and other parameter ranges. Pohoata and Zakharov treat \\(\\mathbb F_p^d\\) asymptotically for fixed dimension and large primes. Neither source determines this restricted instance at \\(p=7,d=3\\).\n\nThe timeboxed feasibility search used one Boolean selection variable \\(x_i\\) for each sphere point and reachability variables \\(r_{i,s}\\) for subset sums after the first \\(i\\) points. Its exact recurrence was\n\\[\nr_{i,s}\\longleftrightarrow r_{i-1,s}\\vee(x_i\\wedge r_{i-1,s-v_i}),\n\\]\nwith only \\(r_{0,0}\\) true. The clause \\(\\neg x_i\\vee\\neg r_{i-1,-v_i}\\) prevents a newly selected point from closing a zero sum, and a cardinality constraint imposes \\(\\sum_i x_i=14\\).\n\nOrthogonal symmetry sends a selected unit vector to \\((0,0,1)\\). Its stabilizer has five orbits on permissible second points, indexed by their last coordinate \\(0,2,3,4,5\\). Z3 returned UNSAT for representatives \\((0,1,0)\\) and \\((0,2,2)\\), in 29.684 and 33.485 seconds. The remaining three runs were interrupted to keep the research bounded. No solver proof artifact was retained, so these observations do not improve the certified upper bound of 18.\n\nA complete continuation should run the same finite-state encoding on the last three orbits and retain independently checkable unsatisfiability proofs. If any case is satisfiable, its model supplies a 14-point construction. If all three are unsatisfiable and the two completed cases are rerun with proof logging, the result proves that 13 is exact.",
  "status": "inconclusive",
  "evidence_grade": "computed",
  "scope": {
    "kind": "bounded",
    "statement": "published zero-sum results relevant to F_7^3 and a timeboxed symmetry-reduced feasibility search for a 14-point spherical set",
    "bounds": {
      "field_order": {
        "min": 7,
        "max": 7
      },
      "target_cardinality": {
        "min": 14,
        "max": 14
      },
      "stabilizer_orbits": {
        "min": 5,
        "max": 5
      },
      "completed_orbits": {
        "min": 2,
        "max": 2
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://arxiv.org/abs/2009.08846",
      "locator": "Cosmin Pohoata and Dmitriy Zakharov, Zero subsums in vector spaces over finite fields, Journal of the London Mathematical Society 104 (2021), 1113-1139; Oscar Ordaz, Andreas Philipp, Irene Santos, and Wolfgang A. Schmid, On the Olson and the Strong Davenport constants, Journal de Théorie des Nombres de Bordeaux 23 (2011), 715-750; timeboxed Z3 4.15.4 search on 2026-07-25"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2009.08846",
    "locator": "Cosmin Pohoata and Dmitriy Zakharov, Zero subsums in vector spaces over finite fields, Journal of the London Mathematical Society 104 (2021), 1113-1139; Oscar Ordaz, Andreas Philipp, Irene Santos, and Wolfgang A. Schmid, On the Olson and the Strong Davenport constants, Journal de Théorie des Nombres de Bordeaux 23 (2011), 715-750; timeboxed Z3 4.15.4 search on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R858",
      "title": "The certified interval is 13 to 18",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "zero-sum-free-f7-sphere",
      "title": "zero sum free f7 sphere",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}