Compile and proof-calibrate the smallest live combined incidence cell r=0,q=3 using the unique minimum-intersection owner and exact internal pair-excess counter.

proof-producing incidence/PB cube decomposition

Fix F=012345 and the disjoint representative 67891011, then append an exact totalizer requiring 63 incidences among the 450 internal-pair support variables and run proof-producing CaDiCaL.

Hypothesis: The smallest live combined cell r=0,q=3 terminates within five solver seconds with either a directly checkable 30-cover or a dual-replayable UNSAT proof.

Test: Run seed-0 CaDiCaL 1.7.3 on CPU 0 with external LRAT, a nominal five-second limit, and a 4 MiB proof cap; directly check SAT or replay UNSAT independently twice.

UNKNOWN and explicit proof rejection provide no SAT witness or UNSAT certificate. They do provide a reproducible fail-closed reason not to scale this unchanged proof-cell mechanism.

• Relative to the hash-pinned audited r=0 source, the generated q=3 CNF exactly appends an equality-to-63 counter over the 450 internal pair supports.
• The generated CNF has 36300 variables and 215724 clauses.
• The bounded CaDiCaL run returned UNKNOWN and its incomplete LRAT prefix was rejected by both lrat-check and CakeLPR.
• The maintained covering range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/build_r0_q03_v1.py --out-dir artifacts/epoch39-20260810/r0-q03-proof-calibration-v1
• python3 scripts/run_r0_q03_lrat_v1.py --artifact-dir artifacts/epoch39-20260810/r0-q03-proof-calibration-v1 --seconds 5 --cpu 0
• python3 checkers/check_r0_q03_v1.py --artifact-dir artifacts/epoch39-20260810/r0-q03-proof-calibration-v1 --out artifacts/epoch39-20260810/r0-q03-proof-calibration-v1/independent-check-v2.json
• sha256sum -c artifacts/epoch39-20260810/SHA256SUMS

• .proof-experiments/20260810-014945-5aa2a2 — built the predicted 36300-variable, 215724-clause CNF
• .proof-experiments/20260810-014956-a2b99a — solver returned UNKNOWN; wrapper then failed on a Path.stat typo
• .proof-experiments/20260810-015149-ce356d — bound and finalized the preserved raw outputs; both proof replayers rejected the prefix
• .proof-experiments/20260810-015313-6d6db0 — independent v2 reconstruction and mutation audit passed

checkers/check_r0_q03_v1.py independently reconstructs the totalizer, verifies source conjunctions and fixed units, checks semantic boundaries, reparses the raw status, freshly compiles both proof replayers, and rejects five real mutations.

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

None recorded.

• The r=0,q=3 formula has 36300 variables and 215724 clauses.
  Hash-bound build manifest and independent-check-v2.json · The retained incidence encoding rooted at F=012345 and 67891011. · computed
• The appended counter is satisfied at 63 true internal-pair supports and rejected at 62 and 64.
  Independent semantic boundary assignments. · The generated balanced totalizer. · computed
• The bounded run produced no accepted SAT or UNSAT certificate.
  Raw CaDiCaL log and fresh lrat-check/CakeLPR replays. · Seed 0, CaDiCaL 1.7.3, normalized r=0,q=3 cell. · computed

• Scale the unchanged proof-producing incidence/q-cell design based on the smallest live combined cell.
  The current CaDiCaL 1.7.3, totalizer, lex-incidence, independent-cell mechanism. · The smallest live combined cell returned UNKNOWN with only 303 conflicts and a rejected incomplete proof prefix. · epoch-receipt.json and independent-check-v2.json · Certified proof-prefix reuse, a materially different solver or encoding, or a terminal proof-producing control of comparable size.

• Fixed-point-free C5 one-orbit tail lookup
  A direct witness settles the problem, while the saved epoch-31 failure profile identifies a specific late-branch bottleneck. · Index unused block orbits by exact residual cycle profile when one slot remains and run matched fixed-node/fixed-wall controls. · high · open
• Canonical root-link catalogue
  Fixing an extremal 12-block root link reduces completion membership variables and is structurally distinct from global incidence search. · Enumerate canonical links under a 10000-orbit or 30-minute cap and independently check the completeness frontier. · normal · open

Objective: Test whether exact residual-orbit tail indexing materially improves constructive C5 search.

First action: Fork scripts/c5_orbit_dfs_v1.py and implement the one-slot residual cycle-profile lookup.

Stop condition: Redirect if matched tests do not materially reduce the prior 888391 depth-six failures; stop immediately on a directly validated 30-cover.

• Fork scripts/c5_orbit_dfs_v1.py and implement a one-orbit tail index keyed by exact residual cycle profile.
• Run matched fixed-node and fixed-wall controls against epoch 31 and directly validate any witness.
• If late depth-six failures do not materially decrease, redirect to the canonical root-link catalogue.
• Do not resume this proof-cell encoding without satisfying its reopen condition.

• 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://github.com/tanyongkiam/cake_lpr ↗

Sol principal agent performed synthesis, implementation, source audit, execution, and interpretation. GPT-5.6 Terra delegate memos supplied advisory prior-art and verification leads and were promoted with provenance; their agreement was not validation. Deterministic tools: CPython 3.12.3, CaDiCaL 1.7.3, GCC 13.3.0, lrat-check, CakeLPR, SHA-256, exact integer arithmetic, and the Proof Factory experiment harness. Web search checked maintained sources and newer literature. No CAS, proof assistant, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1310.0s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-020144-0c0c5c

No human review recorded.