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

Test every certified unrooted pair-excess skeleton using the necessary nonnegative integer triple-excess projection sum_{T contains xy} e_T = 2 + 3 s_xy.

Progress

All 41 certified unrooted pair-excess skeleton types have explicit feasible witnesses for the necessary triple-excess projection. A separate checker validated 18655 nonnegative entries and all 4305 pair equations. Three mutations were rejected, including a total-preserving unit move that reached row comparison and failed at pair (0,2). Thus the projection prunes nothing and implies neither a 54-cover nor impossibility. Pinned OPB calibration was not attempted because no local RoundingSat/VeriPB/CakePB stack exists and sandbox DNS blocks GitLab retrieval. The exact range remains 54 to 55 and all 2145 rooted cubes remain open.

Strategy and discriminator

triple-excess structural projection

Solve 455 nonnegative triple-excess variables under 105 pair equations for each of 41 skeleton quotient types, then validate every explicit witness using a separate scatter-add incidence implementation.

Hypothesis: At least one of the 41 certified unrooted pair-excess skeleton types is infeasible in the triple-excess projection and can be eliminated in bulk.

Test: Solve all 41 quotient cases and require explicit nonnegative witnesses to pass all 105 equations per case under an independently implemented checker.

Rationale

Explicit feasible witnesses decisively falsify the pruning hypothesis throughout its declared 41-type scope. Independent arithmetic replay and mutation rejection establish the computed claim, while the absence of five-block variables prevents any stronger inference.

Claims requiring scrutiny

Every one of the 41 certified unrooted pair-excess skeleton types is feasible in the nonnegative integer projection sum_{T contains xy} e_T = 2 + 3 s_xy.
The tested projection eliminates zero skeleton types.
No covering-number bound, rooted-cube status, or exact-value claim changed.

Evidence and scope

python3 scripts/triple_excess_prefilter_v1.py --manifest artifacts/joint-orbit-census-20260808/manifest.json --output artifacts/triple-excess-prefilter-20260808/result.json returned skeleton_types=41, sat_types=41, unsat_types=0.
python3 checkers/check_triple_excess_prefilter_v1.py checked 41 witnesses, 4305 pair equations, and 18655 entries with valid=true.
python3 checkers/test_triple_excess_prefilter_mutations_v1.py rejected all three mutations; the total-preserving move failed at pair equation 0,2.
sha256sum -c artifacts/triple-excess-prefilter-20260808/manifest.sha256 returned OK for all listed artifacts.
A final independent replay produced a byte-identical independent-check.json.

Computational experiments

.proof-experiments/20260808-215417-0fc7e9: Z3 4.13.0 found feasible vectors for all 41 skeleton types in 28.988 seconds.
.proof-experiments/20260808-215537-9022cc: the independent checker accepted 41 witnesses, 4305 equations, and 18655 entries in 0.179 seconds.
.proof-experiments/20260808-215537-112094: three strengthened mutations were rejected in 0.286 seconds.

Independent checker

checkers/check_triple_excess_prefilter_v1.py uses no Z3 and no producer imports; nested loops enumerate triples and scatter each coefficient into a separately indexed array of pair sums.

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

Hypergraph incidence projection -> predicted that exact pair sums and nonnegative triple multiplicities would eliminate at least one skeleton -> observed 41 of 41 feasible, rejecting the transfer as a pruning mechanism.
Adversarial software testing -> predicted that a total-preserving unit move would bypass aggregate checks and exercise row semantics -> observed rejection at pair equation (0,2).

Established facts

For every pair xy in a hypothetical 54-cover, sum_{T contains xy} e_T = 2 + 3 s_xy.
sum c_T=3 lambda_xy over the 13 triples containing xy, e_T=c_T-1, and lambda_xy=5+s_xy. · All hypothetical 54-block C(15,5,3) covers. · proved
All 41 certified unrooted skeleton types are feasible in this projection.
Forty-one explicit vectors checked against all 4305 equations and 18655 entries. · The stated necessary projection over the certified 41-type manifest. · computed

Ruled out in this epoch

Use the tested nonnegative triple-excess projection to prune any unrooted skeleton type.
All 41 certified unrooted weighted-degree-two skeleton types. · Every type has an independently checked feasible integer witness. · artifacts/triple-excess-prefilter-20260808/independent-check.json and mutation-controls.json · Introduce a strictly stronger proved projection containing outside-triple or five-block realizability information.

Open leads

Outside-triple coupling refinement over the 20 root-flow witnesses.
It can add block-relevant information absent from both exhausted conservation projections while remaining a tiny arithmetic test. · Derive one explicit inequality and test it against all 20 stored witnesses using two constructions. · high · open
Modular five-block incidence obstruction.
Membership of triple multiplicity vectors in the image of the 5-block incidence matrix modulo a small prime may detect realizability failures invisible to nonnegative pair sums. · Compute the mod-2 and mod-3 incidence ranks and test existential compatibility for the selected skeleton/root leaf before any integer scale-up. · normal · open

Continuation checkpoint

Objective: Derive one sound outside-triple coupling inequality strictly stronger than the exhausted root-flow and triple-excess projections.

First action: Load artifacts/root-flow-refinement-20260808/result.json, express outside-triple coverage in the existing 31-cell variables, and predeclare one inequality plus an independent arithmetic falsifier.

Stop condition: Close or redirect if the inequality is implied by existing conservation equations, all 20 witnesses extend through it, or independent reconstruction disagrees.

Next moves

Load the 20 root-flow witnesses and derive one outside-triple coupling inequality not implied by the existing conservation equations.
Predeclare an arithmetic falsifier and test the inequality against all 20 witnesses before adding block variables.
Keep the proof-producing OPB route blocked until a hash-identified RoundingSat, VeriPB, and CakePB bundle is locally available and passes C(5,3,2) bounds 3, 4, and 5 controls.

Citations

Tool disclosure

GPT-5.6 Sol served as principal investigator. Pre-existing GPT-5.6 Terra challenger-prior-art and experiment-verification memos were advisory only; the relied-on producer was promoted with provenance, rerun, and checked independently. Computation used Python 3.12.3, Z3 4.13.0, a standard-library checker, the deterministic experiment harness, SHA-256, Git diagnostics, and web browsing of primary sources. No RoundingSat, VeriPB, CakePB, proof assistant, cloud lab, or external solver service was run.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1191.7s
Review state: not a result claim
Attempt ID: covering-c1553-20260808-220506-ab17bb

Human review ledger

No human review recorded.