← Exact covering number C(15,5,3)2026-08-11 09:27 UTCgpt-5.6-sol · high
Instantiate the Asin et al. shared range-cardinality network on audited canonical type-4 leaf 8, perform a no-solver exact topology/DIMACS census, and stop unless it is at least 20 percent smaller than the totalizer control.
No ProgressThe genuine shared backward-sliced Asin Card_rng encoding was generated and independently reconstructed on canonical type-4 leaf 8. It has 229510 variables and 680822 clauses, 14.5984 percent more clauses than the totalizer and 43.2480 percent above the predeclared advancement gate. All semantic and reproducibility checks passed, so the exact compiler is closed without a SAT run. No cover, branch exclusion, structural covering lemma, or bound improvement was obtained; 54 <= C(15,5,3) <= 55 remains open.
Strategy and discriminatorAsin range-cardinality-network size discriminator
Choose k as the smallest power of two above each exact target, pad only to a multiple of k, build the Card_rng half-sort/simplified-merge DAG, share lower and upper threshold subgraphs, fold false constants, and emit only ancestors of c_t and c_(t+1).
Hypothesis: After false-padding, constant folding, sharing the range-network topology, and slicing from the exact-count thresholds, the genuine Asin Card_rng encoding of all fifteen residual degree rows yields at most 475275 clauses on audited type-4 leaf 8.
Test: Generate the exact DIMACS topology without solving; require two independent recursive constructions, scalar comparator recurrences, and complete clause equality, then compare the reconstructed total with the fixed 475275-clause gate.
RationaleThe two implementations agree on every clause and row, scalar recurrences agree on comparator counts, exhaustive small cases establish the exact-cardinality semantics within the checked range, mutations fail closed, and regeneration is identical. These facts validate the census and failed gate, but provide no evidence about satisfiability of the leaf or the global covering number.
Claims requiring scrutiny- The recorded shared backward-sliced Card_rng CNF for canonical type-4 leaf 8 has exactly 229510 variables, 680822 clauses, and SHA-256 c20228c502c3886e5fa5844df45c17993315b46f6634421bf3f689895e1f579a.
- The formula is primary-semantically equivalent to the audited leaf within the exact checked encoding contract.
- The formula is 86728 clauses larger than the 594094-clause totalizer control and therefore fails the <=475275 clause gate.
- No SAT solver was run and no primary assignment or covering branch was excluded.
Evidence and scope- Producer experiment 20260811-091637-a90004 emitted 229510 variables and 680822 clauses.
- Independent experiment 20260811-091657-9d268d returned valid=true with exact clause equality and advance_gate_recomputed=false.
- Small-semantics experiment 20260811-091714-b0e035 passed 81924 network and 16 gate cases.
- Mutation experiment 20260811-091727-75f7db rejected six of six corruptions.
- Regeneration experiment 20260811-091753-77a59d reproduced both files byte-identically.
- sha256sum -c artifacts/type4-leaf8-asin-cardinality-census-20260811/manifest.sha256 passed.
Computational experiments- .proof-experiments/20260811-091637-a90004: generated 229510-variable, 680822-clause CNF; size gate false.
- .proof-experiments/20260811-091657-9d268d: independently reconstructed the full formula and 15 scalar topology rows.
- .proof-experiments/20260811-091714-b0e035: 81924 network cases and 16 gate truth tables passed.
- .proof-experiments/20260811-091727-75f7db: six corruptions rejected.
- .proof-experiments/20260811-091753-77a59d: CNF and manifest regenerated byte-identically.
Independent checkercheck_type4_leaf8_asin_cardinality_census_v1.py reconstructs block/triple incidence with integer masks, uses separately named recursive full/truncated odd-even routines, emits every clause independently, and cross-checks raw comparator counts with closed scalar recurrences.
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- Asin et al. cardinality networks -> predict k-truncation and shared range topology will beat the totalizer size gate -> exact census instead produced 680822 clauses and falsified the prediction.
Established facts- The recorded Card_rng formula contains exactly 229510 variables and 680822 clauses.
Challenger manifest, complete independent reconstruction, and byte-identical regeneration · Canonical type-4 semantic leaf 8 with the recorded input order and exact residual targets · computed - The raw comparator counts are 4947 for each width-715 row and 8978 for each width-935 row.
Two recursive builders and independent closed scalar recurrences agree on all 15 rows · Asin half-sort/simplified-merge topology padded to 720 at k=16 or 960 at k=32 · computed - The exact compiler fails the <=475275-clause advance gate.
680822 > 475275, independently reconstructed · Predeclared size-first protocol only · proved
Ruled out in this epoch- Advance the exact shared backward-sliced Asin Card_rng formula to a SAT calibration under the current size-first protocol.
Formula SHA-256 c20228c502c3886e5fa5844df45c17993315b46f6634421bf3f689895e1f579a on canonical type-4 semantic leaf 8 · Its 680822 clauses are 14.5984 percent larger than control and 43.2480 percent above the advancement threshold. · independent-check.json, result.json, small semantics, mutations, and regeneration · A materially different topology independently reconstructing to <=475275 clauses, or externally justified propagation evidence supporting a newly approved protocol rather than a larger cutoff. - Rerun the complete fixed-pair-link strengthening as a distinct route.
All 5460 labelled link requirements across four canonical types · Every requirement is a fixed-block tautology or an exact existing coverage clause, for zero logical CNF delta. · artifacts/pair-link-cnf-delta-audit-20260811/independent-check.json · Add a separately justified nonredundant pair-count, skeleton, or labelled correlation; link coverage alone cannot reopen.
Open leads- Owner-approved radius-five selector-union proof tranche
It is hash-bound, independently reconstructed, proof-capable, and materially distinct, but local and authority-gated. · After explicit approval of map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403, freeze exactly stratum 0 and run one 256-cell selector union with LRAT replay. · high · open - Genuinely new constructive exact-degree move family
A 54-block witness is the smallest terminal certificate, while previous 2-for-2, 3-for-3, and ejection neighborhoods stalled at verified defect 10. · Design a move not reducible to the closed neighborhoods and run a bounded independent replay pilot; stop unless best defect is below 10. · normal · open
Continuation checkpointObjective: Resolve authorization for the hash-bound radius-five proof tranche while keeping a terminal constructive route alive.
First action: Request explicit approval or rejection of selector-map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403; do not generate a selector union before approval.
Stop condition: Withheld approval, any map/CNF mismatch, UNKNOWN, proof-replay failure, or a directly checked 54-cover; without approval redirect to a new move-family design and stop its pilot unless defect drops below 10.
Next moves- Do not run or scale the exact Card_rng formula solely by increasing resources.
- Keep the complete fixed-pair-link route closed because its independently audited logical CNF delta is zero.
- Request explicit approval or rejection of radius-five selector-map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403 before any selector-union computation.
- If approval is unavailable, design a genuinely new constructive move family and require a verified defect below 10 before scale-up.
Citations
Tool disclosureGPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance; Sol independently audited the zero-delta fixed-pair artifact and selected discriminator, and model agreement was not validation. Python 3.12.3 generated and independently reconstructed CNF; exact integer-mask incidence, closed scalar recurrences, exhaustive Boolean evaluation, SHA-256, mutation testing, and the computational-researcher harness were used. No SAT solver, lab job, CAS, proof assistant, package installation, system change, external write, or publication was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.
- Duration
- 1581.9s
- Review state
- evidence receipt failure; not durable progress
- Attempt ID
covering-c1553-20260811-092757-449efd
Human review ledgerNo human review recorded.