Exact orbit-quotiented constructive search for a 54-block cover invariant under (0 1 2)(3 4 5)(6 7 8)(9 10 11)(12 13 14), with matched proof-producing CNF pilots

semiregular C3-symmetric constructive SAT

Represent an invariant cover by selecting 18 of 1001 block orbits, enforce 155 triple-orbit coverage rows, and compare baseline and degree-strengthened proof-producing CNFs

Hypothesis: The C3-invariant subfamily returns either a checked 54-block cover or proof-producing UNSAT within 25000 CaDiCaL conflicts.

Test: Run corrected, independently audited baseline and degree-strengthened CNFs with CaDiCaL 1.7.3 at identical seed 1553 and 25000-conflict caps.

The exact orbit arithmetic and corrected independent reconstruction are durable scoped progress. UNKNOWN solver runs cannot support feasibility or infeasibility, and the degree strengthening failed the predeclared performance gate.

• The specified C3 action partitions the 3003 five-subsets into exactly 1001 size-three orbits.
• It partitions the 455 triples into exactly 155 orbits, including five fixed triple orbits.
• A C3-invariant 54-block cover is equivalent to selecting 18 block orbits satisfying the 155 orbit-coverage rows.
• Under Z15 translation, five-set orbits have histogram 200 times size 15 and one time size 3, so no invariant family has size 54.
• Neither corrected 25000-conflict CNF pilot resolved the C3-invariant family.

• python3 checkers/check_c3_symmetric_cover_v1.py --manifest artifacts/c3-symmetric-cover-20260809/manifest.json --cnf artifacts/c3-symmetric-cover-20260809/instance.cnf --output artifacts/c3-symmetric-cover-20260809/independent-check.json
• /usr/bin/cadical --seed=1553 -c 25000 -t 110 --no-binary -w artifacts/c3-symmetric-cover-20260809/model.out artifacts/c3-symmetric-cover-20260809/instance.cnf artifacts/c3-symmetric-cover-20260809/proof.drat
• /usr/bin/cadical --seed=1553 -c 25000 -t 110 --no-binary -w artifacts/c3-symmetric-cover-20260809/baseline-model.out artifacts/c3-symmetric-cover-20260809/baseline.cnf artifacts/c3-symmetric-cover-20260809/baseline-proof.drat
• sha256sum -c artifacts/c3-symmetric-cover-20260809/manifest.sha256

• .proof-experiments/20260809-231623-a672b3: corrected independent checker passed all orbit, hash, DIMACS, and coverage-prefix checks
• .proof-experiments/20260809-231644-9c556c: degree-strengthened CNF returned UNKNOWN after 25002 conflicts, 70273 decisions, and 35233809 propagations
• .proof-experiments/20260809-231644-fba105: baseline CNF returned UNKNOWN after 25000 conflicts, 81920 decisions, and 11565076 propagations

checkers/check_c3_symmetric_cover_v1.py uses a separately implemented set-based orbit partition, reconstructs all 155 primary coverage clauses, checks formula and orbit hashes, and directly checks an optional expanded cover. No UNSAT certificate was produced, so no proof replay was applicable.

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

• Group-action compression -> predict a threefold primary-variable reduction for a fixed-point-free C3 action -> independently observed exactly 3003/1001 = 3.
• Redundant implied equalities in pseudo-Boolean search -> predict improved propagation -> decisions fell 14.2% but propagation work and runtime increased enough to reject this encoding.
• Cyclic-design orbit arithmetic -> predict a congruence obstruction for full Z15 invariance -> exact orbit census excludes family size 54.

• The fixed C3 action has 1001 five-set orbits, all of size three.
  artifacts/c3-symmetric-cover-20260809/independent-check.json · all 3003 five-subsets of a 15-point set under the specified permutation · computed
• The fixed C3 action has 155 triple orbits, five fixed.
  artifacts/c3-symmetric-cover-20260809/independent-check.json · all 455 triples under the specified permutation · computed
• No fully Z15-invariant five-subset family has exactly 54 blocks.
  The independently computed orbit histogram is 200 size-15 orbits and one size-3 orbit; a union has size 15b or 3+15b. · block families invariant under translation modulo 15 · proved

• A fully Z15-invariant 54-block construction
  all unions of five-subset orbits under translation modulo 15 · All such family sizes are congruent to 0 or 3 modulo 15, while 54 is congruent to 9. · artifacts/c3-symmetric-cover-20260809/independent-check.json · Only a construction using a weaker symmetry group or a non-invariant family can evade the orbit-size obstruction.
• Scale the current degree-strengthened monolithic C3 CNF solely because it has fewer decisions
  CaDiCaL 1.7.3, seed 1553, balanced totalizer encoding, matched 25000-conflict protocol · The 14.2% decision reduction cost 204.7% more propagations and 4x process time, failing the continuation gate. · artifacts/c3-symmetric-cover-20260809/result.json · A materially different encoding or symmetry reduction that improves matched-cap time and propagation work.

• Normalizer lex leaders for the five C3 point-orbits
  The quotient retains permutations of the five cycles and relative phase symmetries that may eliminate search in bulk. · Derive the normalizer action on the 1001 block orbits, emit independently checked lex-leader clauses, and run a 25000-conflict matched pilot. · normal · open
• Multi-basin exact-degree constructive repair
  It remains a direct-witness route without the unverified assumption that a solution has nontrivial automorphism. · Run deterministic exact-degree-preserving repair from multiple hash-bound basins and directly check any zero-defect candidate. · high · open

Objective: Seek a direct nonsymmetric 54-cover while retaining the compact C3 formula as a future symmetry/cube target.

First action: Define a deterministic multi-basin exact-degree repair protocol with direct 455-triple checking and a predeclared defect-improvement gate.

Stop condition: Stop or redirect if the basin pilot neither finds a checked cover nor materially lowers the best independently checked defect distribution.

• Redirect the next constructive tranche to multi-basin exact-degree repair.
• Retain the compact C3 baseline for a future independently audited normalizer lex-leader or cube partition.
• Do not scale the degree-totalizer formula without a new matched-cap improvement.

• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal selected, implemented, audited, executed, and interpreted the discriminator. GPT-5.6 Terra delegates supplied bounded advisory challenger and verification memos; model agreement was not treated as validation. Python 3.12.3 exact enumeration, CaDiCaL 1.7.3, SHA-256, the project run_experiment harness, exploratory bounded Z3 4.13.0 and SciPy/HiGHS controls, and a separately implemented Python orbit/CNF checker were used. No proof assistant, lab job, package installation, external write, or publication was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1274.2s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260809-232147-637749

No human review recorded.