TheoremDB
R843claimStatus: openEvidence: ReproducedReplay: source only

[#R843] The certified interval is 30 through 67

claim. An explicit 30-set supplies the lower endpoint. Exact incidence counting in the progression design gives the upper endpoint.

View evidenceOpen source ↗

1Summary

Write \(\alpha(101,4)\) for the requested maximum. The independently replayed bounds are \[ \boxed{30\leq\alpha(101,4)\leq67}. \] The lower bound is witnessed by \[ \{0,10,18,23,27,29,35,37,39,40,45,47,48,49,56,61,65,68,69,70,72,76,78,79,84,85,87,91,93,95\}. \] The executable artifact generates all 5,050 distinct modular four-term progressions and checks that none lies inside this set.

For the upper bound, let \(H\) be the four-uniform progression hypergraph. Every vertex lies in 200 edges, and every unordered pair lies in six edges. If \(A\) is independent and \(j_E=|A\cap E|\), then \(j_E\leq3\). Double-counting selected pairs and selected vertex-edge incidences gives \[ 6\binom{|A|}{2}=\sum_E\binom{j_E}{2}\leq\sum_Ej_E=200|A|. \] For positive \(|A|\), this yields \(3(|A|-1)\leq200\), hence \(|A|\leq67\). The exact value remains open within this record.

Reproduced evidence. Recorded scope: subsets of Z/101Z containing no four distinct terms x, x+d, x+2d, x+3d with d nonzero.

2Evidence

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, Sections 0 and 3; the order-101 incidence calculation is independently derived here

3What was measured

Lower bound
30
Upper bound
67
Gap
37
Exact value known
no
Witness replayed
yes
Upper bound replayed
yes
Search date
2026-07-25

4How it connects

Supported by

Contextualizes (incoming)

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": "R843",
  "content_hash": null,
  "slug": "z101-four-ap-free-claim-certified-interval-30-67",
  "type": "claim",
  "title": "The certified interval is 30 through 67",
  "summary": "An explicit 30-set supplies the lower endpoint. Exact incidence counting in the progression design gives the upper endpoint.",
  "relevance": "For Largest four-term-progression-free subset of Z_101, record z101-four-ap-free-claim-certified-interval-30-67 (“The certified interval is 30 through 67”) records a bound, answer, status fact, or structural consequence. The record states: An explicit 30-set supplies the lower endpoint.",
  "relevance_source": "recorded",
  "body": "Write \\(\\alpha(101,4)\\) for the requested maximum. The independently replayed bounds are\n\\[\n\\boxed{30\\leq\\alpha(101,4)\\leq67}.\n\\]\nThe lower bound is witnessed by\n\\[\n\\{0,10,18,23,27,29,35,37,39,40,45,47,48,49,56,61,65,68,69,70,72,76,78,79,84,85,87,91,93,95\\}.\n\\]\nThe executable artifact generates all 5,050 distinct modular four-term progressions and checks that none lies inside this set.\n\nFor the upper bound, let \\(H\\) be the four-uniform progression hypergraph. Every vertex lies in 200 edges, and every unordered pair lies in six edges. If \\(A\\) is independent and \\(j_E=|A\\cap E|\\), then \\(j_E\\leq3\\). Double-counting selected pairs and selected vertex-edge incidences gives\n\\[\n6\\binom{|A|}{2}=\\sum_E\\binom{j_E}{2}\\leq\\sum_Ej_E=200|A|.\n\\]\nFor positive \\(|A|\\), this yields \\(3(|A|-1)\\leq200\\), hence \\(|A|\\leq67\\). The exact value remains open within this record.",
  "status": "open",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "subsets of Z/101Z containing no four distinct terms x, x+d, x+2d, x+3d with d nonzero",
    "bounds": {
      "modulus": {
        "min": 101,
        "max": 101
      },
      "progression_length": {
        "min": 4,
        "max": 4
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4171/EM/16",
      "locator": "Lorenz and Stephanie Halbeisen, Avoiding arithmetic progressions in cyclic groups, Sections 0 and 3; the order-101 incidence calculation is independently derived here"
    },
    "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, Sections 0 and 3; the order-101 incidence calculation is independently derived here"
  },
  "relations": [
    {
      "slug": "R841",
      "title": "Exact witness and incidence verifier",
      "object_type": "artifact",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R842",
      "title": "Literature audit and exact-search specification",
      "object_type": "attempt",
      "relation": "contextualizes",
      "direction": "incoming"
    },
    {
      "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, Sections 0 and 3; the order-101 incidence calculation is independently derived here
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R843
Stable alias
z101-four-ap-free-claim-certified-interval-30-67
Projection
Reproduction fields are derived from the immutable record.

A statement this project treats as settled at the recorded evidence grade, with the work that backs it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.