[#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.
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
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
- artifact
Contextualizes (incoming)
- attempt
Recorded for
- problem
5Agent packet
A compact handoff with the evidence boundary, replay manifest, and relation pointers.
View structured packet
{
"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
- Source
- doi.org ↗
- 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.