[#R842] Literature audit and exact-search specification
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
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
- claim
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": "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
- Source
- doi.org ↗
- 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.