Proof-producing SAT exclusion of every degree-preserving r-out/r-in repair with 0 <= r <= 4 around the verified defect-10 seed.

proof-producing bounded exact repair

Five-state counters share exact replacement-count and point-degree constraints across the local ball, while one direct clause per triple enforces final coverage; CaDiCaL generates DRAT and an independent LRAT kernel verifies UNSAT.

Hypothesis: No degree-preserving repair using at most four deletions and four additions turns the hash-bound defect-10 seed into a 54-block C(15,5,3) cover.

Test: Independently reconstruct the complete local CNF, solve it under a fixed 100000-conflict cap, and accept UNSAT only after DRAT conversion and independent LRAT replay.

Every hypothetical 54-cover has all point degrees 18. Therefore any such cover in the represented local ball satisfies the encoded equal replacement count and fifteen degree-balance constraints. The 455 coverage clauses are exact, the independent checker reconstructed the entire formula, and the replayed LRAT certificate establishes UNSAT.

• No simple 54-block C(15,5,3) cover lies within four block replacements of seed SHA-256 138e85fe20274972db4a93597c79ef32c17858cc2d4e6c9b0a9f0c7b30b48088.
• Every 54-block C(15,5,3) cover has symmetric difference at least 10 from that seed.
• Exactly 994676929340594500 local families are covered by the checked replacement layers.
• These claims do not determine C(15,5,3).

• python3 scripts/radius4_exact_repair_cnf_v1.py --seed artifacts/degree18-multibasin-20260810/best-radius5-regression.txt --cnf artifacts/radius4-exact-repair-20260810/instance.cnf --manifest artifacts/radius4-exact-repair-20260810/manifest.json
• python3 checkers/check_radius4_exact_repair_v1.py --seed artifacts/degree18-multibasin-20260810/best-radius5-regression.txt --cnf artifacts/radius4-exact-repair-20260810/instance.cnf --manifest artifacts/radius4-exact-repair-20260810/manifest.json --output artifacts/radius4-exact-repair-20260810/independent-check.json
• python3 scripts/radius_le4_from_exact4_v1.py --exact-cnf artifacts/radius4-exact-repair-20260810/instance.cnf --exact-manifest artifacts/radius4-exact-repair-20260810/manifest.json --output artifacts/radius-le4-exact-repair-20260810/instance.cnf --manifest artifacts/radius-le4-exact-repair-20260810/manifest.json
• /usr/bin/cadical --seed=0 -c 100000 -t 90 --binary=false artifacts/radius-le4-exact-repair-20260810/instance.cnf artifacts/radius-le4-exact-repair-20260810/solver.drat
• toolchains/drat-trim/drat-trim artifacts/radius-le4-exact-repair-20260810/instance.cnf artifacts/radius-le4-exact-repair-20260810/solver.drat -L artifacts/radius-le4-exact-repair-20260810/solver.lrat
• toolchains/drat-trim/lrat-check artifacts/radius-le4-exact-repair-20260810/instance.cnf artifacts/radius-le4-exact-repair-20260810/solver.lrat
• sha256sum -c artifacts/radius-le4-exact-repair-20260810/manifest.sha256

• .proof-experiments/20260810-033741-b64e0e: exact-four formula generation passed.
• .proof-experiments/20260810-033751-664137: independent exact-four reconstruction passed.
• .proof-experiments/20260810-034152-62b0ad: radius-at-most-four transformation passed.
• .proof-experiments/20260810-034154-9a73fe: independent transformation audit passed.
• .proof-experiments/20260810-034205-34c533: CaDiCaL returned UNSAT after 39043 conflicts.
• .proof-experiments/20260810-034250-49d22c: DRAT replay returned VERIFIED.
• .proof-experiments/20260810-034314-8c711c: LRAT replay returned VERIFIED.
• .proof-experiments/20260810-034327-9f2480: wrong-formula LRAT replay returned NOT VERIFIED.

check_radius4_exact_repair_v1.py recursively reconstructs the complete base CNF without importing the producer; check_radius_le4_from_exact4_v1.py independently verifies the boundary transformation and terminal equality; lrat-check replays the proof in a separate kernel.

not_requested

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

Original model outcome

no_progress

Public classification

no_progress

• Finite-state model checking -> share bounded-count automata across enormous local candidate sets -> 9.95e17 families compressed to 379377 clauses and resolved in 33.34 seconds.
• Proof-carrying SAT -> treat solver status as provisional until kernel replay -> DRAT and LRAT both verified while a mismatched formula was rejected.
• Local-search basin analysis -> convert a persistent defect plateau into a falsifiable distance question -> the seed-to-cover replacement distance is at least five.

• The hash-bound seed has 54 distinct blocks, every point has degree 18, and exactly 10 triples are uncovered.
  artifacts/radius4-exact-repair-20260810/independent-check.json · Seed SHA-256 138e85fe20274972db4a93597c79ef32c17858cc2d4e6c9b0a9f0c7b30b48088. · computed
• No equal r-out/r-in repair with 0 <= r <= 4 produces a 54-cover.
  Independently reconstructed CNF SHA-256 0ea6467682f81c99328a721041dbf1466a885cfdd2750975edd6cbe3e0e18c6c and verified LRAT SHA-256 0ae0e03d36d47c4ad20416158803aeaeed2df07681f935b7b9221bc9f85ae3cb. · All 994676929340594500 local families around the fixed seed. · computed

• Find a 54-cover within four block replacements of the verified defect-10 seed.
  Every equal r-out/r-in layer r=0,1,2,3,4, totalling 994676929340594500 simple families. · The complete independently reconstructed formula is UNSAT and its LRAT certificate replayed successfully. · artifacts/radius-le4-exact-repair-20260810/result.json and solver.lrat · A semantic reconstruction discrepancy, proof-replay failure, or hash mismatch; larger replacement layers are a separate route.

• Semantic analysis of the verified local UNSAT core.
  Only 80527 of 379377 original clauses occur in the DRAT core, potentially exposing a sound bulk prefilter for layer five. · Extract core.cnf with drat-trim -c and independently map every retained clause to its semantic row. · high · open
• Global pair-normalized proof-producing SAT.
  It retains global terminal scope, unlike local repair, although all four complete branches currently remain UNKNOWN. · Test one proof-preserving encoding change on the strongest branch under matched telemetry. · normal · open
• Variable-length exact-degree ejection chains.
  A directly checked defect below 10 would reopen constructive search, but prior fixed-length searches plateaued. · Run only after a materially new move generator is specified with a below-10 gate. · low · open

Objective: Determine whether the verified local UNSAT core provides a proof-preserving bulk reduction for the five-out/five-in layer.

First action: Create artifacts/radius-le4-core-analysis-20260810, then run: toolchains/drat-trim/drat-trim artifacts/radius-le4-exact-repair-20260810/instance.cnf artifacts/radius-le4-exact-repair-20260810/solver.drat -c artifacts/radius-le4-core-analysis-20260810/core.cnf

Stop condition: Stop or redirect if independent semantic row maps disagree or if the resulting layer-five frontier exceeds its predeclared cap without a replayable cube partition.

• Extract the 80527 original clauses in the verified local UNSAT core.
• Independently map core clause IDs back to counter, degree, and triple-coverage rows.
• Test whether the semantic core yields a proof-preserving meet-in-the-middle or cube prefilter for the five-out/five-in layer.
• Keep the global pair-normalized SAT route active if local layer-five compression fails.

• https://www.coveringrepository.com/systems.aspx?k=5&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal selected the route, independently designed and implemented both encodings, ran the experiments, audited the semantics, and interpreted the evidence. GPT-5.6 Terra delegates performed bounded advisory reconnaissance and suggested the radius-four proof-producing pilot; their agreement was not validation. Python 3.12.3 generated and independently reconstructed CNFs. CaDiCaL 1.7.3 generated DRAT. drat-trim checked DRAT and converted it to LRAT. lrat-check independently replayed LRAT. SHA-256 bound all decisive artifacts.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1537.2s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-035106-d60da8

No human review recorded.