Qualify pinned DRAT-to-LRAT certificate transport on the previously certified epoch-74 11-row UNSAT cylinder, then compare it exactly with direct LRAT emission.

proof-producing incidence/PB cube decomposition

Fresh CPU-pinned CaDiCaL DRAT emission, pinned drat-trim conversion, dual LRAT replay, semantic mutation controls, and a matched byte comparison against direct LRAT for the identical CNF.

Hypothesis: Pinned drat-trim converts a fresh CaDiCaL DRAT proof for the certified 11-row UNSAT control into dual-replayable LRAT, and the converted certificate is no larger than direct LRAT for the identical CNF.

Test: Generate one fresh terminal DRAT on the known 57-conflict control, convert and replay it, reject four mutations, and compare exact bytes with the retained direct LRAT.

Explicit converter verification, byte-identical independent conversion, two replay kernels, and mutation controls establish the scoped infrastructure claim. Exact matched byte counts falsify the proposed certificate-size advantage. The input was already known UNSAT and covers no complete frontier, so no mathematical bound changes.

• For the exact hash-bound epoch-74 child-1 CNF, CaDiCaL 1.7.3 generated a 13270-byte DRAT proof that pinned drat-trim verified.
• Pinned drat-trim converted that DRAT proof into a 185277-byte LRAT accepted by both legacy lrat-check and CakeLPR.
• An independent -O1 build reproduced the converted LRAT byte-for-byte and rejected four independently regenerated mutations.
• The converted LRAT is 54005 bytes larger, or 1.4113977085745628 times the size, of the direct LRAT for the identical CNF.
• No covering-number bound changed.

• python3 scripts/drat_lrat_transport_v1.py --out-dir artifacts/epoch79-20260811/drat-lrat-transport-v1-final --seconds 2 --proof-cap-bytes 8388608
• python3 checkers/check_drat_lrat_transport_v1.py --artifact-dir artifacts/epoch79-20260811/drat-lrat-transport-v1-final --out artifacts/epoch79-20260811/drat-lrat-transport-v1-final/independent-check-v2.json
• Producer harness 20260811-073007-808650 returned 0 under 90 seconds and 1024 MiB.
• Independent harness 20260811-073311-013fbb returned 0 under 90 seconds and 1024 MiB.
• Final hash audit passed all 15 manifest entries.

• .proof-experiments/20260811-073007-808650: final producer passed; DRAT 13270 bytes and converted LRAT 185277 bytes.
• .proof-experiments/20260811-073311-013fbb: independent checker passed; conversion was byte-identical and matched size gate failed.
• .proof-experiments/20260811-072748-ba2131: failed safely because UNSAT status was read from stdout instead of the witness file.
• .proof-experiments/20260811-072843-763b4c: three mutations rejected, but deletion of only DRAT's final empty line still verified; control was strengthened.
• .proof-experiments/20260811-073033-3a6795: independent -O0 build failed before proof use because pinned lrat-check.c does not link at -O0; -O1 was used.

artifacts/epoch79-20260811/source-v1/check_drat_lrat_transport_v1.py; it does not import the producer, compiles tools at -O1 instead of -O2, independently converts and mutates proofs, and replays with legacy lrat-check and CakeLPR.

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

• Compact SAT proof transport -> predict DRAT conversion will reduce final replayable-certificate size -> DRAT itself was compact, but converted LRAT was 41.14% larger than direct LRAT, falsifying the transfer on this control.

• The pinned DRAT-to-LRAT stack accepts the intact fresh certificate under two LRAT replay kernels.
  producer-receipt.json and independent-check-v2.json · Exact epoch-74 child-1 CNF and epoch-79 proof bytes · computed
• Converted LRAT is 185277 bytes versus 131272 bytes for direct LRAT.
  independent-check-v2.json matched_size_comparison and hash-bound proof files · Identical CNF, CaDiCaL 1.7.3 seed 0, pinned drat-trim · computed
• All four final semantic mutations are rejected.
  Independent producer and checker controls · Ten-line DRAT suffix deletion, LRAT final-line deletion, poisoned LRAT hint, and deleted CNF clause · computed

• Scale unchanged DRAT-first conversion because it produces smaller final LRAT certificates than direct LRAT.
  The exact matched epoch-74 child-1 control under the pinned toolchain · Converted LRAT was 1.4113977085745628 times direct LRAT. · artifacts/epoch79-20260811/drat-lrat-transport-v1-final/independent-check-v2.json · A pinned converter mode or materially different formula family that beats direct LRAT under dual replay, or a demonstrated solver-output bottleneck where compact DRAT is decisive.
• Use deletion of only DRAT's final empty-clause line as a universal rejection control.
  The fresh epoch-79 ASCII DRAT proof · The truncated proof still verified because prior units exposed the contradiction. · Failed harness 20260811-072843-763b4c and measured suffix boundary · A proof-specific dependency audit showing the removed line is necessary, or use a stronger semantic mutation.

• Whole-profile dominance audit on the exactly-owned fixed-first q>=5 frontier
  It is a deterministic, cheap test for reusing retained terminal proofs over complete owned cells rather than overlapping local cylinders. · Compare exact profile constraints from the epoch-44 manifest with epochs 69-74 terminal predicates and independently check every implication. · high · open
• Materially changed constructive incidence search
  A 30-block witness would settle the target directly, but the frozen six-representative scan is exhausted as a short control. · Design a new encoding or invariant that changes propagation dimensions before any solver tranche. · normal · open
• DRAT as solver-output transport rather than final certificate compression
  DRAT was only 10.11% of direct LRAT, so it could matter if solver-side proof I/O becomes the measured bottleneck. · Only after observing an actual direct-LRAT I/O failure, compare solver wall time and peak proof traffic on a matched exactly-owned leaf. · low · open

Objective: Determine whether retained terminal equality predicates eliminate any entire unresolved profile in the exactly-owned fixed-first q>=5 frontier.

First action: Implement scripts/audit_fixed_first_terminal_dominance_v1.py against the hash-pinned epoch-44 249-profile manifest and epochs 69-74 predicates, with a separate implication checker.

Stop condition: Redirect if no whole profile is eliminated, if predicates are incomparable, or if profile ownership or implication cannot be proved exactly.

• Implement a hash-bound implication audit from epochs 69-74 terminal predicates to the exactly-owned fixed-first q>=5 profile frontier.
• Require elimination of at least one entire unresolved profile before any new proof-producing solver run.
• Use direct LRAT as the certificate-size incumbent; retain DRAT transport only as an I/O fallback.
• Do not repeat the frozen six-representative UNKNOWN scan without a material encoding or ownership change.

• 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/math/9502238 ↗
• https://github.com/marijnheule/drat-trim/tree/2e3b2dc0ecf938addbd779d42877b6ed69d9a985 ↗

GPT-5.6 Sol was principal investigator. Two pre-completed GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; Sol independently audited, implemented, tested, and interpreted all relied-on claims, and model agreement was not validation. Deterministic tools were CPython 3.12.3, CaDiCaL 1.7.3, GCC, pinned drat-trim at revision 2e3b2dc0ecf938addbd779d42877b6ed69d9a985, legacy lrat-check, CakeLPR, SHA-256, exact file parsers, and the computational-researcher experiment harness. Web search checked current sources and the official converter repository. No CAS, PB solver/checker, proof assistant beyond the CakeLPR replay kernel, cloud lab, external proof service, or human validator produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1361.7s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-073856-b9377a

No human review recorded.