{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R188",
  "content_hash": null,
  "slug": "cyclic315-claim-pair-incidence-upper-13",
  "type": "claim",
  "title": "Pair incidences give an upper bound of thirteen",
  "summary": "Every pair lies in at most nine developed blocks, which caps an unrestricted packing at 418 blocks and a full-orbit cyclic packing at thirteen base blocks.",
  "relevance": "For Largest cyclic 3-(31,5,1) packing, record cyclic315-claim-pair-incidence-upper-13 (“Pair incidences give an upper bound of thirteen”) records a bound, answer, status fact, or structural consequence. The record states: Every pair lies in at most nine developed blocks, which caps an unrestricted packing at 418 blocks and a full-orbit cyclic packing at thirteen base blocks.",
  "relevance_source": "recorded",
  "body": "Fix a pair of points. Exactly 29 triples contain it. A developed 5-block containing the pair uses the three triples obtained by adjoining one of its other points. Distinct packing blocks use disjoint triples, so the pair belongs to at most \\(\\lfloor29/3\\rfloor=9\\) blocks.\n\nIf the developed packing has \\(B\\) blocks, counting pair-block incidences gives\n\\[\n10B=B\\binom52\\leq9\\binom{31}{2}=4185,\n\\]\nhence \\(B\\leq418\\). Every translation orbit of a 5-subset has length 31: a nonzero translation generates the prime-order group, and an invariant subset would have size 0 or 31. A cyclic packing with \\(M\\) base blocks therefore has \\(B=31M\\). It follows that\n\\[\nM\\leq\\left\\lfloor\\frac{418}{31}\\right\\rfloor=13.\n\\]\nThis is the relevant Johnson-style bound with the orbit divisibility condition imposed.",
  "status": "established",
  "evidence_grade": "proved",
  "scope": {
    "kind": "universal",
    "statement": "every cyclic 3-(31,5,1) packing consisting of full translation orbits"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1016/j.disc.2011.11.039",
      "locator": "The general Johnson-Schonheim packing bound is stated as Proposition 1.1.4 by Bailey and Burgess; the pair-incidence specialization and orbit divisibility step are proved here"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/j.disc.2011.11.039",
    "locator": "The general Johnson-Schonheim packing bound is stated as Proposition 1.1.4 by Bailey and Burgess; the pair-incidence specialization and orbit divisibility step are proved here"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R186",
      "title": "The certified interval is 9 through 13 base blocks",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R184",
      "title": "Exact difference and orbit verifier",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "cyclic-315-packing-31",
      "title": "cyclic 315 packing 31",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}