TheoremDB
R185attemptStatus: inconclusiveEvidence: InconclusiveReplay: source only

[#R185] Literature and exact-search audit leaves four cases

View evidenceOpen source ↗

1Summary

The checked sources establish the general framework and upper-bound method, while a capped feasibility run produced no reusable certificate for sizes ten through thirteen.

The primary-source audit covered the original optical orthogonal code framework of Chung, Salehi, and Wei; the ordinary packing definition and Johnson-Schonheim bound summarized by Bailey and Burgess; and Chu and Colbourn's exact-search formulation for small cyclic OOCs. Related cyclic difference-packing and cyclic group-divisible-packing papers concern different strengths or block sizes. No checked source stated \(\Phi(31,5,2)\) or printed a construction with ten or more codewords.

A complete orbit generator found 145 translation classes of triples and 4,761 internally valid translation classes of 5-subsets. The maximum is therefore a 0-1 set-packing problem with 145 at-most-one constraints. A 120-second Z3 feasibility attempt at size 13 did not finish and yielded no proof object. This timing result carries no mathematical weight. A useful continuation would encode target sizes 13, 12, 11, and 10 with a proof-producing pseudo-Boolean or SAT solver, retain a DRAT/LRAT-style unsatisfiability certificate when available, and replay any satisfying base-block list with the artifact in this record.

Inconclusive evidence. Recorded scope: primary sources and a capped orbit-level feasibility search checked on 2026-07-25.

2Outcome

Evidence package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: doi.org ↗, F. R. K. Chung, J. A. Salehi, and V. K. Wei, Optical orthogonal codes: design, analysis and applications, IEEE Transactions on Information Theory 35 (1989), 595-604; literature audit and capped computation on 2026-07-25

3What was measured

Parameter specific primary source found
no
Candidate orbits
4,761
Constraint rows
145
Solver
Z3 pseudo-Boolean constraints
Target attempted
13
Time cap
2 minutes
Certificate retained
no
Remaining target sizes
10, 11, 12, 13

4How it connects

Contextualizes

Recorded for

5Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R185",
  "content_hash": null,
  "slug": "cyclic315-attempt-literature-and-exact-search-audit",
  "type": "attempt",
  "title": "Literature and exact-search audit leaves four cases",
  "summary": "The checked sources establish the general framework and upper-bound method, while a capped feasibility run produced no reusable certificate for sizes ten through thirteen.",
  "relevance": "For Largest cyclic 3-(31,5,1) packing, record cyclic315-attempt-literature-and-exact-search-audit (“Literature and exact-search audit leaves four cases”) documents a concrete method, search boundary, or failed route. The record states: The checked sources establish the general framework and upper-bound method, while a capped feasibility run produced no reusable certificate for sizes ten through thirteen.",
  "relevance_source": "recorded",
  "body": "The primary-source audit covered the original optical orthogonal code framework of Chung, Salehi, and Wei; the ordinary packing definition and Johnson-Schonheim bound summarized by Bailey and Burgess; and Chu and Colbourn's exact-search formulation for small cyclic OOCs. Related cyclic difference-packing and cyclic group-divisible-packing papers concern different strengths or block sizes. No checked source stated \\(\\Phi(31,5,2)\\) or printed a construction with ten or more codewords.\n\nA complete orbit generator found 145 translation classes of triples and 4,761 internally valid translation classes of 5-subsets. The maximum is therefore a 0-1 set-packing problem with 145 at-most-one constraints. A 120-second Z3 feasibility attempt at size 13 did not finish and yielded no proof object. This timing result carries no mathematical weight. A useful continuation would encode target sizes 13, 12, 11, and 10 with a proof-producing pseudo-Boolean or SAT solver, retain a DRAT/LRAT-style unsatisfiability certificate when available, and replay any satisfying base-block list with the artifact in this record.",
  "status": "inconclusive",
  "evidence_grade": "documented",
  "scope": {
    "kind": "bounded",
    "statement": "primary sources and a capped orbit-level feasibility search checked on 2026-07-25",
    "bounds": {
      "candidate_orbits": {
        "min": 4761,
        "max": 4761
      },
      "triple_orbit_constraints": {
        "min": 145,
        "max": 145
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://doi.org/10.1109/18.30982",
      "locator": "F. R. K. Chung, J. A. Salehi, and V. K. Wei, Optical orthogonal codes: design, analysis and applications, IEEE Transactions on Information Theory 35 (1989), 595-604; literature audit and capped computation on 2026-07-25"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/18.30982",
    "locator": "F. R. K. Chung, J. A. Salehi, and V. K. Wei, Optical orthogonal codes: design, analysis and applications, IEEE Transactions on Information Theory 35 (1989), 595-604; literature audit and capped computation on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R186",
      "title": "The certified interval is 9 through 13 base blocks",
      "object_type": "claim",
      "relation": "contextualizes",
      "direction": "outgoing"
    },
    {
      "slug": "cyclic-315-packing-31",
      "title": "cyclic 315 packing 31",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

6Provenance

View source, identifiers, and projection details
Project
cyclic-315-packing-31
Locator
F. R. K. Chung, J. A. Salehi, and V. K. Wei, Optical orthogonal codes: design, analysis and applications, IEEE Transactions on Information Theory 35 (1989), 595-604; literature audit and capped computation on 2026-07-25
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R185
Stable alias
cyclic315-attempt-literature-and-exact-search-audit
Projection
Reproduction fields are derived from the immutable record.

A route someone took, recorded so the next person can reuse it or avoid it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.