2026-08-08 22:50 UTCgpt-5.6-sol · high

Derived and tested a root-pair outside-triple coupling inequality on the selected partition-[15], root-mask-31 case.

Progress

A general root-pair outside-coverage lemma was proved and applied to one selected rooted skeleton case. Exact certificates eliminate 7 of its 20 profiles, while integer witnesses preserve 13. This is profile-level progress only: C(15,5,3) remains between 54 and 55 and all 2145 rooted cubes remain open. An initial wrapper invocation was discarded because shell quoting split the source URL; the claimed receipt is the subsequent clean run with a fresh output path.

Strategy and discriminator

outside-triple root-pair coupling

Couple each root pair's 31-cell intersection counts to its exact triple-excess budget, then classify profiles using integer witnesses or exact rational Farkas certificates.

Hypothesis: At least one of the 20 necessary root profiles for partition [15], root mask 31 becomes infeasible after adding the ten pair-local outside-triple coverage inequalities.

Test: Solve each 31-variable profile relaxation, emit an exact Farkas certificate for every infeasible LP and an integer witness for every survivor, then reconstruct and check all rows without Z3.

Rationale

For root pair ij, the root block covers no outside triple ijx. The other 4+s_ij blocks containing ij provide 3(4+s_ij) third-point incidences. At least ten must go to outside points, leaving at most 2+3s_ij incidences on extra root points. Exact Farkas combinations turn violations into checkable contradictions independent of solver trust.

Claims requiring scrutiny

For any hypothetical 54-block cover and selected root block R, sum_{B != R, ij subset B}(|B intersect R|-2) <= 2+3s_ij for every root pair ij.
In the partition-[15], root-mask-31 case, profile indices 0,1,2,3,4,6,9 are infeasible under this necessary relaxation.
The remaining thirteen profile indices 5,7,8,10,11,12,13,14,15,16,17,18,19 have explicit integer witnesses for the relaxation only.

Evidence and scope

python3 scripts/root_pair_excess_coupling_v1.py --source-manifest artifacts/joint-orbit-census-20260808/manifest.json --protocol protocols/root-pair-excess-coupling-v1.json --output artifacts/root-pair-excess-coupling-20260808-2245/result.json
python3 checkers/check_root_pair_excess_coupling_v1.py --source-manifest artifacts/joint-orbit-census-20260808/manifest.json --protocol protocols/root-pair-excess-coupling-v1.json --result artifacts/root-pair-excess-coupling-20260808-2245/result.json --output artifacts/root-pair-excess-coupling-20260808-2245/independent-check.json
sha256sum -c artifacts/root-pair-excess-coupling-20260808-2245/manifest.sha256 returned OK for every listed artifact.
A fresh producer run compared byte-identically with result.json.

Computational experiments

.proof-experiments/20260808-224437-3703ad: final producer classified 20 profiles as 7 LP-infeasible and 13 integer-feasible.
.proof-experiments/20260808-224450-c32321: independent checker validated 7 certificates and 403 witness entries.
.proof-experiments/20260808-224450-39c486: all 3 deliberate mutations were rejected.

Independent checker

checkers/check_root_pair_excess_coupling_v1.py reconstructs rows using set containment rather than importing producer logic and checks exact Fraction arithmetic. It accepted seven Farkas contradictions and thirteen integer witnesses; a separate mutation harness corrupted a witness, a dual multiplier, and the source binding, and all were rejected.

Contribution gate

not_requested

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

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

None recorded.

Established facts

The root-pair penalty inequality sum(|B intersect R|-2) <= 2+3s_ij is necessary.
Direct counting of the ten required outside triples ijx. · Every hypothetical 54-block C(15,5,3) cover with a selected block R. · proved
Seven specified profiles are infeasible in the selected root-cell relaxation.
Seven exact rational Farkas certificates accepted coefficient-by-coefficient. · Partition [15], root mask 31, internal excess four. · proved
Thirteen profiles satisfy the coupled root-cell relaxation.
Thirteen checked 31-entry nonnegative integer witnesses. · The relaxation only; no five-block realization is implied. · computed

Ruled out in this epoch

Profiles 0,1,2,3,4,6,9 can occur in the selected coupled root-cell relaxation.
Partition [15], root mask 31 with all recorded equalities and ten pair-local inequalities. · Each profile has an exact Farkas combination with nonnegative variable coefficients and combined right-hand side -1. · artifacts/root-pair-excess-coupling-20260808-2245/result.json and independent-check.json · A demonstrated error in the root-pair lemma, source matrix, profile table, or exact certificate reconstruction.
The selected cube is excluded by this relaxation.
The complete selected rooted cube. · Thirteen profiles retain explicit integer witnesses. · 403 independently checked witness entries. · A strictly stronger proved coupling that excludes every surviving profile.

Open leads

Global root-pair coupling census.
The selected pilot removed 35% of profiles at very low cost, and the same proved inequality applies to all rooted cubes. · Canonicalize coefficient signatures across the 2145 root orbits, solve each signature once, and expand results with an independent coverage check. · high · open
Outside-subset realizability refinement.
The remaining root-cell witnesses do not specify actual subsets of the ten outside points. · For one surviving profile, encode outside portions as q-subsets with exact outside point/pair degrees and triple coverage. · normal · open
Proof-producing OPB calibration.
A checked proof stack remains the most direct route to certified cube exclusion. · Run the saved C(5,3,2) bounds 3,4,5 calibration after pinned RoundingSat, VeriPB, and CakePB become available. · high · open

Continuation checkpoint

Objective: Measure the global cube/profile reduction supplied by the proved root-pair inequality.

First action: Generalize scripts/root_pair_excess_coupling_v1.py over artifacts/joint-orbit-census-20260808/manifest.json and canonicalize exact coefficient-system signatures before invoking Z3.

Stop condition: Redirect if no rooted cube is removed, profile pruning is negligible, signature expansion fails its independent check, or any Farkas/witness validation disagrees.

Next moves

Generalize the producer over all 2145 rooted skeleton orbits.
Canonicalize identical coefficient systems before solving and independently expand the signature-to-cube reverse map.
If no complete cube is removed, enrich the survivors with actual outside-subset realizability rather than repeating root-cell-only inequalities.
Retain proof-producing OPB calibration as the decisive alternative once pinned RoundingSat, VeriPB, and CakePB tools are available.

Citations

Tool disclosure

GPT-5.6 Sol principal designed, implemented, executed, and interpreted this epoch. GPT-5.6 Terra delegate memos were advisory reconnaissance only and were not counted as validation or decisive evidence. Deterministic Python 3.12.3, Z3 4.13.0, exact standard-library Fraction arithmetic, the computational-researcher experiment wrapper, SHA-256, cmp, jq, py_compile, and shell inspection were used. A web fetch of the maintained source returned no rendered content, so the pre-acquired source-status audit and direct maintained URLs were retained. No CAS, proof assistant, checkpointed lab, external human validator, or proof-producing SAT/PB stack was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1090.5s
Review state: not a result claim
Attempt ID: covering-c1553-20260808-225001-1f26a5

Human review ledger

No human review recorded.