[queelius]

Change and mathematical scope

Independent verification of PR #6141's characteristic-five exclusion. Adds only research/connector-c5-certificate/: a hash-bound 4,278-variable / 52,672-clause CNF, a compressed trimmed DRAT certificate, a written word-to-CNF implication and a self-contained native replay. Already the sixteen masks of weights two and six are impossible for a length-30 word on six sources, each occurring five times.

This strengthens the evidence for the existing claim; it does not claim a new exclusion, new κ, supplier admission, or a result for deeper blocks/arbitrary floor words. PR6141 remains separately partially reviewed in the ledger.

Task and overlap

Explicitly assigned scope key: connector-c5-proof-certificate; unchanged mathematical scope, following PR6141's open-next-question 2. Base main: a5bff3bf133e482541c09eba4e773884bdb2b1b7. Predecessor: d192172f57b10647ddcff9410c69d48ac06862c1. Contribution head: dd43e856dceec9a92d338345d01d4ad247ce2172.

Coordination claim. Refreshed targeted PR searches, PR6141 comments, main and recent handoffs before submission; no competing certificate was found within this bounded coverage. No characteristic-seven search was launched.

Validation

From the package directory, install requirements.txt in a virtual environment, then:

python -O reproduce.py
python -m unittest -q test_checks test_reproduce test_native test_generate

Expected JSON status: PASS_CONNECTOR_C5_CERTIFICATE, DRAT s VERIFIED, corrected LRAT c VERIFIED, three native rejecting controls, and 19 passing tests. Both normal and optimized complete replays passed. Linux x86_64, Python 3.13.15, GCC 13.3, python-sat 1.9.dev15. The last normal replay took 172.029s for DRAT conversion and 19.71s for LRAT. The compressed proof is 38,506,051 bytes; allow roughly 2 GB temporary disk.

The written implication accounts for relabeling, weight pruning, boundary 30→0, repeated reads and all twelve anonymous counter blocks. Tests cover all 116 small floor words in the stated three domains, constructive counter assignments and a satisfiable weight-two-only relaxation. Owned Python coverage is 93% combined; the bridge helper is 100%. Coverage limits are explicit.

A rejecting control exposed the known LRAT empty-clause bug (drat-trim issue42). The wrapper failed closed. Final replay uses haskiindahouse's exact existing PR43 correction, head 0ca925b4f5b4ed04d02d830807cfd614483e7320, retaining the original source and regression. This is neither a new checker fix nor a complete checker audit. Earlier uncorrected LRAT positive output is explicitly not relied on.

One scoped AI reviewer checked the encoding bridge and wrappers, found that dependency failure, and the response was verified by the author. No human peer review or Lean/kernel verification is claimed. No selected cold replay, repository-wide suite or hosted scientific CI was run. This is a standalone native/PySAT replay; the generic replay manifest supports only numpy/sympy/scipy pins, so no unsupported registration was added.

Credit

Alexander Richard Towell, with substantial OpenAI Codex assistance. Josie Elliston supplied PR6141's encoding, exclusion and controls; Nick Petalas supplied the interface and prior connector bounds, with zxv, apoursh, Ross Richardson and retained lineage. Credit haskiindahouse's checker correction, Marijn Heule/Nathan Wetzler, PySAT/CaDiCaL and the Sinz/Knuth/Alex Healy counter lineage. Apache-2.0 contribution; vendored MIT checker licenses and notices retained.

Open next questions

See the package README: a separately budgeted characteristic-six certificate, or an elementary proof removing encoding/tool trust. Characteristic seven and other architectures remain outside this contribution; none is an automatic next cycle.

Durable archive

The exact 47-file source snapshot at the contribution head is archived as version 0.1.0: 10.5281/zenodo.23777615. All three public deposited files and every source ZIP member were downloaded and hash-verified. The archive retains original predecessor credit and historical failed logs; the outer note records the later submission/publication event. DOI publication is separate from upstream acceptance or human peer review.

[queelius]

Response to the intake question on logs/reproduce-optimized.json (reviewed head dd43e85):

The empty file was the first optimized replay, run with the original lrat-check before the packet switched to the PR43 checker. reproduce.py stopped at its satisfiable-formula control because that checker accepted a fake refutation (drat-trim issue 42). That is the fail-closed outcome the README describes. The exception was raised before any JSON was printed, so the redirected receipt was empty, and its stderr (FAIL: satisfiable formula falsely refuted) is retained beside it.

Commit f5ebae0 replaces the empty file with a valid JSON record that classifies it as that retained failure (relied_on: false) and names the passing receipts: reproduce-normal.json, reproduce-pr43-optimized.json and reproduce-fixed-optimized.json. No other file changed, and nothing referenced the empty file.

Alexander Richard Towell, with Anthropic Claude (Claude Code)