Hash-owned root-link completion SAT on the second SHA-ranked type-(6,6,4^12) depth-four node, followed by a proved redundant-totalizer deletion and verifier-ready DIMACS repair.

certified root-link completion

Encode 1,998 residual 5-subset selectors using exact point-degree deficits and 59 uncovered-pair clauses, then seek a directly checked link or replayable UNSAT proof.

Hypothesis: The SHA-ranked index-one type-(6,6,4^12) depth-four root-link node either has a directly checkable twelve-block link completion or a replayable link-only UNSAT certificate within 60 solver seconds, 1 GiB, and 16 MiB of proof.

Test: Run pinned CaDiCaL 1.7.3 on an independently reconstructed canonical-header CNF; accept only a directly checked link or a complete DRAT converted to LRAT and replayed independently.

The only acceptable terminal observables were a directly checked link or a complete replayed proof. Neither occurred. The arithmetic reduction and pipeline defect are independently reproducible, but they do not satisfy the field contribution gate.

• The selected link formula's exact point-degree equations imply exactly eight residual blocks, making the separate exact-eight totalizer redundant.
• Deleting that totalizer reduces the formula from 38,904 variables and 174,660 clauses to 30,671 variables and 124,307 clauses without changing its Boolean models.
• The verifier-ready canonical formula's 16-MiB DRAT prefix does not derive a conflict and was reported NOT VERIFIED by fresh drat-trim.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/type2_rank1_link_completion_canonical_v1.py --out-dir artifacts/epoch103-20260812/type2-rank1-link-canonical-v1 --seconds 60 --proof-cap-bytes 16777216
• python3 checkers/check_type2_rank1_link_completion_canonical_v1.py --run-dir artifacts/epoch103-20260812/type2-rank1-link-canonical-v1 --out artifacts/epoch103-20260812/type2-rank1-link-canonical-independent-check.json
• Fresh drat-trim parsed 30,671 variables and 124,307 clauses, then reported 'c ERROR: no conflict' and 's NOT VERIFIED'.
• python3 checkers/check_epoch103_receipt_v1.py --out artifacts/epoch103-20260812/aggregate-independent-check.json returned PASS with no failures.

• .proof-experiments/20260812-003741-954f15: initial 38,904-variable formula hit the 16-MiB DRAT cap and returned UNKNOWN.
• .proof-experiments/20260812-003841-449e6a: proofless ten-second control returned UNKNOWN after 30,363 conflicts.
• .proof-experiments/20260812-004537-bb63bf: canonical-header reduced formula hit the 16-MiB cap and returned UNKNOWN.
• .proof-experiments/20260812-004552-5ce1ff: independent canonical reconstruction passed.
• .proof-experiments/20260812-004600-9007a4: fresh drat-trim explicitly rejected the canonical capped prefix.
• .proof-experiments/20260812-004810-c3eb3f: aggregate audit returned PASS.

The producer and checker use separate source files. The checker independently reconstructs the rank binding, candidate order, exact totalizers, degree targets, uncovered pairs, and canonical header. The canonical receipt reran byte-identically, and a separate aggregate checker passed.

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

• Certified link-orbit analysis for C(12,6,4) -> predict a smaller owned C(15,6,3) link cylinder -> observed a 30,671-variable canonical formula but nonterminal proof growth.
• Degree-conservation arguments -> predict a redundant global block-count constraint -> proved 5*sum(x_b)=40 and removed 8,233 variables plus 50,353 clauses.
• Formal certificate pipelines -> predict that parser compatibility must be tested independently -> fresh drat-trim exposed and then verified repair of the padded-header defect.

• The residual exact-degree constraints imply exactly eight selected residual blocks.
  Summing all point-degree equations yields 5*sum_b(x_b)=40. · The selected depth-four root-link completion encoding. · proved
• The canonical reduced formula has exactly 30,671 variables, 124,307 clauses, and 2,208,362 bytes.
  Producer metadata, two byte-identical clean-room reconstructions, and aggregate audit. · CNF SHA-256 57c7430a941666bdf1c3a12bb7527b7cf0f4dceb796e16a57b15969790bbd134. · computed
• The canonical 16-MiB DRAT prefix is not an UNSAT certificate.
  Fresh drat-trim reported no conflict and NOT VERIFIED. · DRAT SHA-256 6d49fc611eb79251aaf35088ff80079f3bc9cb125900e4ada99fe19549d74678 against the canonical CNF. · computed

• Use the exact-eight totalizer in this link encoding.
  Selected link-selector CNF and analogous exact-degree link encodings. · It is implied by the point-degree equations and adds 8,233 variables plus 50,353 clauses. · Degree-sum proof and independent formula reconstruction. · Only an encoding without all exact point-degree equations would require a separate count constraint.
• Use zero-padded DIMACS headers as a replayable drat-trim certificate base.
  The inherited Cnf writer and pinned drat-trim parser. · drat-trim misparsed the padded integer fields. · Fresh parser control followed by successful parsing of the canonical unpadded header. · A different pinned parser with independently verified padded-decimal semantics.
• ASCII DRAT under the 16-MiB cap classifies the selected node.
  CaDiCaL 1.7.3, seed 0, -P0, canonical reduced CNF, 60-second solver limit. · The proof hit exactly 16 MiB after 5.55 seconds before a terminal status. · Canonical producer receipt and explicit drat-trim rejection. · A materially different proof format, segmented certificate design, solver, or encoding.
• Infer link infeasibility or C(15,6,3)=31 from this epoch.
  Selected node and global target. · No terminal SAT or UNSAT result exists. · All producers are UNKNOWN; aggregate audit records global_covering_bound_changed=false. · A directly checked link/cover or complete independently replayed proof with exhaustive ownership.

• Binary-DRAT storage discriminator on the canonical reduced formula.
  It changes proof compression without changing semantics or increasing the certificate cap. · Run default binary DRAT for 60 seconds under the same 16-MiB cap and fresh conversion/replay gate. · high · open
• Canonical complete-link catalogue above the rank-one node.
  Direct canonical augmentation may classify link completions without storing a large SAT proof prefix. · Enumerate with a 10,000-node/120-second cap and independently compare every child-parent ownership relation. · normal · open
• Materially different exact-degree-12 constructive search.
  A directly checked 30-block witness remains the smallest terminal certificate. · Define a global exchange or alternate encoding outside the exhausted local and six-representative protocols, then apply a short witness gate. · normal · open

Objective: Determine whether binary DRAT makes the verifier-ready rank-one link cylinder certifiable under the unchanged storage budget.

First action: Run CaDiCaL 1.7.3 on artifacts/epoch103-20260812/type2-rank1-link-canonical-v1/link.cnf with default binary DRAT, seed 0, -P0, 60 seconds, 75-second watchdog, 1 GiB, and a 16-MiB cap.

Stop condition: Close the selector-CNF route on cap hit, UNKNOWN, conversion failure, reconstruction drift, or replay rejection; promote only a checked link or complete proof.

• Run binary DRAT on the canonical-header reduced CNF under the unchanged 16-MiB and 60-second limits.
• If binary DRAT is nonterminal, close this selector-CNF proof route rather than increasing the cap.
• Then implement a canonical full-link catalogue with independently checked child-parent ownership and a 10,000-node or 120-second gate.
• Keep native PB blocked until pinned RoundingSat, VeriPB, and CakePB sources and executables satisfy the recorded reopen condition.

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

GPT-5.6 Sol was principal investigator. Two pre-completed GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; their exact promoted files were audited and were not independent validators. Deterministic work used Python 3.12.3, CaDiCaL 1.7.3 seed 0, GCC, freshly built drat-trim, exact integer/set arithmetic, SHA-256, and the computational-researcher experiment harness. Web search checked LJCR, the Covering Repository context, arXiv:2607.23766, and arXiv:math/9502238. No complete LRAT proof, native PB solver/checker, CAS, cloud lab, external proof service, human validator, system installation, publication, or external write was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1421.8s

Review state

not a result claim

Attempt ID

covering-c1563-20260812-005158-ed0001

No human review recorded.