Proof-capable unary SAT decision of integral ten-zero parent row 123 in the rooted [13,2] pair-excess partition

integral ten-zero dominance census

Shared monotone unary thresholds encode triple-excess integers; balanced truncated totalizers impose all 105 exact pair equations.

Hypothesis: Global rooted [13,2] row 123, root [0,2,3,4,7], is decided within 2,000 CaDiCaL conflicts and admits an integral ten-zero triple-excess vector.

Test: Generate one source-bound CNF, independently reconstruct every clause, run CaDiCaL seed 0 to 2,000 conflicts, and accept SAT only after exact vector checking or UNSAT only after LRAT replay.

The direct arithmetic witness, independent clause reconstruction, mutation rejection, and byte-identical regeneration establish local feasibility only. They do not justify a candidate or field-level claim.

• Global rooted [13,2] row 123 with root [0,2,3,4,7] admits a nonnegative integral ten-zero triple-excess vector of total 85.
• The vector satisfies all 105 exact pair equations and ten zero pins.
• All 120 seven-zero children survive the same necessary projection.
• No literal 54-block cover, global branch exclusion, or improved bound was obtained.

• Generated CNF SHA-256 fc26624281acbd3fa8a922ad069c09802ae4571b50d2b033e1744f99df517858
• Independent checker returned accepted=true, valid=true, witness_sum=85, pair_equations_checked=105
• CaDiCaL seed 0 returned SAT after 1,031 conflicts under the 2,000-conflict cap
• A one-unit witness mutation was rejected at pair [0,1]
• sha256sum -c artifacts/row123-ten-zero-cnf-20260810/manifest.sha256 passed

• .proof-experiments/20260810-232036-3986cb: deterministic CNF generation
• .proof-experiments/20260810-232037-2567a5: independent clause reconstruction passed
• .proof-experiments/20260810-232038-5d8bdd: CaDiCaL SAT after 1,031 conflicts
• .proof-experiments/20260810-232038-191c5e: decoded 66 positive entries with total 85
• .proof-experiments/20260810-232038-8ba4e7: exact arithmetic check passed
• .proof-experiments/20260810-232039-f14709: one-unit mutation rejected

checkers/check_row123_ten_zero_cnf_v1.py uses recursive bit-mask enumeration, separate unary allocation and totalizer code, byte-compares all clauses, and checks the sparse vector arithmetically without importing 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

• Pseudo-Boolean unary thresholds -> small right-hand sides should propagate more decisively than a one-second MILP search -> row 123 changed from HiGHS-UNKNOWN to checked SAT in 1,031 conflicts.

• Row 123 has an integral ten-zero triple-excess vector of total 85.
  witness.json SHA-256 d228d57bd324b45b785fa9262510119be258064e68db2c756a56b0a5bfaeafc9; independent-check valid=true · Row 123 necessary projection only · computed
• All 120 seven-zero children of row 123 survive the necessary projection.
  The checked vector vanishes on all ten root triples, a superset of every child's seven zeros. · The 120 attached child headers; not literal lifts · proved

• Use integral infeasibility of row 123 to prune its children.
  Row 123 only · An exact checked positive integer witness exists. · witness.json and independent-check.json · Only a stronger labelled constraint can distinguish these children.
• Treat a one-second HiGHS UNKNOWN as evidence of infeasibility or pruning promise.
  Row 123 and the present integral protocol · Unary SAT found a checked witness in 1,031 conflicts. · .proof-experiments/20260810-232038-5d8bdd/experiment.json · A source-bound parent with proof-replayed UNSAT or a measured predictor correlated with certified pruning.

• Certificate-first 16-cube pilot on a complete multiplicity-five type-4 branch.
  It restores labelled block identities and can yield replayable class elimination. · Emit all 16 cube leaves and an independent coverage map, then run each leaf under a fixed proof cap. · high · open
• Exact-degree constructive neighborhood beyond the verified defect-10 seed.
  A direct 54-cover would settle the problem. · Test one bounded new trade or ejection-chain neighborhood with a below-10 defect gate. · normal · open
• Pair-excess skeleton/common-family labelled coupling.
  Exact pair targets may add propagation absent from aggregate projections. · Count joint orbits and require a complete lift before generating SAT leaves. · low · open

Objective: Obtain the first replayed nontrivial UNSAT leaf or checked SAT model in a globally complete labelled multiplicity-five decomposition.

First action: Create protocols/type4-semantic-16-cube-pilot-v1.json binding the base CNF hash, four audited primary literals, all 16 assignments, proof flags, and independent coverage checks.

Stop condition: Redirect on any cube-map mismatch, model/checker disagreement, non-replayable proof, or all leaves hitting the cap; advance only with a checked model or replayed UNSAT leaf.

• Hold the all-root integral census unless a certified pruning predictor appears.
• Construct and independently audit a four-literal, 16-leaf cube partition for the complete type-4 branch.
• Run every leaf with proof emission and advance only with a checked model or replayed nontrivial UNSAT leaf.
• Switch to exact-degree constructive search if all cube leaves merely hit the cap.

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

GPT-5.6 Sol was principal investigator and designed, implemented, ran, audited, and interpreted the experiment. GPT-5.6 Terra delegates supplied advisory reconnaissance only; the relied-on memo was promoted with provenance and model agreement was not validation. Python 3.12.3 generated and independently reconstructed the CNF. CaDiCaL 1.7.3 seed 0 ran the 2,000-conflict search. The pinned DRAT/LRAT tools were available but unused because the result was SAT. SHA-256 and the computational-researcher harness bound artifacts. Pre-acquired source-status searches were used; no new web browse, subagent, lab job, CAS, proof assistant, installation, external write, publication, or Git operation occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1137.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-232845-0b2769

No human review recorded.