Condition the fixed-block SAT model on one explicit simple 4-regular pair-excess graph and benchmark exact pair counters against unsplit pair bounds in two encodings.

rooted pair-excess-profile SAT decomposition

Fix B0=012345, impose (K6-{03,14,25}) union Circ(9;±1,±2) as E_xy=lambda_xy-4, replace pair intervals by exact residual targets, and compare matched CaDiCaL runs.

Hypothesis: The declared rooted exact pair-excess profile reduces both conflicts and decisions by at least 2x in both validated cardinality encodings versus matched unsplit pair bounds at seed 0 and 15 seconds, without increasing peak RSS.

Test: Four cold seed-0 CaDiCaL 1.7.3 calls: profile and unsplit-pair CNFs for the sequential and totalizer encodings, each capped at 15 seconds, followed by an independent bitmask, DIMACS, and log audit.

The predeclared route gate required at least 2x baseline/profile conflict and decision ratios in both encodings with no RSS increase. Every measured conflict and decision ratio was below 1, and sequential RSS increased, so scaling this profile is unjustified. UNKNOWN carries no mathematical exclusion.

• For any hypothetical 30-block C(15,6,3) cover, E_xy=lambda_xy-4 is a loopless 4-regular multigraph with total edge multiplicity 30.
• For the declared rooted profile, sequential exact conditioning reduced the CNF from 1043262 variables and 4047744 clauses to 766992 variables and 2943054 clauses.
• For the declared rooted profile, totalizer exact conditioning reduced the CNF from 449802 variables and 2860824 clauses to 388392 variables and 2185854 clauses.
• At seed 0 and a 15-second cap, this profile failed the predeclared propagation gate in both encodings.
• No result in this epoch changes 30 <= C(15,6,3) <= 31.

• python3 scripts/rooted_excess_profile_v1.py --out-dir artifacts/epoch6-20260808/rooted-excess-profile-v1 --time-limit 15 --cadical /usr/bin/cadical --cadical-sha256 7b73df0a6d9cf3c751a1948300e5baff8e82c4d39bcd88f0c063b5f5cfb8b33e
• python3 checkers/check_rooted_excess_profile_v1.py artifacts/epoch6-20260808/rooted-excess-profile-v1/run-manifest.json --receipt /tmp/rooted-profile-recheck.json
• Cardinality regression: 112636 exhaustive semantic cases passed.
• Archival-cover controls: Python and C validators accepted the 31-cover and rejected duplicate and corruption controls.

• .proof-experiments/20260808-191539-e9f3b7: four-cell profile benchmark; all UNKNOWN and propagation gate failed
• .proof-experiments/20260808-192132-c85579: independent graph, metadata, DIMACS, and solver-log audit passed
• .proof-experiments/20260808-191247-6eec50: 112636 cardinality semantics cases passed
• .proof-experiments/20260808-191755-2fb1a5: archival-cover positive and negative controls passed

checkers/check_rooted_excess_profile_v1.py independently reconstructs the graph and ordered targets with bitmasks, validates full DIMACS bodies and hashes, reparses solver logs, and recomputes ratios. It is not a clean-room global CNF generator, so no SAT/UNSAT mathematical claim is promoted.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• Regular-graph decomposition -> predict exact pair profiles shrink SAT counters and improve propagation -> formulas shrank but search worsened, rejecting the transfer for this profile.
• Proof-certificate covering campaigns -> require disjoint cubes and replayable leaves before global exclusion -> no profile enumeration was attempted because those prerequisites are absent.

• In every hypothetical 30-block cover, each point has degree 12 and the pair-excess multiplicities form a loopless 4-regular multigraph with 30 total edges.
  Degree-12 lemma plus lambda_xy>=ceil(13/4)=4 and incidence identity 12*5-14*4=4. · All 30-block C(15,6,3) covers. · proved
• The declared rooted graph has residual target multiset 3^3 4^84 5^18 and target sum 435.
  Independent bitmask audit in rooted_excess_profile_receipt.json. · The declared profile after fixing B0. · computed
• The declared profile failed the 2x conflicts-and-decisions propagation gate in both encodings at seed 0 and 15 seconds.
  Hash-bound run manifest and independently checked receipt. · CaDiCaL 1.7.3, seed 0, same host, stated four formulas and 15-second caps. · computed
• The screened Horsley-Singh Theorem-6 substitution evaluates to 28.
  b2=4, b1=12, a1=8, d=4 and ceil(195/7)=28; arithmetic independently recomputed. · The pre-acquired theorem mapping for v=15,k=6,t=3,s=1. · conditional

• Scale the declared simple rooted excess profile because exact conditioning improves propagation.
  This profile, two encodings, seed 0, 15-second matched protocol. · Conflicts and decisions worsened in both encodings and sequential RSS increased. · artifacts/epoch6-20260808/rooted_excess_profile_receipt.json · A materially different encoding or matched multi-seed evidence on several nonisomorphic profiles that passes the same gate.
• Obtain a new lower bound from the screened Horsley-Singh substitution.
  The supplied s=1 Theorem-6/15/18 instantiation. · The applicable screened arithmetic gives 28; the stronger screened hypothesis would require false 12<6. · artifacts/epoch6-20260808/prior_art_route_screen.md · A distinct primary-sourced theorem with every hypothesis checked and a symbolic value at least 31.
• Infer that the tested profile or arbitrary 30-covers are impossible from the solver runs.
  The local leaf and global target. · Every solver status was UNKNOWN; there is no proof log or exhaustive profile partition. · Run manifest and receipt. · A proof-producing UNSAT rerun for the leaf, or an independently checked exhaustive partition with replayed proofs for the global target.

• Five-seed global pair-bound SAT confirmation
  The packet is hash-bound and directly measures whether the global incumbent has stable propagation value. · Run bash scripts/submit_pair_multiseed_lab_v1.sh after lab registration becomes writable. · high · open
• Six-case second-block assumption pilot
  The orbit reduction is proved and may supply global information without profile enumeration. · Run literals 4921,1876,589,136,19,1 on the immutable pair CNF under a matched aggregate cap. · normal · open
• Alternative global constructive encoding
  A 30-block witness settles the problem, while local two-for-one and three-for-two repairs around the archival cover are exhausted. · Design a bounded alternative optimization/SAT encoding with the degree-12 equalities and six-case block normalization, then calibrate it on the verified 31-cover. · normal · open

Objective: Obtain global information from the prepared pair-bound model without scaling the failed excess-profile leaf.

First action: Test lab ledger writability; if writable run bash scripts/submit_pair_multiseed_lab_v1.sh, otherwise prepare the six canonical second-block assumption-literal benchmark.

Stop condition: SAT triggers dual direct validation; provisional UNSAT triggers proof-producing replay; failure to improve both conflicts and decisions redirects to an alternative constructive encoding.

• Check whether /root/proof-factory/state/labs/jobs is writable.
• If writable, run bash scripts/submit_pair_multiseed_lab_v1.sh and require a durable job ID before treating it as submitted.
• If still blocked, benchmark the six verified second-block assumption literals 4921, 1876, 589, 136, 19, and 1 against the unsplit pair CNF under a matched aggregate budget.
• Do not enumerate excess-profile orbits without a disjoint exhaustive canonicalization and stabilizer certificate.
• SAT must pass both direct 455-triple validators; UNSAT must be regenerated with replayable proof logs.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=6&t=3&v=15 ↗
• https://arxiv.org/abs/1706.06825 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol was principal investigator. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-design memos; their agreement was not validation. Deterministic tools used: Python 3.12.3, Z3 via the existing exhaustive cardinality regression, CaDiCaL 1.7.3, GNU time, GCC, SHA-256, and the Proof Factory run_experiment harness. The web connector returned no source page body; status relied on pre-acquired source records. No proof assistant, DRAT/LRAT replay, clean-room global CNF generator, or external human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1501.3s

Review state

not a result claim

Attempt ID

covering-c1563-20260808-192457-b8fa70

No human review recorded.