{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R190",
  "content_hash": null,
  "slug": "db127-attempt-published-exhaustive-audit",
  "type": "attempt",
  "title": "Two exhaustive computations exclude a 12-element cover",
  "summary": "Wiedemann and Haanpää used separate isomorph-rejecting backtrack searches and agreed on every cyclic value through 127.",
  "relevance": "For Difference size of Z_127, record db127-attempt-published-exhaustive-audit (“Two exhaustive computations exclude a 12-element cover”) documents a concrete method, search boundary, or failed route. The record states: Wiedemann and Haanpää used separate isomorph-rejecting backtrack searches and agreed on every cyclic value through 127.",
  "relevance_source": "recorded",
  "body": "Wiedemann's 1992 computation extended the table of lexicographically first minimum cyclic difference covers through modulus 133. Its modulus-127 result has cardinality 13, which excludes a 12-element cover.\n\nHaanpää independently computed minimum difference covers for every finite Abelian group of order at most 127. His search recursively extends subsets, rejects affine-equivalent copies, and prunes a partial set once its repeated differences exceed the final collision allowance. For a cyclic group, the equivalence mappings used by the canonicity test are exactly affine maps \\(x\\mapsto ux+c\\) with \\(u\\) a unit. The orderly-search theorem proves that every canonical subset is visited. Section 5 reports agreement with Wiedemann on the minimum cardinality of every cyclic group through order 127.\n\nFor this modulus, affine normalization may send any ordered pair of distinct elements to \\((0,1)\\). A hypothetical 12-set would then have to cover the 63 nonzero inverse classes using 66 unordered pairs, so only three repeated inverse classes are allowed. This is the exact monotone collision prune described by the published method. The two implementations supply independent exhaustive evidence for the lower endpoint 13.",
  "status": "completed",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "published exhaustive determinations of minimum cyclic difference covers through modulus 127",
    "bounds": {
      "largest_modulus": {
        "min": 127,
        "max": 133
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
      "locator": "Haanpää 2004, Sections 3.2, 3.3, 4, and 5, especially the orderly-search completeness theorem and the comparison with Wiedemann; Wiedemann 1992, 181-185"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
    "locator": "Haanpää 2004, Sections 3.2, 3.3, 4, and 5, especially the orderly-search completeness theorem and the comparison with Wiedemann; Wiedemann 1992, 181-185"
  },
  "models": [],
  "relations": [
    {
      "slug": "R192",
      "title": "The exact difference size of Z/127Z is 13",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "difference-basis-z127",
      "title": "difference basis z127",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}