Fix the validated 18-block 7,5^13 point link, encode the remaining 36 root-avoiding blocks with exact residual degrees and triple coverage, then run a bounded controlled CaDiCaL discriminator.

local-link-seeded residual covering SAT

Fixing the complete point link removes every root-containing block choice and leaves 2002 residual primary variables constrained by 292 missing-triple clauses and residual degrees 11,13^13.

Hypothesis: The validated 18-block local link with ordered degrees 7,5^13 extends to a 54-block C(15,5,3) cover.

Test: Generate the exact residual CNF twice, validate it against a fully fixed split of the maintained 55-cover, and run CaDiCaL under a deterministic 5000-conflict cap.

The controls establish that the packet is suitable for further reproducible search, but UNKNOWN contains no mathematical information about satisfiability. This supports infrastructure progress only.

• The live fixed-link instance has 2002 primary variables, 49938 total variables, 360910 clauses, 292 residual coverage clauses, and residual degrees 11,13^13.
• The live CNF regenerated byte-identically with SHA-256 6f5c4979e6dd414a2543f2e1150042202a0b9c0abb6580890005f946edce96d2.
• The maintained 55-cover passed the generalized split encoder and both independent global checkers.
• The 5000-conflict live run returned UNKNOWN and makes no existence or nonexistence claim.

• python3 scripts/fixed_link_extension_cnf.py generate --link artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt --output artifacts/fixed-link-extension-pilot-20260808/live-a.cnf
• /usr/bin/cadical -c 5000 -w artifacts/fixed-link-extension-pilot-20260808/live-5000.model artifacts/fixed-link-extension-pilot-20260808/live-a.cnf
• python3 checkers/check_global_cover.py artifacts/fixed-link-extension-pilot-20260808/source-root0-decoded-cover.txt --blocks 55 --degrees 19,18,18,18,21,18,18,19,18,18,18,18,18,18,18
• python3 checkers/check_global_cover_masks.py artifacts/fixed-link-extension-pilot-20260808/source-root0-decoded-cover.txt --blocks 55
• sha256sum -c artifacts/fixed-link-extension-pilot-20260808/manifest.sha256

• .proof-experiments/20260808-164923-0b290c: fully fixed maintained-cover control returned SAT
• .proof-experiments/20260808-165011-85f4f2 and 20260808-165011-43823c: independent positive checks covered all 455 triples
• .proof-experiments/20260808-165011-26926d and 20260808-165011-ee65eb: the mutation produced the same six missing triples
• .proof-experiments/20260808-165249-8bc1bd: live 5000-conflict run returned UNKNOWN
• .proof-experiments/20260808-165657-6c3020: manifest integrity check passed

checkers/check_global_cover.py uses tuple/set enumeration and checkers/check_global_cover_masks.py uses an independent 15-bit-mask representation. Both accepted the maintained-cover control and rejected the same mutation. No live witness existed to check.

not_requested

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

Original model outcome

progress

Public classification

progress

• C(12,6,4) certified-SAT workflow -> require deterministic encodings, controls, and replay before negative claims -> the controls succeeded but no UNSAT claim arose.
• Maintained 55-cover split -> predict the generalized fixed-link encoder and decoder accept a known covering -> observed SAT and 455/455 triple coverage.
• Exact-pinnability -> predict residual degrees determine the residual block count without a separate constraint -> observed residual sum 180, hence 36 blocks.

• The maintained 55-cover survives the generalized split, fully fixed residual CNF, decoder, and two global checkers.
  Experiments 20260808-164923-0b290c, 20260808-165011-85f4f2, and 20260808-165011-43823c. · The copied maintained 55-cover under zero-based root 0 and its relabeling. · computed
• The displayed fixed link induces residual degrees 11,13^13, exactly 36 residual blocks, and 292 uncovered local triple obligations.
  Deterministic generator metadata in the two byte-identical live CNFs. · Extensions of the displayed labeled link only. · computed
• The bounded live CaDiCaL run reached 5000 conflicts and returned UNKNOWN.
  .proof-experiments/20260808-165249-8bc1bd/experiment.json and stdout.txt. · The exact live CNF, CaDiCaL 1.7.3, and the recorded conflict cap. · computed

• Treat the 5000-conflict UNKNOWN result as evidence that the fixed link extends or does not extend.
  Experiment 20260808-165249-8bc1bd. · UNKNOWN supplies neither a model nor an UNSAT proof. · The solver record has return code 0 and model file content c UNKNOWN. · A directly checked SAT model or independently replayed UNSAT proof.
• Use the unreceipted 60-second attempt as mathematical evidence.
  .proof-experiments/20260808-165104-d105b6. · No experiment.json, SAT status, UNSAT status, model, or proof was produced. · Only a partial solver log exists. · A clean deterministic rerun with a completed receipt and decisive certificate.

• Redundant exact-36 totalizer matched comparison.
  It is the cheapest test of whether global block-count propagation changes fixed-link tractability. · Generate with --add-block-count and run CaDiCaL -c 5000. · high · open
• Root-block-only constructive SAT calibration.
  It covers every link type and a SAT result directly settles the target. · Fix global block 01234, impose all point degrees 18 and all triple clauses, and run a matched bounded totalizer pilot. · normal · open
• Joint skeleton-and-distinguished-block certified exclusion.
  It is the sound route to a complete negative proof if constructive searches fail. · Enumerate and independently audit joint orbits before generating any UNSAT leaves. · normal · open

Objective: Measure whether redundant exact-36 propagation improves the fixed-link encoding enough to justify further compute.

First action: python3 scripts/fixed_link_extension_cnf.py generate --link artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt --add-block-count --output artifacts/fixed-link-extension-pilot-20260808/live-block-count.cnf

Stop condition: SAT advances to independent validation; replay-checked UNSAT closes this fixed link; no material telemetry improvement redirects to root-block-only constructive SAT.

• Generate the live instance with --add-block-count.
• Run the redundant-count instance under the same 5000-conflict CaDiCaL cap.
• Compare decisions, remaining variables, propagation, and elapsed time with experiment 20260808-165249-8bc1bd.
• Redirect to root-block-only constructive calibration if no material improvement appears.
• On SAT, decode and run both global checkers plus a separate fixed-model Z3 PB encoding.
• On UNSAT, provision and hash a proof checker before accepting any local exclusion.

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

GPT-5.6 Sol principal audited, implemented, and interpreted this epoch. Pre-existing GPT-5.6 Terra delegates supplied advisory reconnaissance; the relied-on fixed-link memo was promoted to sources/advisory/terra-fixed-link-extension-20260808.md and independently checked. Python 3.12.3 generated and checked artifacts; CaDiCaL 1.7.3 ran SAT controls and the bounded live calibration; web browsing checked current status and prior art. NetworkX 3.3 was used only for an unrecorded exploratory automorphism check and supports no claimed result. No CAS, proof assistant, lab job, external publication, or newly spawned delegate was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1158.6s

Review state

not a result claim

Attempt ID

covering-c1553-20260808-170047-690e25

No human review recorded.