Proof-core-guided necessary filtering of a deterministic 288-cell sample from the strict five-for-five repair neighborhood of one defect-10 degree-18 seed.

proof-core-guided layer-five filtering

Use proof-selected coverage and point-balance rows as a sound necessary filter, compress sampled deletion cases with selector variables, and certify the resulting union CNF by DRAT-to-LRAT replay.

Hypothesis: At least 36 of 288 deterministic layer-five deletion cells are proof-certifiably infeasible under the proof-selected necessary rows, with median decision time at most 0.25 seconds.

Test: Solve a shared-selector union CNF for the 288 cells, independently reconstruct every clause, and require successful DRAT/LRAT replay plus rejection against a satisfiable wrong-formula control.

Every valid repair within a sampled deletion cell would satisfy the encoded necessary rows. The complete disjunction of those cells is UNSAT under independently reconstructed semantics and kernel-replayed proof logs. Scope guards prevent extrapolation beyond the named cells.

• All 288 hash-bound sampled deletion cells are infeasible under the nine-point, 326-coverage-row necessary relaxation.
• The union CNF has 74,073 variables and 344,169 clauses and SHA-256 7babc18e7a4143eda9ee4b84f7e303364bf3e955b61392bfff9948fd03b87fc6.
• The maintained global range remains 54 <= C(15,5,3) <= 55.

• python3 checkers/check_core_guided_layer5_union_cnf_v1.py reconstructed all 344,169 clauses exactly.
• CaDiCaL 1.7.3 returned UNSAT and produced union.drat.
• drat-trim reported VERIFIED and emitted union.lrat.
• lrat-check reported VERIFIED on the exact union CNF.
• CaDiCaL reported SAT on the selector-dropped control, and lrat-check reported NOT VERIFIED against it.
• sha256sum -c artifacts/core-guided-layer5-filter-pilot-20260810/manifest.sha256 passed every entry.

• .proof-experiments/20260810-050826-81c758: failed closed because discrete midpoint binning left an empty stratum.
• .proof-experiments/20260810-050934-345fe7: corrected 288-cell Z3 pilot returned 288 unverified UNSAT answers; median 0.0118379439 seconds.
• .proof-experiments/20260810-051526-727ee6: first independent union checker failed on an incorrect strict zip over n versus n+1 layers.
• .proof-experiments/20260810-051556-df2e08: corrected independent checker reproduced 74,073 variables and 344,169 clauses exactly.
• .proof-experiments/20260810-051652-fa5fa4: CaDiCaL returned UNSAT and emitted the complete DRAT proof.
• .proof-experiments/20260810-051723-57533c: drat-trim verified DRAT and emitted LRAT.
• .proof-experiments/20260810-051855-6d4255: lrat-check verified the LRAT proof.
• .proof-experiments/20260810-051855-a968f8: selector-dropped wrong formula was SAT.
• .proof-experiments/20260810-051856-8f6472: locked LRAT proof was rejected against the wrong formula.
• .proof-experiments/20260810-052341-10d396: complete packet manifest integrity check passed.

check_core_guided_layer5_filter_v1.py independently reconstructs the 288-cell sample and cell semantics. check_core_guided_layer5_union_cnf_v1.py independently rebuilds every union-CNF clause. lrat-check separately replays the final proof, and a selector-dropped SAT control tests formula binding.

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

• DRAT proof-core selection -> predict that proof-used invariant rows prune count-five repair cells -> all 288 sampled cells were certified infeasible.
• Multi-case SAT selector encoding -> predict that shared counters can compress hundreds of branches into one proof surface -> 288 branches fit in one 74,073-variable CNF with one replayed proof.
• Wrong-formula proof binding -> predict that removing the branch-activation clause makes the control SAT and invalidates the proof -> both signals occurred.

• All 288 sampled deletion cells are infeasible under the selected necessary relaxation.
  certified-result.json, independently reconstructed union.cnf, and kernel-verified union.lrat · The exact hash-bound 288 cells only. · computed
• The selector-dropped control formula is satisfiable.
  CaDiCaL SAT result in experiment 20260810-051855-a968f8. · wrong-no-selector.cnf SHA-256 a0bc235367a502eb8be327f7f6d42874768eadd5efeb4d8aa6df164242ae1aa1. · computed
• The proof is bound to the selector-bearing formula.
  lrat-check verified the intended formula and rejected the selector-dropped formula. · Union LRAT SHA-256 6aba943024632bd33b845bfa2428aec2b32cf36f4209a140148cfbe99e4188d0. · computed

• Treat the initial 288 Z3 UNSAT answers as exclusions without proof replay.
  All sampled cells before union-proof construction. · The fail-open protocol counted every unverified UNSAT as retained. · result.json and independent-check.json initially recorded certified_unsat=0 and fail_open_retained=288. · A proof-capable equivalent encoding, independent reconstruction, and successful proof replay. · The shared-selector CNF and verified LRAT proof subsequently satisfied this condition.
• Extrapolate the 288/288 sampled rejection rate to all count-five repairs or all 54-block families.
  Unsampled deletion cells and global C(15,5,3). · The sample is a deterministic discriminator, not a statistical sample with an inference model, and the search is local to one seed. · Protocol and certified-result scope guards. · A complete independently checked partition covering every deletion cell for the local claim, and a globally complete case split for any statement about C(15,5,3).

• Complete strict five-for-five deletion-cell filter around the fixed seed.
  The 288-cell pilot passed both pruning and median-time gates. · After human scope approval, build one immutable selector batch and measure proof throughput before checkpointed lab submission. · high · open
• Globally complete pair-normalized proof-producing SAT.
  It retains terminal global scope, unlike the local repair filter. · Test one materially different proof-preserving encoding against the best audited branch at a matched cap. · normal · open
• Variable-length exact-degree constructive ejection chains.
  A directly checked defect below 10 would escape the current local basin and reopen constructive search. · Specify a new move generator and run a bounded below-10 discriminator. · low · open

Objective: Decide whether to scale the local filter or redirect to a globally scoped route.

First action: Review records/attempts/epoch-0044-core-guided-layer5-filter-20260810.json and the proposed successor scope in CHECKPOINT.md.

Stop condition: Hold without human approval; redirect if a representative proof batch exceeds the declared resource plan or any producer/checker/proof binding disagrees.

• Have the human owner approve or reject the proposed complete strict five-for-five neighborhood scope.
• If approved, design one immutable proof-producing selector batch and measure construction, solving, proof size, and replay throughput before full lab dispatch.
• Retain globally complete pair-normalized SAT and constructive variable-length ejection chains as alternative routes.

• 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/2607.23766 ↗

GPT-5.6 Sol principal independently selected, designed, implemented, audited, and interpreted the epoch. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance; the used memo was promoted with provenance and model agreement was not validation. Deterministic tools were Python 3.12.3, Z3 4.13.0, CaDiCaL 1.7.3, drat-trim, lrat-check, sha256sum, and the computational-researcher experiment wrapper. No CAS or proof assistant was used, no new sub-agent was spawned, and no successor lab job was dispatched.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1758.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-052658-05074b

No human review recorded.