{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R842",
  "content_hash": null,
  "slug": "z101-four-ap-free-attempt-literature-audit-and-exact-plan",
  "type": "attempt",
  "title": "Literature audit and exact-search specification",
  "summary": "The checked cyclic-group paper supplies the framework but no value for these parameters. A small, auditable SAT instance would decide the optimum.",
  "relevance": "For Largest four-term-progression-free subset of Z_101, record z101-four-ap-free-attempt-literature-audit-and-exact-plan (“Literature audit and exact-search specification”) documents a concrete method, search boundary, or failed route. The record states: The checked cyclic-group paper supplies the framework but no value for these parameters.",
  "relevance_source": "recorded",
  "body": "Halbeisen and Halbeisen define \\(\\alpha(n,r)\\) as the independence number of the modular progression hypergraph and give exact values for selected smaller parameters. Their table has no row for \\((101,4)\\). The broader primary literature checked for four-term progression bounds is asymptotic and does not certify a sharper order-101 value.\n\nAn exact computation can encode one Boolean variable \\(x_i\\) for each residue. Each of the 5,050 edges contributes the clause \\(\\bigvee_{i\\in E}\\neg x_i\\). To test a target \\(k\\), add an exact cardinality constraint \\(\\sum_i x_i\\geq k\\). Affine maps \\(x\\mapsto ux+v\\), with \\(u\\ne0\\), preserve the hypergraph. For every solution of size at least two, one ordered selected pair can therefore be normalized to \\(0,1\\). A complete upper certificate should use a proof-logging SAT or pseudo-Boolean solver, record the generator hash and normalized case split, and replay the emitted proof with an independent checker. Running targets downward until satisfiable would determine the exact value; the satisfying assignment supplies the matching lower witness.",
  "status": "inconclusive",
  "evidence_grade": "sourced",
  "scope": null,
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://doi.org/10.4171/EM/16",
      "locator": "Lorenz and Stephanie Halbeisen, Avoiding arithmetic progressions in cyclic groups, definition of alpha(n,r), hypergraph formulation, and summary"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4171/EM/16",
    "locator": "Lorenz and Stephanie Halbeisen, Avoiding arithmetic progressions in cyclic groups, definition of alpha(n,r), hypergraph formulation, and summary"
  },
  "models": [],
  "relations": [
    {
      "slug": "R843",
      "title": "The certified interval is 30 through 67",
      "object_type": "claim",
      "relation": "contextualizes",
      "direction": "outgoing"
    },
    {
      "slug": "z101-four-ap-free",
      "title": "z101 four ap free",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}