Mandatory source/status baseline audit, design-theoretic reduction audit, and bounded validation of the promoted S(4,5,v) exact-cover tooling

counterexample and witness search

Derive necessary Steiner large sets, validate their exact encodings on a known positive instance and adversarial corruptions, and distinguish independently reproducible bounds from unsupported reports.

Hypothesis: The first parameter surviving the audited established exclusions is k=16; its necessary S(4,5,21) exact-cover encoding can be validated independently without attempting the open solve, while the bare recursive Johnson bound is insufficient to reproduce the forum's stronger k<=500 exclusion report.

Test: Check primary/current sources for every exclusion, solve and independently validate the known S(4,5,11) control, reject three corrupted witnesses under two checkers, reconstruct every clause of the S(4,5,21) CNF independently, and compare two exact implementations of the unseeded Johnson recurrence through k=500.

This is legitimate baseline progress because it corrects the source trail, converts the design implication into a quantifier-preserving frontier map, independently validates reusable certificate tooling, records exact computational scale, and prevents three likely overclaims. It is not candidate-level because no new coloring, design, nonexistence certificate, improved bound, or formal theorem was obtained.

• A target coloring yields LS(k-1,k,2k); for k>=5, derivation at any fixed (k-5)-set yields the necessary LS(4,5,k+5).
• Known nonexistence of S(4,5,15) and S(4,5,17) excludes k=10 and k=12.
• Relative to the explicitly audited results, k=16 is the first parameter still live.
• The generated pairwise CNF for S(4,5,21) has 20,349 variables and 819,945 clauses and matches an independent semantic reconstruction.
• For 3<=k<=500, the unseeded recursive Johnson bound excludes exactly the composite k+1 cases and leaves every prime-offset case at chromatic lower bound k+1.
• No S(4,5,21), LS(4,5,21), or Johnson coloring search was attempted.

• notes/baseline-audit-2026-07-21.md, SHA-256 a350f9341e03874f66804ef978b7886ea542937715ed8f349aaa573f6e850e1c
• records/research-state.json records the completed baseline review and exact continuation.
• .proof-experiments/20260721-024238-f079dc: return code 0, seed 0, 120-second/1024-MB limits, peak child memory 19,968 KB.
• The v=21 CNF SHA-256 is 37deda7c20de593fad902ddec5d143b17d20a0c83b848ed1bbd2ce9d99bc5966.
• .proof-experiments/20260721-024452-8ac515: return code 0, seed 0, 30-second/512-MB limits; canonical bound-record SHA-256 88a0e1f2ea6ec0691e958553fcb1b5c9336fc93fd643d008c7f68e034e5c2517.
• python3 -m json.tool accepted both structured JSON records; Python compilation and git diff --check passed.

• .proof-experiments/20260721-024238-f079dc: S(4,5,11) solved and accepted by two non-import-sharing checkers; missing, duplicate, and wrong-block controls were rejected by both; all 819,945 clauses of the unsolved v=21 CNF were independently checked.
• .proof-experiments/20260721-024452-8ac515: two exact implementations of the bare recursive Johnson bound agreed for every 3<=k<=500 and left all prime-offset cases.

tools/check_steiner45.py independently reconstructs the lexicographic variable map and expected DIMACS clauses and separately checks block incidences without importing tools/steiner45_exact_cover.py. It agreed on the valid S(4,5,11) witness and rejected all three corruptions.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• Constant-weight codes -> chi(J(2k,k)) >= ceil(C(2k,k)/A(2k,4,k)) -> the bare recurrence reproduced only the composite-offset obstruction, so stronger table seeds are the next measurable requirement.
• Steiner derivation -> a coloring implies LS(4,5,k+5) -> published S(4,5,15) and S(4,5,17) nonexistence eliminates k=10 and k=12 and redirects attention to k=16.
• Exact-cover certification -> a known S(4,5,11) control should validate generator/checker semantics -> both checkers accepted the model and rejected six checker-corruption combinations.

• For every k>2 with composite k+1, chi(J(2k,k))>=k+2.
  Ma-Tang Theorem 2.2, repository commit 7f131832bab5abfc903014ddb61efff21d56ae01; audited PDF SHA-256 1597f3f9eb577869e9955aacd4234bc8ab02584c1f879b55688f810b882d9424. · All k>2 with composite k+1. · proved
• A target coloring implies LS(k-1,k,2k) and, for k>=5, LS(4,5,k+5).
  For each (k-1)-set, its k+1 one-point extensions form a K_(k+1) and receive every color once; derivation preserves the partition. · Necessary condition only; no converse is asserted. · proved
• The target is impossible for k=10 and k=12.
  Nonexistence of the necessary S(4,5,15) and S(4,5,17), respectively. · Exactly k=10 and k=12. · proved
• k=16 is the first parameter not excluded by the audited results.
  Maintained k<=8 exclusions, Ma-Tang composite-offset theorem, and the k=10 and k=12 design obstructions. · Relative to the explicitly audited published/maintained results. · conditional
• The S(4,5,21) pairwise CNF contains 20,349 variables and 819,945 semantically verified clauses.
  .proof-experiments/20260721-024238-f079dc and independent checker tools/check_steiner45.py. · Encoding correctness; satisfiability was not tested. · computed
• The unseeded Johnson recurrence excludes exactly composite offsets through k=500.
  .proof-experiments/20260721-024452-8ac515, two exact implementations. · 3<=k<=500 and the bare recurrence only. · computed

• Present one S(4,5,21) model as a solution to Erdős #835.
  Any isolated derived design without a 17-design partition and full lift. · The coloring implies LS(15,16,32), and derivation gives LS(4,5,21), not merely one constituent design. · Design derivation in notes/baseline-audit-2026-07-21.md. · Supply a proved lift or a complete independently checked coloring.
• Naive direct SAT encoding of J(32,16) on the audited host.
  Straightforward vertex-color and edge-clause encoding. · It requires over 10.2 billion color variables and roughly 1.31 trillion edge-color clauses. · Exact graph counts in the baseline audit. · A rigorous compression, orbit theorem, or structural reduction changing the scale by orders of magnitude.
• Treat the forum's k<=500 four-survivor statement as established.
  The reported exclusions beyond the bare recurrence. · No frozen seeds, implementation, origin ledger, or certificate was supplied, and the independently run bare recurrence leaves every prime offset. · .proof-experiments/20260721-024452-8ac515. · Two independently implemented exact table-seeded propagations with matching origin ledgers.
• Infer nonexistence of S(4,5,21) from searches with prescribed automorphism groups.
  The group-restricted searches in Kiermaier-Krčadinac-Wassermann (2026). · They do not cover asymmetric designs, and the authors explicitly describe the negative results as little evidence. · https://doi.org/10.1007/s10623-026-01888-w · An unrestricted proof-checked enumeration or theorem exhausting all automorphism possibilities.

• Reconstruct the reported table-seeded constant-weight-code exclusions through k=500.
  This is the cheapest way to convert a currently uncheckable report into a precise exclusion map and identify the decisive bound seeds. · Freeze codes.se/cw.html, build two exact fixed-point propagators with seed provenance, and compare the survivor sets. · high · open
• Formalize coloring implies LS(k-1,k,2k) and derived LS(4,5,k+5).
  The reduction is compact, central, and has a tractable kernel-checkable verification surface. · Run /root/proof-factory/scripts/bootstrap-formal-conjectures.sh and compile the reduction against the pinned Property definition without sorry. · normal · open
• Test tactical-decomposition constraints for LS(4,5,21).
  Partition-level obstructions are closer to the target than searching for one isolated S(4,5,21). · Encode only design-level intersection equations and validate the encoding on smaller known large-set controls. · low · open

Objective: Independently reconstruct the forum-reported table-seeded constant-weight exclusion map through k=500.

First action: Run `curl --fail --location --create-dirs --output sources/codes-se-cw-2026-07-21.html https://codes.se/bounds/cw.html`, then record its SHA-256 and retrieval timestamp before implementing tools/table_seeded_bound_audit.py.

Stop condition: Stop when two independent exact update orders either reproduce exactly {16,112,256,268} with an origin ledger or expose the first irreducible missing or ambiguous seed. Do not extend beyond k=500 or begin a design/coloring search.

• Freeze the maintained codes.se constant-weight table with retrieval timestamp and SHA-256.
• Implement two independent table-seeded exact bound propagators with an origin ledger for every imported or derived bound.
• Stop at exact reproduction of the reported survivor set {16,112,256,268} or at the first irreducible table-seed discrepancy.
• Do not launch S(4,5,21) or direct J(32,16) search during that reconstruction.

• https://www.erdosproblems.com/835 ↗
• https://doi.org/10.1007/BFb0066199 ↗
• https://github.com/QuanyuTang/erdos-problem-835 ↗
• https://doi.org/10.1016/j.jcta.2008.04.005 ↗
• https://doi.org/10.1007/s10623-026-01888-w ↗
• https://doi.org/10.1109/18.887851 ↗
• https://codes.se/bounds/cw.html ↗
• https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/835.lean ↗

The campaign's GPT-5.6 Sol principal performed synthesis, source auditing, experiment design, and checkpointing. A GPT-5.6 Terra source-discriminator supplied an advisory memo, SHA-256 f6b22221eda2e5565a44a0e51639237b7bbb45fadb64d0a82d1e5f2f8457cc56; its claims and promoted generator were independently audited. Automated tools used were web retrieval, Git/GitHub metadata, Python 3.12.3, and CaDiCaL 1.7.3. GAP 4.12.1 and Lean/Lake were inventoried but produced no mathematical evidence. No frontier SAT solve, proof assistant theorem, or external publication occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1432.6s

Review state

not a result claim

Attempt ID

erdos-835-20260721-025353-29df74

No human review recorded.