{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R47",
  "content_hash": null,
  "slug": "b2z100-claim-certified-interval-13-14",
  "type": "claim",
  "title": "The certified maximum lies between 13 and 14",
  "summary": "The current certified interval is 13 <= M <= 14: an explicit 13-set passes all 99 difference checks, and ordered-pair counting rules out size 15. Whether a valid 14-set exists remains unresolved.",
  "relevance": "For Existence of a fourteen-point two-fold difference packing modulo 100, record b2z100-claim-certified-interval-13-14 (“The certified maximum lies between 13 and 14”) records a bound, answer, status fact, or structural consequence. The record states: The current certified interval is 13 <= M <= 14: an explicit 13-set passes all 99 difference checks, and ordered-pair counting rules out size 15.",
  "relevance_source": "recorded",
  "body": "Let \\(M\\) be the largest size of a subset with the stated property. The current certified bounds are\n\\[\n\\boxed{13\\leq M\\leq14}.\n\\]\nThe lower bound is attained by\n\\[\nA=\\{8,13,18,28,29,47,68,71,82,83,91,95,99\\}.\n\\]\nFor this set, the 99 nonzero ordered-difference multiplicities have histogram\n\\[\n12\\text{ zeros},\\qquad18\\text{ ones},\\qquad69\\text{ twos}.\n\\]\nTheir sum is \\(13\\cdot12=156\\), and their maximum is two. The executable record checks every ordered pair directly. It also checks that adjoining any of the other 87 residues violates the bound, so this particular 13-set is inclusion-maximal.\n\nFor the upper bound, a \\(k\\)-set has \\(k(k-1)\\) ordered pairs of distinct elements. All of their differences lie in the 99 nonzero residues, each with capacity two. Hence\n\\[\nk(k-1)\\leq2\\cdot99=198.\n\\]\nSince \\(15\\cdot14=210\\), one has \\(k\\leq14\\). This counting proof leaves the candidate size 14 undecided.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "subsets of the cyclic group Z/100Z under the ordered nonzero-difference multiplicity bound two",
    "bounds": {
      "modulus": {
        "min": 100,
        "max": 100
      },
      "multiplicity": {
        "min": 2,
        "max": 2
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1109/18.30982",
      "locator": "Direct ordered-difference count and exhaustive verification in b2z100-artifact-verifier-and-ilp"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/18.30982",
    "locator": "Direct ordered-difference count and exhaustive verification in b2z100-artifact-verifier-and-ilp"
  },
  "models": [],
  "relations": [
    {
      "slug": "R44",
      "title": "Exact difference verifier and complete size-14 feasibility model",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "R45",
      "title": "Bounded local searches reached one circular-distance violation",
      "object_type": "attempt",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R46",
      "title": "The problem is a one-codeword optical autocorrelation problem",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "b2-two-set-z100",
      "title": "b2 two set z100",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}