A predeclared 256-cell min-hash-stratified usefulness pilot for exact demand-aware maximum-recovery LP dual certificates, with full-sort independent sampling reconstruction.

demand-aware loss-mask recovery LP

Relax each strict five-addition completion to fractional outside-seed block weights with exact point demand, maximize capped recovered triples, and use an exact dual to lower-bound residual defect.

Hypothesis: At least 52 of the 256 predeclared sampled deletion cells have an exactly certified integer residual-defect lower bound at least 10, with median LP solve time at most 0.05 seconds and median normalized certificate size at most 32768 bytes.

Test: Select 16 minimum-hash cells in each of 16 contiguous lexicographic-rank strata, solve all 256 sparse LPs plus two controls, and require an independent full-sort sampler and exact rational replay of every primal and dual constraint.

Every legal five-addition completion embeds in the fractional primal, and exact dual feasibility bounds its recovered triples. Independent replay therefore validates each local lower bound. Because the experiment covers only a hash-selected local sample around one non-cover seed, it is progress and reusable infrastructure, not a covering-number candidate.

• For every one of the 256 hash-bound sampled deletion cells, every legal exact-degree five-addition completion has residual defect at least 11.
• The exact sampled integer lower-bound histogram is {11:1,13:2,14:2,15:7,16:15,17:32,18:43,19:34,20:43,21:39,22:24,23:9,24:4,25:1}.
• The predeclared usefulness gate passes with 256/256 cells at least 10, median producer solve time 0.01844978309236467 seconds, and median normalized certificate size 5887.5 bytes.
• The maintained exact range remains 54 <= C(15,5,3) <= 55.

• Producer experiment 20260811-185610-fe9688 returned the exact histogram, 256/256 threshold yield, median 0.01844978309236467-second solve time, and 5887.5-byte median certificate.
• Independent experiment 20260811-185705-dfae32 returned valid=true after a full-sort sampler reconstruction and 373112 exact dual block inequalities.
• Mutation experiment 20260811-185829-67f4e9 rejected all seven predeclared sampler and certificate corruptions.
• Regeneration experiment 20260811-190008-72d374 reproduced selection.jsonl, certificates.jsonl, and toolchain.json byte-for-byte.
• sha256sum -c artifacts/degree18-demand-recovery-lp-usefulness-pilot-20260811/manifest.sha256 passes.

• .proof-experiments/20260811-185610-fe9688: producer generated 256 sampled certificates and controls; all count, timing, and size gates passed.
• .proof-experiments/20260811-185705-dfae32: independent checker reconstructed all sampler ranks and replayed 373112 dual inequalities.
• .proof-experiments/20260811-185829-67f4e9: seven sampler and certificate mutations were rejected.
• .proof-experiments/20260811-190008-72d374: selection and certificate artifacts regenerated byte-identically.

checkers/check_degree18_demand_recovery_lp_usefulness_pilot_v1.py imports neither the producer, SciPy, NumPy, nor any solver. It fully sorts each rank stratum, reconstructs every demand, uncovered triple, and eligible block, and checks exact Fraction primal-dual feasibility, objectives, residual ceilings, hashes, counts, and certificate sizes.

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

• Maximum-coverage LP duality -> predict cheap exact pruning of strict local-repair cells -> observed 256/256 sampled cells certified worse than the defect-10 seed with small exact certificates.
• Min-hash stratification from residual-state sampling -> predict a reproducible non-lexicographic usefulness sample -> independent full sorting reproduced every selected cell and hash.

• All 256 selected strict-five deletion cells have certified integer residual-defect lower bound at least 11.
  certificates.jsonl SHA-256 3c5020b01b6f6aa8f812f424dbe3d681426bba4dcc22b535279b203c0799103c; independent-check.json valid=true with 373112 inequalities. · Exactly the selection.jsonl cells around the locked degree-18 defect-10 seed, with additions restricted to five distinct outside-seed blocks satisfying exact point demand. · computed
• The exact sampled integer residual-bound histogram ranges from 11 to 25 with counts recorded in result.json.
  Independent checker reconstructed the histogram and all per-cell rational residual ceilings. · The fixed 256-cell sample only. · computed

• Repeat the complete fixed-pair-link strengthening recommended by the injected tactical brief.
  Link-only requirements in all four canonical degree-18 CNFs. · Epoch 70 independently classified all 5460 requirements as fixed-block tautologies or exact baseline coverage clauses, giving zero logical clause delta. · artifacts/pair-link-cnf-delta-audit-20260811/independent-check.json valid=true. · A new pair-count, skeleton, or other labelled semantic constraint with an independently checked positive formula delta.
• Use any of the 256 selected strict-five deletion cells to find a five-addition family of defect at most 10.
  The exact selected cells and strict outside-seed, exact-demand five-addition model. · Every cell has an exact LP-dual integer residual lower bound at least 11. · independent-check.json and certificates.jsonl. · A checker error, hash mismatch, or a completion outside the stated strict-five model; none is currently known.

• Batched integer replay and certificate compression for the recovery-LP route.
  The 256-cell yield is decisive locally, but naive all-cell validation would require billions of Fraction inequalities and roughly 18.6 GB at the observed median certificate size. · Clear denominators per certificate, verify all current inequalities with packed integer kernels, compress normalized certificates, and require exact agreement with the existing checker plus a measured full-census projection. · high · open
• Globally complete proof-producing SAT with a materially new decomposition or semantic cut.
  This remains the terminal negative route, but current canonical branches are solver-UNKNOWN and stale link constraints add zero information. · Run one matched proof-smoke pilot only after specifying and independently validating a positive semantic or decomposition delta. · normal · open
• Constructive exact-degree search beyond strict five-for-five moves.
  A 54-cover is the shortest terminal positive certificate, while the current seed has defect 10 and the sampled radius-five basin is frozen. · Design a bounded radius-six or ejection-chain move family with incremental exact coverage deltas and stop unless it beats defect 10 under independent replay. · normal · open

Objective: Decide whether a complete strict-five local-optimality certificate can be made independently checkable at reasonable artifact size and validation cost.

First action: Implement a denominator-cleared batched checker for artifacts/degree18-demand-recovery-lp-usefulness-pilot-20260811/certificates.jsonl and compare its exact per-cell outputs and wall time against experiment 20260811-185705-dfae32.

Stop condition: Redirect if any result disagrees, mutation controls survive, projected full-census validation remains billions of slow rational operations, projected compressed evidence is impractical, or the human owner declines the exact local-optimality scope.

• Do not extrapolate the 256/256 sample result to the other 3162254 cells or to the global covering problem.
• Implement denominator-cleared batched exact replay and transparent compressed storage on the existing 256-certificate corpus.
• Request human approval of the exact full-census scope before submitting a checkpointed all-cell lab job, and only if validation time and artifact size are tractable.
• Preserve proof-producing globally complete SAT and constructive defect reduction as the terminal resolution 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 ↗
• https://arxiv.org/abs/math/9502238 ↗

Codex GPT-5 Sol acted as principal investigator. Two GPT-5.6 Terra delegates supplied advisory route reconnaissance and verification design only; their agreement was not evidence. Deterministic work used Python 3.12.3, NumPy 1.26.4, SciPy 1.11.4 with HiGHS, sparse matrices, standard-library Fraction arithmetic, SHA-256, mutation testing, the computational-researcher experiment harness, and pre-acquired/live source checks. No sub-agents were spawned by Sol; no lab job, SAT solver, proof assistant, external write, publication, package installation, system change, or Git operation was performed.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1505.9s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260811-191051-998375

No human review recorded.