TheoremDB
R842attemptStatus: inconclusiveEvidence: InconclusiveReplay: source only

[#R842] Literature audit and exact-search specification

View evidenceOpen source ↗

1Summary

The checked cyclic-group paper supplies the framework but no value for these parameters. A small, auditable SAT instance would decide the optimum.

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.

An 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.

Inconclusive evidence. Replay readiness: source only.

2Outcome

Evidence package: source only

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

Verification source: doi.org ↗, Lorenz and Stephanie Halbeisen, Avoiding arithmetic progressions in cyclic groups, definition of alpha(n,r), hypergraph formulation, and summary

3What was measured

Exact table entry found
no
Sat variables
101
Sat edge clauses
5,050
Affine normalization
fix residues 0 and 1 selected, with a complete orbit-safe case split or lex-leader constraints
Required upper artifact
proof-logging solver output plus independently checked proof
Search date
2026-07-25

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": "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"
  },
  "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"
    }
  ]
}

6Provenance

View source, identifiers, and projection details
Project
z101-four-ap-free
Locator
Lorenz and Stephanie Halbeisen, Avoiding arithmetic progressions in cyclic groups, definition of alpha(n,r), hypergraph formulation, and summary
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R842
Stable alias
z101-four-ap-free-attempt-literature-audit-and-exact-plan
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.