Run the complete predeclared [13,2] integral ten-zero parent census until the first one-second HiGHS non-SAT row, then independently reconstruct every positive witness and the exact stopping row.

integral ten-zero dominance census

Ten-zero parents compress 10,144 seven-zero child systems to 106 integer margin systems; sparse MILP searches for witnesses and a separate checker verifies them by exact integer incidence arithmetic.

Hypothesis: Every one of the 106 safely quotiented rooted [13,2] representatives admits a nonnegative integral triple-excess vector vanishing on all ten triples of its root.

Test: Run each root with a fixed one-second HiGHS cap, stop at the first non-SAT row, accept positive rows only after exact independent checking, and scale only if the full tranche completes.

Exact integer checking supports the 12 positive claims, while the terminal solver status is only UNKNOWN and cannot support an exclusion. The predeclared fail-closed gate therefore blocks scale-up and selects one proof-capable follow-up.

• Global rooted [13,2] rows 111 through 122 are feasible in the integral ten-zero triple-excess projection.
• Their 1,272 attached seven-zero child headers survive that necessary projection by forbidden-set containment.
• Global row 123 was not decided within the fixed one-second HiGHS cap; this is not evidence of infeasibility.

• result-a.json and result-b.json have identical SHA-256 2782d13f70c90e5c20fb7c97047815f9ef2ed31666f497c47ae6de2f735a6376.
• independent-check.json accepted 12 witnesses, 798 entries, 1,260 equations, 1,272 child headers, and the terminal row map.
• Both witness and root-map mutations were rejected; final manifest replay experiment 20260810-204153-ed472e passed.

• .proof-experiments/20260810-203822-6d6a26: 12 exact SAT parents then UNKNOWN at global row 123.
• .proof-experiments/20260810-203834-708bdf: byte-identical regeneration with the same terminal row.
• .proof-experiments/20260810-203907-85106e: independent checker PASS.
• .proof-experiments/20260810-203917-2d1fe0 and 20260810-203924-565f5d: two fail-closed mutations rejected.
• .proof-experiments/20260810-204153-ed472e: final manifest replay PASS.

checkers/check_partition_132_ten_zero_integral_v1.py independently reconstructs all [13,2] roots, the skeleton matrix, ten-zero sets, 105 pair equations, sparse witnesses, and child counts 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

• Continuous-relaxation basis discovery -> predict that a sparse exact integer solver will rapidly classify most parents -> observed 12 rapid integer witnesses but a reproducible UNKNOWN on parent 13, so the transfer is useful only for target selection, not global pruning.

• Rooted [13,2] rows 111 through 122 admit nonnegative integral ten-zero triple-excess witnesses.
  result-a.json SHA-256 2782d13f... and independent-check.json SHA-256 e11e49b... · Twelve rooted parents and 1,272 attached children in the necessary integral projection only. · computed

• Scale the all-root integer census immediately under the same one-second HiGHS protocol.
  The planned 106-parent [13,2] tranche and any extrapolation to the remaining global parents. · The predeclared full-tranche gate failed at parent 13; UNKNOWN is not evidence and further capped rows would accumulate no certified pruning. · Two byte-identical runs stop at global row 123. · A proof-capable decision of row 123 or a measured encoding improvement that yields an independently validated class elimination.

• Proof-capable integer decision for global row 123, root [0,2,3,4,7].
  It is the first reproducible hard parent under the complete [13,2] order and is far smaller than literal block realization. · Encode its 445 allowed triple variables with exact 105 margins, test semantics independently, and run CaDiCaL for 2,000 conflicts. · high · open

Objective: Decide exact integer feasibility of [13,2] global row 123 proof-capably.

First action: Generate a hash-bound CNF for root [0,2,3,4,7] with 445 allowed triple variables bounded by 0..8 and all 105 exact pair margins, plus an independent semantic checker.

Stop condition: Stop on checker mismatch, SAT with an exact decoded witness, replayed LRAT UNSAT, or UNKNOWN at 2,000 conflicts without a material propagation gain.

• Build a proof-capable bounded integer CNF for global row 123 with independently reconstructed semantics.
• Run a fixed 2,000-conflict CaDiCaL pilot; decode SAT exactly or replay LRAT for UNSAT.
• If row 123 is SAT, keep the global integer census held because this tranche supplied no pruning; if UNSAT, test its 120 weaker seven-zero children before claiming any header elimination.

• 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 ↗

GPT-5.6 Sol principal audited the route, rejected stale Terra delegate rediscoveries, designed and implemented the discriminator, ran it, and interpreted the evidence. GPT-5.6 Terra delegates supplied advisory memos only; their agreement was not validation. No Sol subagents were spawned. Deterministic Python 3.12.3, NumPy 1.26.4, SciPy 1.11.4 with bundled HiGHS, a separately written standard-library checker, SHA-256, the computational-researcher experiment harness, and web access to the maintained covering sources were used. No CAS, proof assistant, SAT proof, lab job, external write, or publication occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1134.9s

Review state

not a result claim

Attempt ID

covering-c1553-20260810-204630-d6ba7d

No human review recorded.