Exact covering number C(15,5,3)

Two exhaustive encodings agree that every one of the 52,155,333 legal strict degree-preserving 3-for-3 exchanges from the pinned degree-18 defect-nine family has final defect at least ten. The seed is a strict local minimum for this move. This is local progress only; the exact range remains 54 to 55.

The matched totalizer compressed both formulas and replayed row 414 with much less proof effort, but row 343 remained UNKNOWN. The predeclared gate failed, no new assignment was excluded, and 54 <= C(15,5,3) <= 55 remains unchanged.

A deterministic nine-row literal residual pilot found one replay-verified local exclusion. Interface row 414 passes all previous capacity checks but cannot be decomposed into twelve distinct residual 4-sets; this removes its complete 547-orbit fibre from the rooted [3^5] frontier. Two rows are locally SAT and six remain UNKNOWN, so no global branch or covering number is decided.

The complete rooted [3^5] attachment family for all 353 surviving B interfaces was reduced exactly from 5,436,200 labelled relative placements to 471,270 marked-automorphism orbits. An independent signature-group implementation reproduced every canonical representative and checked every orbit count by Burnside's lemma. No orbit, interface, skeleton profile, or 54-cover was excluded; the exact range remains 54 <= C(15,5,3) <= 55.

The eight-class q=6 full-root-link native-PB pilot failed its predeclared twofold propagation gate. All 16 runs were UNKNOWN, no decision ratio was at most 0.5, no 54-cover was found, and no link was excluded. The exact range remains 54 <= C(15,5,3) <= 55.

All 1059 coincident-mark interface/profile cells survive the exact pair-count relaxation. The result is independently checked and reproducible, but it neither constructs nor excludes a 54-block cover. The maintained range remains 54 <= C(15,5,3) <= 55.

The complete triangle/coincident-mark interface was classified into exactly 575 isomorphism types. A sound point-capacity test independently rejects 222 and leaves 353. Combined with the prior ordered-distinct-mark corpus, the interface decomposition now covers all 41 pair-excess skeleton profiles. No skeleton profile, 54-cover, or exact value was settled; the maintained range remains 54 <= C(15,5,3) <= 55.

Six exact local residual kernels were generated and independently reconstructed. Both sides of the maximum representative are SAT with directly checked 12-block witnesses; four minimum/median sides remain UNKNOWN at the fixed cap. No type was excluded and the exact range remains 54 <= C(15,5,3) <= 55.

A proved point-capacity prefilter and independent implementation reject exactly 1599 of the 3770 ordered-distinct-mark two-link interfaces, leaving 2171 survivors in 25 strata. Hash checks, four mutations, and byte-identical regeneration pass. A scope audit retains three of 41 pair-excess skeleton profiles requiring coincident-mark or seven-common-triple interfaces, so the exact covering number remains 54 to 55.

The stale fixed-pair rerun was rejected. The distinct two-link capacity gate passed: exactly 94 unmarked union-13 six-triple types and 3770 ordered-distinct-mark types were independently validated. No residual kernel was solved, so 54 <= C(15,5,3) <= 55 remains open.

The pinned degree-18 defect-nine seed is a strict local minimum under degree-preserving 2-for-2 moves. There are 40,809 incidence-compatible cells, 38,941 legal nonidentity exchange occurrences, and exact minimum neighbor defect ten. No cover or global exclusion was obtained.

The complete fixed-alignment two-parent union census produced a directly and independently checked degree-18 defect-nine 54-block family. It classified 12,210 proper occurrences and proved local minimum ten over 2692 deep occurrences. The gain is shallow from one parent, so the exact crossover corpus is exhausted and the next route is local repair from the new seed. No 54-cover or exclusion was obtained.

A header-conditioned lazy internal-pair CNF was generated, independently reconstructed, regenerated byte-identically, mutation-tested, and compared against its exact header baseline at 25000 conflicts for two seeds. The extension was genuine and primary-model equivalent, but all runs stayed UNKNOWN and the required decision-plus-propagation gain failed on both seeds. No header or cover was excluded; 54 <= C(15,5,3) <= 55 remains open.

The complete degree-balanced four-delete/three-add shell contains no 54-block cover. Two different exact enumerations scored all 43928064 candidates and found minimum defect ten. A third checker directly audited a defect-ten endpoint. The global exact value remains open.

The exact degree-feasible four-delete/three-add shell around Iorio's 55-cover contains 33100 feasible deletion headers and 43928064 exact-shell candidate families. Independent reconstruction and four mutation controls passed. This is a capacity result only: no candidate was checked for triple coverage, so the exact range remains open.

The displayed q=7 link's complete internal pair-multiplicity histogram is 1^76,2^13,3^2. Therefore mu_xy-1 <= 2+3s_xy forces no internal pair-excess edge beyond the root/high-point doubled edge, and all 24 compatible skeleton types survive. Independent checking, four mutations, manifest replay, and byte-identical regeneration passed. The exact covering range is unchanged.

The 25,000-conflict pair-upper gate passed on all four globally complete canonical types. All 16 runs were UNKNOWN at exactly 25,001 conflicts, so the range remains 54 to 55. Independent reconstruction and 52 mutations passed. The two seeds traced the same algorithmic search. This validates a propagation mechanism, not a cover or exclusion.

An exact, independently checked 91-class local corpus was produced and its predeclared count-only mobility predictor was falsified. The covering range remains 54 <= C(15,5,3) <= 55.

An exact, independently checked 106-cube symmetry cover of the complete [13,2] branch was generated. The index-6 cube adds 143 earlier-orbit negations and one anchor. The matched seed-0 pilot remained UNKNOWN and increased decisions from 6488 to 7258, so the 0.8 advancement gate failed and seed 1553 was not run. The covering range remains 54 to 55.

A complete proof-capable [13,2] branch CNF and exact 52-element symmetry quotient were generated and independently checked. The quotient was operationally harmful: both seeds remained UNKNOWN and decisions rose 24.5215782984x, so the full sequential-lex compiler is closed at this protocol. No cover or branch exclusion was obtained.

A fresh exhaustive three-delete/two-add census around Iorio's 55-cover was sound but redundant. It found 684 feasible deletion headers, 15407 raw pairs, 15159 distinct candidate families after 248 retained-block rejections, zero covers, and minimum defect ten attained 88 times. A matched comparison proved exact key-and-defect equality with epoch 32, so there is no net-new result and the exact range remains 54 to 55.

All fifteen proposed q=6 neighbor-triple caps are already implied by exact nonedge-pair multiplicity and triple coverage on the canonical 15-cycle leaf. The independent checker reconstructed every relevant row and rejected five mutations. No strengthened CNF or solver run was performed. The exact range remains 54 to 55.

A proved fixed-point budget lemma and complete 41-type classification show that every q=6 point link forces its root into a triangle component of the pair-excess skeleton. Exactly 21 skeleton types contain a triangle and 20 do not. An independent checker reconstructed all inputs and agreed on 4,961 sampled link-type/skeleton-type cells. This is a scoped branch reduction only; C(15,5,3) remains between 54 and 55.

A complete exact census of the 24 newly found degree-18 defect-10 classes examined 937,780 legal degree-preserving 2-for-2 moves. None reduced defect below ten. The 142 defect-preserving endpoints comprise 105 labelled families; 62 occurrences return to the known 40-class frontier and 80 occurrences form exactly 51 additional point-isomorphism classes. This raises the independently validated local plateau from at least 40 to at least 91 classes, but the 51-class growth exceeds the predeclared 48-class stop, so further BFS is held. The exact range remains 54 <= C(15,5,3) <= 55.

The proposed closure of the sixteen saved defect-10 classes was falsified. The complete one-step frontier contains 115 defect-10 occurrences representing 91 labelled families. Eighty-six occurrences map to fifteen saved classes; the other 29 form exactly 24 additional point-isomorphism classes. The known local plateau therefore has at least forty classes. No defect below 10, 54-block cover, or exclusion of 54 was obtained, so the maintained range remains 54 <= C(15,5,3) <= 55.

The complete direct degree-preserving 2-for-2 neighborhoods of all sixteen saved defect-10 isomorphism classes were enumerated. From 22,896 deleted pairs there were 633,425 nonidentity replacement attempts, 7,076 collision rejections, and 626,349 legal simple candidates. Every class had minimum defect exactly 10; no improvement and no cover was found. Exactly 115 candidates retained defect 10. Independent reconstruction, five mutation controls, byte-identical regeneration, and a hash manifest passed. The global range remains 54 <= C(15,5,3) <= 55.

The twenty fixed-column occurrences across the four normalized branches comprise twelve distinct blocks. Each distinct block has an independently checked 16-term signed 3-trade with coefficient +1 on the target and all other terms among the 2991 retained columns. Therefore simultaneous twelve-column deletion leaves the integer incidence lattice unchanged. This closes only signed-lattice congruence filtering; the exact range remains 54 <= C(15,5,3) <= 55.

The declared saved degree-18 defect-10 corpus contains 90 distinct labelled families and exactly 16 point-isomorphism classes. The 88 Iorio radius-five minima form 14 classes, while two later persisted families form two additional singleton classes. This is an exact saved-corpus classification, not a classification of all near-covers; the maintained range remains 54 <= C(15,5,3) <= 55.

Rank-0 strict-six cell (6,7,17,19,29,53) was compiled to an independently reconstructed 14,837-variable, 51,196-clause CNF. It is UNSAT at final defect at most 9, with DRAT and LRAT independently replayed. This is a local exclusion only; 54 <= C(15,5,3) <= 55 remains unchanged.

The fixed-pair-link proposal was rejected using the prior independently checked zero-delta audit, and the already-executed joint skeleton quotient was rejected because its checked lower bound was 12,247,501 orbits. The selected constructive discriminator removed the previous pairwise separability restriction. It sampled 131,072 exact-demand profiles over 1,024 ranked deletion cells and scored 5,503,010 literal completions. Independent replay found minimum defect 11, zero positive-loss-budget winners, and no cover. The exact range remains 54 <= C(15,5,3) <= 55.

The fixed-pair-link challenger was rejected as a certified zero-delta replication. The constructive discriminator generated 32768 valid strict 6-for-6 degree-18 neighbors. Independent replay found minimum defect 11, three minimizers, and zero positive-loss-budget candidates. No cover or exclusion was obtained, so 54 <= C(15,5,3) <= 55 remains open.

The fixed-pair rerun was rejected as redundant. The radius-six MILP timed out with a valid but worse defect-13 incumbent. No move was excluded and the exact range remains open.

A frozen, prior-corpus-disjoint 512-cell lexicographic shard was produced and independently verified. Every exact-demand strict five-addition completion in these cells has residual defect at least 14. The checker replayed 626773 dual inequalities, six mutations failed, and stable bytes regenerated. This is a local one-seed classification only; 54 <= C(15,5,3) <= 55 remains open.

The immutable 256 recovery-LP dual certificates were converted to a transparent sparse integer format. Canonical size fell 12.70805448323528x and deterministic gzip size 73.82407090045537x; packed and scalar checkers verified all 373112 inequalities and the original histogram, nine mutations failed, and certificate bytes regenerated identically. This is validated infrastructure only; 54 <= C(15,5,3) <= 55 remains open.

A fixed 256-cell stratified pilot produced exact demand-recovery LP certificates for 256 previously unclassified local deletion cells. Every cell has integer residual-defect lower bound at least 11; all predeclared count, timing, and size gates passed. A materially different checker reconstructed the complete sampler and 373112 dual inequalities, seven mutations failed closed, and certificate bytes regenerated identically. The global range remains 54 <= C(15,5,3) <= 55.

The demand-aware recovery LP exactly certifies local minimum defects 10 and 11 on the two predeclared calibration cells and strictly ranks them. An independent checker replayed 2041 exact dual block inequalities, five mutations failed closed, and regeneration was byte-identical. The global range remains 54 <= C(15,5,3) <= 55.

The complete singleton minimum-unique-loss deletion class was selected from all 3162510 cells and exhaustively searched. Independent encodings agree on 6767836 threshold-relevant exact-degree completions and minimum defect 11. This excludes defect at most nine only in cell [7,17,19,30,53] and leaves 54 <= C(15,5,3) <= 55 unchanged.

The untried modular-incidence lead was executed after rejecting the stale Terra joint-census recommendation. Exact and independent calculations show that GF(2), GF(3), and the full unrestricted signed-block lattice add no constraint beyond established margins. All four normalized residual pools preserve the GF(2)/GF(3) image ranks. This is a scoped route closure, not a cover or exclusion; the exact range remains 54 <= C(15,5,3) <= 55.

The maintained range remains 54 <= C(15,5,3) <= 55. The fixed incoming boundary set has exactly one degree-compatible deletion and reproduces the known defect-10 fixture. The additional 262,144 sampled incoming families yielded 1,561 compatible moves, all with defect at least 18. This closes only random all-hitter scale-up around one seed.

The 10000-cell pilot found 10000 distinct exact states. Independent selection and coverage reconstruction agreed on every record, and five mutations failed closed. The 128x gate failed at 1.0x, so no full census or completion search ran. The range remains 54 <= C(15,5,3) <= 55.

The exact q=5,6,7 partition was compiled with 1092 variables and 6245 clauses and independently reconstructed. Every leaf remained UNKNOWN and regressed in decisions, so the route failed its gate. The range remains 54<=C(15,5,3)<=55.

The two-marked-pair saved-witness pilot failed its compression gate. All 376 joint target-witness objects are distinct stabilizer orbits; ignoring targets leaves 219 family-only orbits. The literal families have a genuine 275-unit syntactic delta, but no exhaustive family census or SAT test was performed. The exact range remains 54 <= C(15,5,3) <= 55.

A complete, independently reconstructed meet-in-the-middle census proves that one fixed strict five-deletion cell around the locked defect-10 seed cannot reach defect at most nine. Exactly 1451104 canonical completions were checked; the known boundary fixture is the unique defect-10 minimizer. This does not change the maintained range 54 <= C(15,5,3) <= 55.

The hybrid formula is exact within its independently checked encoding contract and materially smaller than the one-hot control. It did not decide the local question, failed its decision-quality gate, and produced no covering-design bound or witness. The maintained range remains 54 <= C(15,5,3) <= 55.

The complete strict 5-for-5 defect-at-most-nine local question was compiled and independently reconstructed, but CaDiCaL returned UNKNOWN at the fixed cap. No candidate, local exclusion, global bound, or exact covering value was obtained. The incomplete partial DRAT from the initial proof-producing control was removed by the runner because it was non-evidence.

The joint model represented every strict exact-degree 5-for-5 move from one defect-10 seed but timed out with another defect-10 family. Independent direct checking passed. The reported lower bound was not independently certified, so no local or global exclusion follows and 54 <= C(15,5,3) <= 55 remains open.

The fixed-pair-link challenger was rejected as zero-delta. Because the exact selector map lacked explicit owner approval, a new constructive 4-for-4 MILP pilot was run instead. It produced no family below defect 10. Independent reconstruction and byte-identical regeneration passed, but no MILP optimality certificate, 54-cover, branch exclusion, structural lemma, or bound improvement was obtained.

The 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.

An exact backward-sliced bitonic compiler produced a 618,812-variable, 1,848,728-clause audited leaf. All runs remained UNKNOWN and were worse than the totalizer on decisions, propagation, and wall time. This compiler is closed; C(15,5,3) remains between 54 and 55.

An exact Wallace compiler reduced the audited leaf to 29,681 variables and 215,899 clauses and passed independent semantic/proof checks. All matched runs remained UNKNOWN; decisions improved only 13.96 percent, so the 20-percent all-seed gate failed. The exact range remains 54 <= C(15,5,3) <= 55.

A 126,976-variable, 710,190-clause proof-capable collision CNF was independently reconstructed and tested against its unchanged leaf for three seeds. All runs were UNKNOWN, challenger decisions regressed by 13.7164 percent, and the all-seed gate failed. No cover or exclusion was obtained, so 54 <= C(15,5,3) <= 55 remains open.

A validated 13-row endpoint-collision PB encoding used only 21.0526% of the 104-row control's incidences, but reduced aggregate rlimit by 16.0463%, retained only 30.2587% of the control's saving, and regressed on type 4. The exact range remains 54 <= C(15,5,3) <= 55.

Two independent exact counts show that the 91 surviving type-4 endpoint headers support 1,203,611,004 labelled weighted internal skeletons and at least 12,247,501 joint symmetry cells. This exceeds the 1,000,000-cell materialization gate by 12.247501-fold, so explicit quotient enumeration is closed. The exact range remains 54 <= C(15,5,3) <= 55.

The omitted internal pair-excess constraint reduces the type-4 endpoint frontier from 8,281 labelled headers in 104 orbits to 7,956 in 91. Exactly 325 headers in 13 orbits are impossible. The maintained range remains 54 <= C(15,5,3) <= 55.

The stale fixed-pair-link continuation was rejected. The materially distinct endpoint skeleton-link census classified all 8,281 labelled type-4 headers into 104 stabilizer orbits and constructed a positive necessary-relaxation witness for every orbit. Independent reconstruction, byte-identical regeneration, mutation tests, and manifest replay passed. No header was excluded, no 54-cover was found, and the exact range remains 54 <= C(15,5,3) <= 55.

Exactly 1,191,854 strict neighbors across a deterministic 512-endpoint prefix were produced, regenerated, and independently reconstructed. The best covers 445 of 455 triples with degree 18 at every point and defect ten. The below-ten gate failed, so the exact covering number remains open.

The stale fixed-pair-link rerun was rejected. The exact approval-gated 3,072-cell local map was generated from all 3,162,510 deletions, independently reconstructed, mutation-tested, and regenerated byte-identically. No cell was solved, no cover or exclusion was obtained, and 54 <= C(15,5,3) <= 55 remains unchanged.

The stale fixed-pair-link continuation was rejected and a distinct 256-pair constructive discriminator was executed. Neither selector improved the defect-10 seed; proof-core weighting lost the matched comparison. Independent reconstruction and all controls passed, but no cover, exclusion, structural lemma, or covering-number improvement was obtained.

A hash-bound, independently checked 16-cube partition of the complete canonical type-4 CNF was generated and run. Every leaf returned UNKNOWN at the 2000-conflict cap. The exact range remains 54 <= C(15,5,3) <= 55.

The complete pair-link proposal was audited across all four canonical CNFs. Every labelled requirement was already present, so the logical clause delta is zero. This rules out only link-only strengthening and leaves 54 <= C(15,5,3) <= 55 unchanged.

A deterministic unary SAT formula decided the previously HiGHS-UNKNOWN row 123 as SAT after 1,031 conflicts. The exact total-85 vector passes all 105 equations and ten zero pins, so 120 weaker children survive this necessary projection. No cover or exclusion resulted; 54 <= C(15,5,3) <= 55 remains open.

The reflection normalizer of the fixed C6 action was independently classified and encoded. It produces an exact near-twofold quotient of the local weighted-size-54 selection space. The bounded CaDiCaL test remained UNKNOWN and failed both predeclared 20-percent telemetry thresholds, so no repeat or scale-up was run. The global range remains 54 <= C(15,5,3) <= 55.

The cap CNF regenerated byte-identically with 80332 variables and 481880 clauses, versus 695275 clauses for the exact-degree baseline. Both matched runs remained UNKNOWN at 25000 conflicts. The candidate reduced propagations, time, and memory but increased decisions from 59078 to 86075, so the predeclared advancement gate failed. No cover, excluded branch, or bound improvement resulted.

The stale fixed-pair rerun was rejected. A fixed C6-invariant constructive search was independently implemented and audited. Its compact encoding gives a large measured efficiency improvement but remained UNKNOWN at 25,000 conflicts. No cover or exclusion resulted, so 54 <= C(15,5,3) <= 55 remains open.

The bounded [13,2] integral census produced and independently verified exact witnesses for 12 rooted parents, covering 1,272 children in the necessary projection, then reproducibly stopped at global row 123 with HiGHS-UNKNOWN. No cover or exclusion resulted, so 54 <= C(15,5,3) <= 55 remains open.

All 2145 rooted pair-excess skeleton representatives admit exact nonnegative rational ten-zero triple-excess witnesses. Consequently all 124988 seven-zero child headers survive this necessary continuous relaxation. Independent checking, five fail-closed mutations, byte-identical regeneration, and manifest replay passed. No cover or branch exclusion was obtained, so 54 <= C(15,5,3) <= 55 remains open.

All ten rooted [3,2^6] representatives have explicit ten-zero triple-excess witnesses, so all 211 seven-zero child headers survive this necessary relaxation. Independent checking, mutation testing, regeneration, and manifest replay passed. No cover, excluded exact branch, or covering-bound improvement was obtained.

The stale fixed-pair challenger was rejected as dominated. A deterministic sequential-counter encoding of the exact orbit-27 cube was generated, independently reconstructed, exhaustively tested on small cases, mutation-tested, and compared with a fresh totalizer control. Both solver runs returned LIMIT. The sequential encoding missed both telemetry gates, so no cover, exclusion, or field-level improvement was obtained.

The exact orbit-27 unit CNF was generated at the predeclared hash, independently reconstructed, and run once at the existing 25000-conflict cap. CaDiCaL returned LIMIT. The partial DRAT is not a certificate, no cover or exclusion was obtained, and the maintained range remains 54 <= C(15,5,3) <= 55.

The fixed size-1 [3,2^6] leaf admits an independently verified exhaustive cover by 31 representative second-block cubes instead of 3002 labelled choices. Two matched solver runs left every cube unresolved. Orbit 27 nevertheless reduced decisions from 8295 to 4057, passing the continuation gate. The exact range remains 54 <= C(15,5,3) <= 55.

A proof-producing exact CNF was created for the unique size-1 rooted [3,2^6] representative and independently reconstructed clause-for-clause. Four mutations were rejected, 258 small totalizer cases passed, and the DRAT-to-LRAT smoke stack plus wrong-formula control passed. The live run returned LIMIT, so no branch was excluded and 54 <= C(15,5,3) <= 55 remains unchanged.

All five rooted [3,3,3,3,3] representatives have explicit ten-zero witnesses, so all 80 seven-zero headers in this partition survive the necessary triple-excess projection. The result is independently checked and reproducible but does not change the exact covering-number range.

All 111 rooted simple-15-cycle representatives have explicit ten-zero triple-excess witnesses. These independently certify survival of all 12,096 seven-zero headers in the complete [15] partition tranche. The result closes this necessary relaxation as a pruning mechanism for that partition but does not change 54 <= C(15,5,3) <= 55.

The deterministic first 100 of 12,096 safely quotiented [15]-skeleton headers all survive the seven-zero integer triple-excess relaxation. Independent checking and mutation controls passed. This prefix neither excludes a header nor changes 54 <= C(15,5,3) <= 55. The complete resumable run was prepared, but lab submission was blocked by a read-only service-state directory.

The globally safe 257400-header universe collapses to exactly 124988 joint orbits, eliminating 132412 orientations. This is a structural classification only; every remaining header may still be extendable.

Every hypothetical 54-cover admits one of four independently checked seven-unique-triple root normalizations. The reduction is global and exact, but all eight capped solver runs remained UNKNOWN and failed the telemetry gate. The exact range remains 54 <= C(15,5,3) <= 55.

A deterministic producer and materially different checker established that the [3,2^6] pair-excess skeleton, rooted at a doubled-edge endpoint, has a 23040-element stabilizer and exactly 14 orbits on its 1001 possible first root-link blocks. This yields a complete overlapping 14-branch extension split but excludes no branch and does not change 54 <= C(15,5,3) <= 55.

The full point-boundary census is complete. Of 32,768 boundaries, 28,054 hide at least one compatible trade and 4,714 separate all tested trades. The minimum separating size is 10, the largest hidden size is 11, and all boundaries from size 12 separate. This closes the route as a compact aggregation because a minimum separator retains 445 of 455 triple bits. The exact covering range remains 54 <= C(15,5,3) <= 55.

An exhaustive, independently reconstructed census shows that every two-point boundary in canonical fixed-family type 1 is blind to many compatible lifted-Pasch trade directions. The exact covering range remains 54 <= C(15,5,3) <= 55, and no 54-block candidate family was eliminated.

A checked lifted-Pasch-trade witness falsified the declared pair-summary/two-endpoint-boundary projection as a general completion congruence, even while the normalized pair remains in exactly five blocks. The exact range remains 54 <= C(15,5,3) <= 55.

The validated type-2 cap CNF reduced clauses from 594088 to 410049 but increased matched decisions from 54423 to 85748. Both runs stopped at the conflict limit, so the exact range remains 54 <= C(15,5,3) <= 55. Seed 1, other types, and larger cutoffs were not run.

The fixed-pair recommendation was rejected as stale, and the approval-gated layer-five job was not dispatched. A new globally complete link-cap CNF was independently reconstructed and proof-smoke validated. It reduced clauses by 30.692172% and decisions by 21.464272% at both matched seeds, but every live run remained at the conflict limit. The exact range remains 54 <= C(15,5,3) <= 55.

The globally complete native-PB pair-floor pilot was executed and independently checked. All four runs remained UNKNOWN, both seeds regressed in deterministic resource usage, and the exact covering range remains 54 to 55. Protocol v1 is closed, not the global problem.

The four-arm variable-length ejection-chain discriminator completed 32768 proposals. Although 32750 strict exact-degree replacements were generated, none improved defect 10 before acceptance. Independently checked proposed minima were 13, 17, 18, and 22. No cover or exclusion was obtained.

A deterministic global intersection-moment projection was derived, implemented, independently reconstructed, mutation-tested, and run over all 41 pair-excess skeleton types. Every saved triple-excess witness survived. This closes the aggregate envelope as a type-pruning route but leaves 54 <= C(15,5,3) <= 55 unchanged.

A deterministic 288-cell count-five repair pilot was built, independently reconstructed, and proved UNSAT as one shared-selector union CNF. All sampled deletion cells are excluded under a necessary relaxation. The result is strictly local and leaves C(15,5,3) in the maintained range 54 to 55.

drat-trim verified the locked proof and selected 80527 of 379377 source clauses. Canonical literal-multiset mapping found no missing or duplicate clauses and preserved source occurrence order. The map contains 326 coverage clauses, 28 point-degree clauses spanning 9 points, 4 global-count equivalences, and 80169 auxiliary clauses. Independent reconstruction and mutation testing passed. This is reusable infrastructure, not a layer-five or global exclusion.

A deterministic 93253-variable, 379377-clause formula representing every degree-preserving repair layer zero through four around the verified defect-10 seed was independently reconstructed and proved UNSAT. DRAT conversion and LRAT replay passed, and a wrong-formula control failed as required. Thus every 54-cover is at symmetric-difference distance at least 10 from this seed. The result is local and does not change the global range 54 to 55.

The complete strict degree-preserving 3-for-3 neighborhood of the verified defect-10 seed contains exactly 52,472,921 neighbors. Independent ordered-triple reconstruction and stratified brute controls agree. The count is 12.5105 times the scoring cap, so no neighbor was scored and no cover or global exclusion was obtained.

A deterministic uncovered-triple-guided strict 3-for-3 exact-degree trajectory completed 32,768 proposals. Independent replay matched all 30,123 legal proposals and 1,591 accepted moves, but the best defect remained 10. No cover, exclusion, or covering-number improvement was obtained.

The explicit joint pair-type/exact-skeleton header route fails its compression gate: simple 15-cycle skeletons alone require at least 65,765,700 canonical headers. Independent checking, regeneration, and mutation controls passed. No cover or solver branch was excluded, so 54 <= C(15,5,3) <= 55 remains open.

A deterministic three-basin exact-degree constructive tranche executed 786432 proposals and accepted 68396 legal 2-for-2 moves. Independent replay verified best defects 10, 27, and 26. The predeclared below-10 advance gate failed, so no 54-cover, exclusion, structural lemma, or field-level improvement was obtained.

A deterministic 260,358-variable, 1,028,222-clause BDD-CNF was generated and independently reconstructed for one joint type-4 necessary leaf. All semantic and proof-stack controls passed. CaDiCaL returned UNKNOWN at the fixed 60-second limit, so no witness, exclusion, or exact covering-number result was obtained.

The exact C3 orbit quotient and proof-producing CNFs were built and independently audited. The audit caught a duplicate-member bug in fixed triple orbits, after which every formula and pilot was regenerated. Both corrected 25000-conflict runs remained UNKNOWN. A separate exact Z15 orbit census excludes fully cyclic invariant families of size 54, but no unrestricted cover or exclusion was obtained.

The stale standalone fixed-pair-link challenger was rejected. A materially new joint skeleton/profile/coverage leaf was encoded and independently reconstructed, but Z3 returned UNKNOWN at the predeclared 90-second cap. No witness, exclusion, or exact-value progress resulted; 54 <= C(15,5,3) <= 55 remains unchanged.

A proof-producing canonical type-2 pair-cap CNF was generated and independently reconstructed. It satisfied the formula-size and validation gates but failed the performance gate: decisions rose from 54423 to 148779 at matched 25000-conflict caps. Both searches remained UNKNOWN, so the exact covering number remains unresolved.

The predeclared cross-type native-PB robustness gate passed. Types 1–3 all showed large PB-propagation and rlimit-count reductions with the implied pair bounds, supported by six independent formula reconstructions, an exact four-type audit, and 27 rejected mutations. All six searches remained UNKNOWN, so the exact covering number is unresolved.

The complete degree-compatible three-delete/two-add neighborhood contains 15159 distinct 54-block candidates and no cover. Its minimum defect is ten. This proves only a local symmetric-difference lower bound of seven from the displayed Iorio cover; C(15,5,3) remains between 54 and 55.

The pass did not produce a valid research result: TimeoutExpired: Command '['/root/.local/bin/codex', 'exec', '--ephemeral', '--json', '--sandbox', 'workspace-write', '-c', 'approval_policy="never"', '-c', 'forced_login_method="chatgpt"', '-c', 'model_reasoning_effort="high"', '--ignore-user-config', '--ignore-rules', '--model', 'gpt-5.6-sol', '-']' timed out after 7200 seconds

An auxiliary-free native-PB pair strengthening passed its predeclared propagation gate on canonical type 4. Exact counters reproduced across reruns, both formulas remained UNKNOWN, and the stricter Terra time-plus-resource advancement gate did not pass. The exact covering number remains 54 to 55.

The global pair-envelope extension was generated, independently reconstructed, mutation-tested, and compared at a matched fallback cap. It remained UNKNOWN and increased propagations by 87.9812 percent. This closes only this encoding/protocol, not any mathematical branch. The exact value remains open.

The complete labelled {4,5} link was tested across the entire frozen type-4 frontier. Exact aggregation produced 431 cells. All 754 targets survived with independently checked positive witnesses, so the relaxation has zero pruning value. This is scoped campaign progress, not a 54-cover, exclusion certificate, or exact determination.

Both complete minimum residual-triple orbits were exhaustively tested on the frozen type-4 frontier. Each retained all 395 signatures and all 754 previously skeleton-feasible signature/e_45 targets. The exact covering number remains unresolved.

The exact {4,5} pair-identity refinement retained all 395 frozen type-4 signatures. Every signature has checked residual witnesses for e_45 = 0,1,2. This closes only the one-pair necessary relaxation and does not change 54 <= C(15,5,3) <= 55.

The q=6 capacity hypothesis was falsified by 121 explicit, independently verified isomorphism classes. This is a local lower bound and route-capacity result only; the q=6 bin remains incompletely counted and C(15,5,3) remains between 54 and 55.

The prerequisite gate passed and produced independently checked research infrastructure. It did not enumerate a link frontier, solve an extension instance, produce a 54-cover, or exclude any cover. The exact range remains 54 <= C(15,5,3) <= 55.

The D15 encoding and all controls succeeded, but the solver discriminator did not. Both formulas remained UNKNOWN, and the 2.8191 percent propagation reduction missed the 20 percent retention threshold. No seed, cover, exclusion, or proof was obtained. The maintained range remains 54 <= C(15,5,3) <= 55.

The prerequisite seed gate was implemented for four canonical pair-excess skeletons. All four bounded MILPs returned UNKNOWN without incumbents, so no second seed or trade census was attempted. A materially different [15] balanced-totalizer CNF regenerated byte-identically and also returned UNKNOWN under a ten-second CaDiCaL cap. Independent structural and mutation checks passed. The exact covering number remains unresolved.

The canonical type-4 projection contains 1176 possible internal-excess vectors. The producer reported 395 skeleton-feasible vectors, and every one has both a full skeleton witness and a simultaneous exact-capacity aggregate feature witness accepted by an independent checker. Since 395 exceeds the 117-vector promotion threshold, no SAT leaves were generated. The producer's 781 negative skeleton statuses were not promoted because this epoch did not independently certify them.

A deterministic proof-capable CNF and independent checker were completed for the frozen mapping-1438 profile. Ten redundant degree totalizers were safely discharged, cutting the all-row CNF estimate by 32.83% of variables and 47.19% of clauses. All semantic, mutation, boundary, regeneration, and proof-stack controls passed. The single 110-second CaDiCaL run returned UNKNOWN, so no cover, local exclusion, or global bound was obtained.

The selected aggregate survivor was promoted to a reproducible literal-subset PB instance. Independent checks passed, but the bounded solver result was UNKNOWN. This is reusable infrastructure and a negative tractability signal, not a cover, exclusion or new bound.

The type-4 pointwise and full stabilizers were independently verified at orders 5,184 and 10,368. Sound lex CNFs were constructed and audited, but both remained UNKNOWN and nearly doubled or more than doubled propagation at the matched cap. This rejects scaling these particular encodings; it does not exclude type 4 or change the maintained 54–55 range.

A complete four-case normalization was proved and independently counted. The known 55-cover supplied a successful type-2 encoding and decoding control. All four live 54-cover branches remained UNKNOWN at 25,000 conflicts, so the maintained range remains 54–55.

The exact-cardinality C(5,3,2) OPB packet passed independent exhaustive checking, byte-identical regeneration, and semantic mutation controls. The first required pinned RoundingSat source could not be acquired because gitlab.com did not resolve, so no proof was emitted or replayed and no C(15,5,3) leaf was run. The maintained range remains 54–55.

The selected two-link canonicalization gate is complete. The full cycle group has order 30, the root stabilizer has order 2, and fixing ordered edge (0,1) leaves only the identity. Forced endpoint-triple coverage reduces the six-triple common-family frontier by factor 66.54, but 10835789965 families remain. No 54-cover was found or excluded, so the exact range remains 54–55.

The two-link representation passed its positive calibration on the maintained 55-cover. Endpoints (1,15) produce two 18-block C(14,4,2) links, each covering all 91 pairs, with six exactly shared triples. Byte-identical regeneration and three mutation controls passed. This excludes no 54-cover case, so the exact value remains unresolved.

The global root-pair sweep compressed 30,845 systems to 279 canonical signatures and independently validated 3,955 LP-infeasible profile mappings plus 25,278 integer-feasible mappings. Zero of 2,145 rooted orbits was excluded, so the exact covering number remains unresolved and this relaxation is closed at its current strength.

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.

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.

The root-31 leaf now has a canonical sparse OPB formula and independently checked semantic manifest. Exact counts are 3002 variables, 445 coverage inequalities, 105 equalities, 550 written constraints, 655 equality-expanded proof axioms, and 59390 incidence terms. Three hash-rebound mutations were rejected. No model or proof was run, so C(15,5,3) remains between 54 and 55 and all 2145 cubes remain open.

The exact byte-identical no-reflection native-PB continuation returned UNKNOWN at 250001 conflicts and produced no witness. Independent reconstruction and provenance checks passed, including two fail-closed negative controls. The covering range remains 54 to 55, every one of the 2145 cubes remains open, and further cutoff-only scaling on this leaf is closed.

The incumbent root-flow refinement was independently falsified as a reduction: all 20 profiles survive with checked integer witnesses. A new direct-PB producer and independent checker validated a 3002-variable, 550-row formulation. Z3 returned UNKNOWN at 25001 conflicts both with and without reflection, so no cover or exclusion was obtained. The no-reflection control was faster, making one larger bounded constructive test inexpensive, but all 2145 cubes remain open.

A deterministic generator and materially different checker validate the first certified exact-pair joint leaf. The final CNF has 109327 variables and 542540 clauses, with target histogram 4^6,5^88,6^11. All structural, mutation, and counter controls passed. The fixed live run returned UNKNOWN, so no cover or exclusion was obtained and all 2145 cubes remain open.

A deterministic producer and materially different checker establish exactly 2145 joint pair-excess-skeleton/root orbits. Necessary aggregate triple coverage reduces the attached root-profile layer from 54032 to 30845. No 54-cover was found and no joint orbit was excluded, so C(15,5,3) remains between 54 and 55.

The root-block encoder passed duplicate-generation, fixed SAT/UNSAT CNF and PB controls, decoder, two direct cover checkers, and 448 exhaustive cardinality tests. The live 5000-conflict run returned UNKNOWN. No 54-cover was found and no case was excluded; the exact range remains 54 to 55.

The forced-pair strengthening was implemented and validated but failed its retention threshold. All three matched formulas returned UNKNOWN, so no cover was found and no case was excluded. The durable campaign state now activates root-block-only constructive SAT.

A deterministic fixed-link residual CNF generator, decoder, protocol, and two independent global checkers were implemented. All maintained-cover and mutation controls passed, and two live CNFs regenerated byte-identically. The clean bounded live run returned UNKNOWN, so no link class or global case was eliminated and the exact range remains 54 to 55.

The local-infeasibility hypothesis was falsified. A byte-reproducible rooted CNF produced an 18-block C(14,4,2) cover with ordered degrees 7,5^13. Three materially different validations accepted the exact witness. This eliminates no global skeleton and leaves 54 <= C(15,5,3) <= 55 unchanged.

The mandatory baseline was completed without launching a frontier search. The 55-block source cover and the ordinary-profile C(14,4,2) link were directly verified. A pair-excess lemma reduces hypothetical 54-covers to 41 skeleton types. Two independent counts corrected the Terra labeled-profile total to 147267180508. The exact value remains open.