Compiled the exact inherited-threshold incidence CNF for H=Cay(Z_15,{+/-1,+/-2}) rooted at F={0,1,2,3,4,5}, ran a five-CPU-second constructive CaDiCaL discriminator, and independently classified the fixed-H root-block orbits.

high-symmetry pair-surplus cylinder diversification

Fix all pair multiplicities through inherited unary thresholds for one simple 4-regular surplus graph, quotient possible root blocks by Aut(H), and test the unique maximum-q root orbit for a directly checkable cover.

Hypothesis: CaDiCaL 1.7.3 finds a directly checkable 30-block cover in the fixed circulant-H, maximum-q-root cylinder within five CPU seconds.

Test: Build the byte-reconstructible 33178-variable, 156603-clause formula and accept only a SAT assignment independently covering all 455 triples with the prescribed pair loads.

UNKNOWN supplies no witness or exclusion, but the exact orbit reduction is a reproducible structural compression useful for an owned fixed-H frontier. Two materially different enumerations and mutation controls validate its exact scope.

• For H=Cay(Z_15,{+/-1,+/-2}), Aut(H) has order 30 and has exactly 185 orbits on six-subsets.
• Exactly 1890 of the 5005 six-subsets have q>=5, and these form exactly 70 Aut(H) orbits.
• Every hypothetical cover inducing this fixed H can be normalized to one of those 70 root representatives.
• The q=9 representative F=012345 branch remained UNKNOWN after the frozen five-second CaDiCaL run.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• Producer experiment 20260811-204243-db322b returned UNKNOWN with formula SHA-256 1fac571ac8df7efa96a45e5b893db4bc1e7e0176520ba2291f2332283eeb9523.
• Independent experiment 20260811-204320-18e0c3 reconstructed the formula byte-for-byte and enumerated 30 automorphisms and 185 block orbits.
• Mutation experiment 20260811-204328-5afff7 rejected all five declared receipt and protocol corruptions.
• Explicit-dihedral experiment 20260811-204610-ea409a independently reproduced 185 total and 70 q>=5 orbits.
• sha256sum -c artifacts/epoch97-20260811/SHA256SUMS returned OK for every listed artifact.

• .proof-experiments/20260811-204243-db322b: the q=9 circulant-H branch returned UNKNOWN after 4.99 solver CPU seconds.
• .proof-experiments/20260811-204320-18e0c3: independent formula reconstruction and NetworkX orbit audit passed.
• .proof-experiments/20260811-204328-5afff7: five of five receipt/protocol mutations were rejected.
• .proof-experiments/20260811-204610-ea409a: explicit dihedral enumeration independently reproduced 185 total and 70 q>=5 orbits.

Two materially different encodings were used: NetworkX VF2 enumerated all graph automorphisms, while a separate checker enumerated the explicit x -> +/-x+a permutations and tuple-set orbits. The formula was also reconstructed from the base totalizers rather than trusted from the producer.

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 -> a high-symmetry fixed H should sharply reduce rooted cases -> 5005 labelled roots became 185 orbits and 70 q>=5 existence-relevant orbits.
• Inherited-threshold reuse -> exact pair equations should require units rather than fresh counters -> the formula used 135 units and avoided 9975 variables and 47220 clauses.
• Constructive local-cylinder search -> strong pair structure might expose a cover rapidly -> the maximum-q branch remained UNKNOWN, so isolated cylinder search did not supply terminal evidence.

• Aut(Cay(Z_15,{+/-1,+/-2})) has exactly 30 elements.
  NetworkX found 30 automorphisms; the explicit 30-element dihedral subgroup preserves every edge, proving equality. · The fixed simple circulant graph on 15 labelled vertices. · computed
• The graph has 185 six-subset orbits, with q-orbit histogram {2:7,3:44,4:64,5:42,6:19,7:7,8:1,9:1}.
  Independent NetworkX and explicit-dihedral enumeration receipts agree. · All 5005 six-subsets of the fixed graph. · computed
• The 70 q>=5 orbits form an existence-complete root frontier for covers inducing this fixed H.
  Previously proved q>=5 anchor lemma plus the independently checked orbit catalogue. · Only covers whose pair-surplus graph equals this fixed simple H. · proved
• The exact q=9 rooted formula returned UNKNOWN under the frozen protocol.
  Raw log SHA-256 ce84127a039e8285645c84c1d0f192b3518c7c4fa0007982680f0a3af55938b4 and independent status check. · CaDiCaL 1.7.3 seed 0, five CPU seconds, formula SHA-256 1fac571a... · computed

• Treat the five-second q=9 UNKNOWN as evidence that the branch is infeasible.
  The exact recorded circulant-H maximum-q branch. · UNKNOWN provides neither a model nor a negative certificate. · Producer receipt and independent status parser. · A directly checked SAT model or independently replayed UNSAT proof.
• Repeat the six-way minimum-overlap audit as new work.
  The fixed-first-block minimum-intersection decomposition. · Attempt covering-c1563-20260809-221759-2ae2be already proved and independently checked it. · Immutable epoch-34 attempt and artifacts. · A material strengthening such as a new disjoint compiler invariant or solved owner branch.
• Run a plain or owned r=2 calibration as an untested route.
  The normalized r=2 incidence root and owner-H6 r=2 formula. · Attempts covering-c1563-20260809-230018-5dc524 and covering-c1563-20260810-161940-1c6ba7 already ran these tests. · Immutable epoch-35 and epoch-58 records. · A material encoding, ownership, proof-format, or decomposition change.
• Scale arbitrary circulant-H sibling-orbit scans without ownership.
  The remaining 69 q>=5 root orbits. · Nonterminal isolated cylinders do not aggregate into a global exclusion and risk overlapping effort. · The q=9 branch was nonterminal and the 70-orbit union is not yet materialized as disjoint CNFs. · An independently checked owner manifest or a model-finding protocol whose SAT output is globally decisive.

• Disjoint 70-owner circulant-H root frontier.
  It converts the validated existence-complete orbit catalogue into aggregatable fixed-H proof scope. · Compile maximum-q/minimum-orbit ownership predicates without solving, then independently test coverage, disjointness, and mutation rejection. · high · open
• Canonical weighted 4-regular pair-surplus H prefix.
  It attacks the global ownership blocker rather than one simple H isomorphism class. · Enumerate a tiny node- and time-capped canonical prefix with exact duplicate and parent-ownership checks. · high · open
• Constructive exact-degree search with a materially different global mechanism.
  Any directly checked 30-block cover remains globally decisive and avoids the certificate burden of a negative result. · Predeclare one new nonduplicate encoding or neighborhood with a short direct-model acceptance gate. · normal · open

Objective: Determine whether exact pair-surplus ownership can be made disjoint and checkable before allocating more solver compute.

First action: Specify and audit a maximum-q/minimum-orbit owner rule for the 70 circulant-H representatives, while comparing its engineering cost with a tiny canonical weighted-H prefix.

Stop condition: Redirect on any ownership gap or overlap, formula-semantic mismatch, arbitrary-cutoff-only gain, or proof projection lacking independent replay.

• Implement and independently check a maximum-q then minimum-orbit owner manifest for the 70 circulant-H representatives before solving more fixed-H leaves.
• Compare that local frontier with a tiny capped canonical weighted-4-regular-H ownership prefix; prefer the latter if its duplicate and coverage checks are tractable.
• Do not lengthen the unchanged q=9 seed-0 run or scan arbitrary sibling orbits without an ownership manifest.
• Require a directly checked cover or replayed proof before changing any covering bound.

• 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://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. Two GPT-5.6 Terra delegates supplied advisory route memos; Sol audited and rejected both suggested routes as prior internal work, and no model agreement was treated as validation. Deterministic work used CPython 3.12.3, CaDiCaL 1.7.3, NetworkX 3.3 VF2, an independent explicit-dihedral enumerator, GNU taskset, SHA-256, and the computational-researcher experiment harness. The maintained source trail and arXiv references were checked; the browser returned no new extractable content. No SAT witness, DRAT/LRAT proof, CAS, proof assistant, PB solver, cloud lab, external proof service, human validator, publication, or system-level modification was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1244.0s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-205122-770db2

No human review recorded.