Combined the audited global incidence CNF with the exact five-way root-link degree partition, materialized the asymmetric (8,4^13) cube, and ran a proof-producing 20-second CaDiCaL discriminator with independent semantic and proof-replay checks.

proof-producing root-profile incidence cube decomposition

Normalize one point as a root, split its 12 incident and 18 nonincident block columns, fix one of five link-degree profiles, sort columns within both groups, and search the resulting exact incidence CNF.

Hypothesis: The proof-compatible asymmetric (8,4^13) root-profile incidence cube yields terminal SAT or UNSAT evidence within 20 seconds, or materially shrinks the proof-oriented state relative to the epoch-9 second-block cubes.

Test: Generate the exact cube, run CaDiCaL 1.7.3 for 20 seconds in LRAT mode, independently reconstruct every added clause, and require direct witness validation or source-pinned dual proof replay before interpreting a terminal result.

The formula and decomposition are independently checkable infrastructure progress, and the proof-plumbing defects were reproduced and corrected. However, UNKNOWN plus a dual-rejected partial proof establishes no SAT or UNSAT claim, and the mixed preprocessing change does not justify scaling the unchanged route.

• The corrected selected-profile formula has exactly 33,661 variables and 158,679 clauses and SHA-256 f097917339695d6032b5e13ecc3008aab417ac9b41865b4f80d4e2223da70e48.
• Every putative 30-cover can be represented in at least one of the five root-link degree profile families after relabeling.
• The (8,4^13) run remained UNKNOWN after the declared 20-second limit and excludes no cover.
• The 6,548,972-byte partial LRAT was not accepted by either pinned proof-verification condition after lrat-check parsed the exact formula dimensions.
• The exact covering range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/root_profile_incidence_pilot_v1.py --out-dir artifacts/epoch49-20260810/root-profile-incidence-pilot-v2 --seconds 20
• python3 checkers/check_root_profile_incidence_pilot_v1.py --artifact-dir artifacts/epoch49-20260810/root-profile-incidence-pilot-v2 --receipt artifacts/epoch49-20260810/root-profile-incidence-checker-receipt-v6.json
• python3 checkers/check_root_profile_receipt_determinism_v1.py --artifact-dir artifacts/epoch49-20260810/root-profile-incidence-pilot-v2 --canonical-receipt artifacts/epoch49-20260810/root-profile-incidence-checker-receipt-v6.json --out artifacts/epoch49-20260810/root-profile-receipt-determinism-v2.json
• Epoch receipt hash audit passed for 13 declared files.

• .proof-experiments/20260810-094228-c8091a: corrected proof-compatible cube, UNKNOWN after 20 seconds with 5,000 conflicts
• .proof-experiments/20260810-094844-59c00c: source-pinned independent checker PASS; partial LRAT not verified
• .proof-experiments/20260810-094854-dcf942: two clean normalized checker receipts were byte-identical

checkers/check_root_profile_incidence_pilot_v1.py independently reconstructs the inherited core and complete root-profile suffix with a pure-list encoding, enumerates the five profiles, rejects three mutations, binds lrat-check and CakeLPR source hashes, and fails closed on UNKNOWN. check_root_profile_receipt_determinism_v1.py verifies byte-level receipt reproducibility.

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 extremal-link decompositions for C(12,6,4) -> predict that link-conditioned cubes can support proof leaves -> the coarse root-degree cube was exact but delivered only a 1.652% retained-variable reduction and no terminal signal.
• Proof-certificate engineering -> predict that syntactically valid DIMACS is sufficient for replay -> falsified for zero-padded headers because the retained lrat-check uses %i and interprets leading zeroes as octal.

• The root-link degree multiset of a chosen point in any putative 30-cover is one of exactly five profiles.
  Each of fourteen link degrees is at least 4, their sum is 60, and independent stars-and-bars enumeration gives five partitions of four excess units. · Every chosen root point in every putative 30-block (15,6,3) cover · proved
• The corrected (8,4^13) formula has 33,661 variables and 158,679 clauses.
  Formula SHA-256 f097917339695d6032b5e13ecc3008aab417ac9b41865b4f80d4e2223da70e48 and independent full-clause reconstruction · The selected normalized root-profile cube · computed
• The selected 20-second solver run was nonterminal.
  CaDiCaL exit 0, UNKNOWN receipt, and both proof acceptance conditions false · Seed 0, CaDiCaL 1.7.3, selected formula, 20-second limit · computed
• Unpadded decimal DIMACS headers are required for correct dimension parsing by the retained lrat-check.c.
  The padded formula was parsed as 14,257 variables and 13 clauses; the corrected formula was parsed as 33,661 variables and 158,679 clauses. · The retained lrat-check.c scanf %i header parser · computed

• Scale all five root-profile cubes using the unchanged totalizer/global-core CNF.
  The current encoding family calibrated on the (8,4^13) cube · No terminal signal; only 1.652% fewer retained variables and 1.339% more retained clauses than the prior branch. · solver-receipt.json, cadical.log, and epoch-9 matched preprocessing dimensions · A matched encoding reduces retained variables or clauses by at least 10% without worsening the other dimension, or produces terminal evidence.
• Use zero-padded DIMACS headers in proof-replay artifacts.
  Artifacts replayed by the retained lrat-check.c · The %i parser interpreted leading-zero fields as octal and did not parse the declared formula. · Padded versus corrected exact-dimension replay control · Replace the checker with a source-pinned parser that demonstrably treats header fields as decimal, with regression tests.
• Treat the incomplete LRAT prefix as an exclusion.
  The selected (8,4^13) 20-second run · Both verifier acceptance conditions were false. · root-profile-incidence-checker-receipt-v6.json · A complete proof accepted by both source-pinned verification paths.

• Fixed complete C(14,5,2) root-link constructive completion
  It reduces the primary incidence representation from 450 to 252 variables and can directly return a terminal 30-block witness. · Verify one complete link and compile its 18-co-block/247-residual-triple completion CNF. · high · open
• Compressed proof-producing global incidence/PB formulation
  A materially different PB or selector encoding may enforce link degrees without the 2,196-clause totalizer overhead. · Compile only the selected profile and compare preprocessing against the exact 29,885-variable/158,097-clause reference. · normal · open
• Constructive search outside the closed C5-invariant neighborhood
  A directly checked witness settles the target at 30, but another run requires a new decomposition rather than a larger arbitrary cutoff. · Derive a new tail or anchor decomposition with a measured bulk reduction before search. · low · open

Objective: Test whether one fixed complete root link permits a compact constructive 18-co-block completion search.

First action: Hash-audit a retained or published 12-block C(14,5,2) link and directly verify all 91 pairs before encoding.

Stop condition: Redirect on link identity or coverage failure, invalid SAT model, UNKNOWN without material state reduction, or any attempt to treat one-link UNSAT as global.

• Hash-audit and directly verify one complete 12-block C(14,5,2) root link.
• Compile its 18-co-block completion problem using 252 primary membership variables and 247 residual triple rows.
• Write a separate checker that validates the fixed link, formula semantics, and any returned 30-block cover.
• Run one 30-second witness-oriented pilot; do not extrapolate single-link UNSAT globally.

• 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://www.dmgordon.org/papers/cover.pdf ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol was principal investigator, performing audit, design, implementation, execution, and interpretation. GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; their agreement was not validation, the already-known five-profile suggestion was not claimed as new, and the replication-only rank-1 replay suggestion was rejected. Deterministic tools used were CPython 3.12.3, CaDiCaL 1.7.3, GCC 13.3.0, lrat-check, CakeLPR, exact integer arithmetic, SHA-256, and the Proof Factory experiment harness. Browser access attempted the supplied primary/current URLs but returned no extract. No CAS, proof assistant, cloud lab, external proof service, human validator, or external publication was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1363.9s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-095232-af3e50

No human review recorded.