Strategy and discriminatormonotone forbidden-coordinate dominance
A feasible triple-excess vector vanishing on all ten triples of a distinguished 5-set simultaneously witnesses every seven-zero child by coordinate-set containment.
Hypothesis: Every one of the 111 safely quotiented rooted simple-15-cycle representatives admits a nonnegative integral triple-excess vector vanishing on all ten triples of its distinguished 5-set.
Test: Solve 111 exact ten-zero integer systems and independently verify whether their positive witnesses cover all 12,096 seven-zero headers by set containment.
RationalePositive ten-zero witnesses are stronger than the required seven-zero witnesses, and every arithmetic and containment condition was reconstructed independently. The result is complete for one skeleton partition but is neither a cover nor an exclusion of any literal covering-design branch.
Claims requiring scrutiny- All 111 safely quotiented rooted [15]-partition representatives admit nonnegative integral ten-zero triple-excess witnesses.
- All 12,096 safely quotiented seven-zero headers in the [15] partition survive the necessary integer projection.
- The exact covering range remains 54 <= C(15,5,3) <= 55.
Evidence and scope- python3 scripts/cycle15_ten_zero_root_dominance_highs_v1.py --joint artifacts/seven-unique-skeleton-joint-orbits-20260810/result.json --skeleton artifacts/joint-orbit-census-20260808/manifest.json --protocol protocols/cycle15-ten-zero-root-dominance-v1.json --output artifacts/cycle15-ten-zero-root-dominance-20260810/result.json --per-row-seconds 5
- Independent check: 111 witnesses, 50,505 entries, 11,655 pair equations, and 12,096 child-containment checks.
- Five fail-closed mutations were rejected.
- Original and regenerated result SHA-256 values both equal 8caddcbc4092421af3950efafc35e21b00cb1f94c98d8b20ad44ca1e6ee3674a.
- sha256sum -c artifacts/cycle15-ten-zero-root-dominance-20260810/manifest.sha256 passed.
Computational experiments- .proof-experiments/20260810-150753-b61889: Z3 timed out after 120 seconds on the first ten-zero row; no mathematical inference.
- .proof-experiments/20260810-151115-f77db8: HiGHS completed 111/111 SAT rows and covered 12,096 child headers in 53.079 seconds.
- .proof-experiments/20260810-151238-e4ca8f: fresh regeneration completed in 55.952 seconds and was byte-identical.
Independent checkercheckers/check_cycle15_ten_zero_root_dominance_v1.py independently reconstructs triples, pairs, roots, all child selections, set containment, totals, and pair margins without importing producer code.
Contribution gatenot_requested
No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.
- Original model outcome
- no_progress
- Public classification
- no_progress
Cross-domain transfers tested- Constraint-programming dominance -> test a stronger forbidden-coordinate superset once per parent -> all 111 parents were feasible and represented 12,096 children.
- Alternative exact MILP backend -> stronger ten-zero constraints may become easier under presolve than incremental SMT -> HiGHS completed the tranche while Z3 timed out on its first row.
Established facts- A feasible ten-zero vector witnesses every seven-zero child of the same root.
Direct subset containment of forbidden coordinate sets. · Any rooted triple-excess system · proved - All 111 rooted simple-15-cycle representatives possess such ten-zero vectors.
Result SHA-256 8caddcbc4092421af3950efafc35e21b00cb1f94c98d8b20ad44ca1e6ee3674a and independent check SHA-256 9bf9e085b72e77f001c9ca2a51b98ede263029e3e8869e92b759bb3ad60b6502. · Complete [15]-partition rooted frontier · computed - All 12,096 [15]-partition seven-zero headers survive this necessary integer relaxation.
Independent reconstruction of every child selection and its containing ten-set. · Complete safely quotiented [15] joint-header tranche · computed
Ruled out in this epoch- Repeat the complete fixed-{4,5} pair-link challenger.
All 754 frozen type-4 signature/e45 targets · The existing complete artifact retained every target and has result SHA-256 b5eb3ccf2ad757c0f2ec3098553a6c89ac47adb7c8cd68d10a2fa11ddd5ae9fb. · artifacts/type4-complete-pair-link-gate-20260809/result.json and independent-check.json · Add genuinely new labelled information beyond the complete fixed-pair link. - Use the seven-zero integer triple-excess projection to prune a [15]-partition header.
All 12,096 safely quotiented [15] headers · Every root has a stronger ten-zero positive witness. · artifacts/cycle15-ten-zero-root-dominance-20260810/manifest.sha256 · Introduce stronger labelled block-incidence information; additional subsets of the same ten root coordinates cannot prune these roots. - Use incremental Z3 for the ten-zero dominance census at the current encoding.
The exact recorded [15] base system and first rooted row · It exceeded the 120-second cap before completing one row, while HiGHS completed all 111 rows in 53.079 seconds. · .proof-experiments/20260810-150753-b61889/experiment.json · A measured encoding or solver change that materially improves the same first-row control.
Open leads- Complete ten-zero dominance census over all 41 skeleton partitions.
The global rooted universe has 2,145 rows rather than 124,988 child headers, and the [15] tranche showed a 47.9105-fold measured runtime reduction. · Generalize the scripts and run the smallest non-[15] partition under the same independent-check contract. · high · open - Return to the globally complete four-branch labelled SAT encoding.
SAT or replayable UNSAT remains terminal, unlike aggregate feasibility classifications. · Run a fixed-cap propagation pilot only after a concrete encoding improvement of at least 20 percent on a matched branch. · normal · open - Constructive repair from the verified defect-10 exact-degree seed.
A 54-cover would settle the problem directly, but previous 2-for-2, 3-for-3, multibasin, and sampled ejection-chain searches did not improve defect 10. · Use a materially new exact or trade-based neighborhood; do not increase the same random cutoff. · normal · open
Continuation checkpointObjective: Determine whether ten-zero dominance can classify the complete all-partition triple-excess relaxation at practical cost.
First action: Run `rg -n "partition.*\[15\]|rows =" scripts/cycle15_ten_zero_root_dominance_highs_v1.py checkers/check_cycle15_ten_zero_root_dominance_v1.py`, generalize those restrictions, and pilot the smallest non-[15] partition.
Stop condition: Stop or redirect if producer/checker coverage differs, median exact-solve time exceeds two seconds per root, or uniformly feasible pilots make labelled SAT or constructive repair materially more valuable.
Next moves- Generalize the HiGHS producer and independent checker from the [15] partition to all 2,145 rooted skeleton representatives.
- Pilot the smallest non-[15] partition and stop if checker coverage disagrees or projected full-census cost is unattractive.
- For any root without a ten-zero witness, screen its canonical seven-zero children individually; do not treat ten-zero infeasibility as an exclusion.
- Keep the four labelled SAT branches and constructive defect-10 route available as immediate switches.
Citations
Tool disclosureGPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance that was audited and promoted under sources/advisory; their agreement was not validation. Python 3.12.3, SciPy 1.11.4 with bundled HiGHS, NumPy 1.26.4, Z3 4.13.0 as a timed-out control, deterministic Python checkers, SHA-256, and the computational-researcher experiment harness were used. No CAS, proof assistant, cloud-lab job, external write, or publication was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.
- Duration
- 1462.3s
- Review state
- evidence receipt failure; not durable progress
- Attempt ID
covering-c1553-20260810-152341-f8137e
Human review ledgerNo human review recorded.