{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R184",
  "content_hash": null,
  "slug": "cyclic315-artifact-exact-verifier",
  "type": "artifact",
  "title": "Exact difference and orbit verifier",
  "summary": "Standard-library Python develops the construction, checks every triple, enumerates the complete orbit-level search space, and replays the upper bound.",
  "relevance": "For Largest cyclic 3-(31,5,1) packing, record cyclic315-artifact-exact-verifier (“Exact difference and orbit verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python develops the construction, checks every triple, enumerates the complete orbit-level search space, and replays the upper bound.",
  "relevance_source": "recorded",
  "body": "The program uses exact integer and set arithmetic. It develops all nine base blocks, rejects any duplicate developed block or triple, and canonicalizes translation orbits by trying every point as the translate sent to zero. It also enumerates all 5,481 translation orbits of 5-subsets. Exactly 4,761 are internally admissible because their ten triples lie in ten distinct triple orbits. These are the columns of the finite set-packing formulation over 145 triple orbits.\n\nThe enumeration scopes a future exact search. It does not certify infeasibility for ten through thirteen base blocks. The pair-incidence proof supplies the certified upper endpoint. The seven-line output has SHA-256 digest `027dcba8ec13682f044b6c7ee8eb1e609f5e5ac537dee552a17d0e18a2f427f2`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the displayed packing, all cyclic 3- and 5-subset orbits on Z_31, and the pair-incidence arithmetic",
    "bounds": {
      "group_order": {
        "min": 31,
        "max": 31
      },
      "base_blocks_checked": {
        "min": 9,
        "max": 9
      },
      "five_subset_orbits_enumerated": {
        "min": 5481,
        "max": 5481
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.1016/S0012-365X(03)00266-8",
      "locator": "Inline CPython verifier; the set-theoretic cyclic-shift formulation follows Wensong Chu and Charles J. Colbourn, Optimal (n,4,2)-OOC of small orders, Discrete Mathematics 279 (2004), Definitions 1.1-1.3"
    },
    "outputs": "base_blocks=9 developed_blocks=279\ntriples=2790 distinct_triples=2790\ntriple_orbits_used=90 total_triple_orbits=145\nblock_orbits=5481 internally_valid=4761\npair_multiplicity=4:31,5:124,6:124,7:186\npair_cap=9 ordinary_block_cap=418 cyclic_base_cap=13\npacking_sha256=2323141aa6883f95a8b8ee5b300cc4b8a57f7437d08a43054de576c99e30228f\n",
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from math import comb",
      "V=31",
      "BASE_BLOCKS=[(0,3,9,12,24),(0,2,6,8,15),(0,1,15,27,29),(0,1,9,18,20),(0,3,6,14,19),(0,3,7,13,27),(0,1,2,7,24),(0,1,5,13,26),(0,1,4,21,22)]",
      "def translate(block,shift):",
      "    return tuple(sorted((x+shift)%V for x in block))",
      "def canonical_translate(values):",
      "    values=tuple(values)",
      "    return min(translate(values,-shift) for shift in values)",
      "assert len(BASE_BLOCKS)==len(set(BASE_BLOCKS))==9",
      "assert all(len(block)==5 and tuple(sorted(block))==block for block in BASE_BLOCKS)",
      "orbits=[[translate(block,shift) for shift in range(V)] for block in BASE_BLOCKS]",
      "assert all(len(set(orbit))==V for orbit in orbits)",
      "blocks=[block for orbit in orbits for block in orbit]",
      "assert len(blocks)==len(set(blocks))==279",
      "triples=[triple for block in blocks for triple in combinations(block,3)]",
      "triple_counts=Counter(triples)",
      "assert len(triples)==2790 and len(triple_counts)==2790",
      "assert set(triple_counts.values())=={1}",
      "triple_orbits_used={canonical_translate(triple) for triple in triples}",
      "assert len(triple_orbits_used)==90",
      "all_triple_orbits={canonical_translate(triple) for triple in combinations(range(V),3)}",
      "all_block_orbits={canonical_translate((0,)+tail) for tail in combinations(range(1,V),4)}",
      "valid_block_orbits=0",
      "for block in all_block_orbits:",
      "    covered={canonical_translate(triple) for triple in combinations(block,3)}",
      "    valid_block_orbits+=len(covered)==comb(5,3)",
      "assert len(all_triple_orbits)==145",
      "assert len(all_block_orbits)==5481",
      "assert valid_block_orbits==4761",
      "pair_counts=Counter(pair for block in blocks for pair in combinations(block,2))",
      "pair_distribution=Counter(pair_counts.get(pair,0) for pair in combinations(range(V),2))",
      "assert sum(pair_counts.values())==len(blocks)*comb(5,2)==2790",
      "assert max(pair_counts.values())<=9",
      "pair_cap=(V-2)//(5-2)",
      "ordinary_block_cap=comb(V,2)*pair_cap//comb(5,2)",
      "cyclic_base_cap=ordinary_block_cap//V",
      "assert pair_cap==9 and ordinary_block_cap==418 and cyclic_base_cap==13",
      "canonical='\\n'.join(' '.join(map(str,block)) for block in BASE_BLOCKS)+'\\n'",
      "packing_sha=sha256(canonical.encode()).hexdigest()",
      "print(f'base_blocks={len(BASE_BLOCKS)} developed_blocks={len(blocks)}')",
      "print(f'triples={len(triples)} distinct_triples={len(triple_counts)}')",
      "print(f'triple_orbits_used={len(triple_orbits_used)} total_triple_orbits={len(all_triple_orbits)}')",
      "print(f'block_orbits={len(all_block_orbits)} internally_valid={valid_block_orbits}')",
      "print('pair_multiplicity='+','.join(f'{k}:{pair_distribution[k]}' for k in sorted(pair_distribution)))",
      "print(f'pair_cap={pair_cap} ordinary_block_cap={ordinary_block_cap} cyclic_base_cap={cyclic_base_cap}')",
      "print(f'packing_sha256={packing_sha}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/S0012-365X(03)00266-8",
    "locator": "Inline CPython verifier; the set-theoretic cyclic-shift formulation follows Wensong Chu and Charles J. Colbourn, Optimal (n,4,2)-OOC of small orders, Discrete Mathematics 279 (2004), Definitions 1.1-1.3"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R187",
      "title": "Nine base blocks form a cyclic 3-packing",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R188",
      "title": "Pair incidences give an upper bound of thirteen",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "cyclic-315-packing-31",
      "title": "cyclic 315 packing 31",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}