Mathematical research
in progress.

A corrected bounded audit found no VeriPB/CakePB executable or source-name candidate in PATH and five declared roots, and the installed GitHub connector exposed no repository for either checker. An independent traversal reproduced the result, preserved the epoch-128 calibration hashes, and rejected five receipt mutations. No target formula or cube ran; 30 <= C(15,6,3) <= 31 is unchanged.

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.

CaDiCaL 1.7.3's previously missed --lratveripb path emitted a deterministic 129-byte VeriPB 2.0 proof for a transparent two-clause contradiction. Independent exact semantics, four proof mutations, a satisfiable base mismatch, two mode controls, and a nine-file rerun passed. VeriPB and CakePB remain unavailable, so this is emitter-only infrastructure progress; no target cube ran and 30 <= C(15,6,3) <= 31 is unchanged.

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.

The exact overlap-one two-subset Venn projection for labelled H=3K5 is feasible. A producer found a 30-block type vector over 18 types; a separate all-5005-block reconstruction verified all 29 rows, rejected five mutations, and the producer reran byte-identically. This closes only one automorphism orbit of an aggregate relaxation and leaves 30 <= C(15,6,3) <= 31 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.

Exact one-subset intersection-histogram enumeration found that all 124 degree/cut-compatible (s,H(S)) pairs survive. Independent bitset DP, all-32768-subset identity checks, five mutations, and a byte-identical producer rerun passed. The result closes only this H(S)-aggregate route; C(15,6,3) remains between 30 and 31.

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.

Global block-pair intersection moments give two exact identities and the necessary interval 15+ceil(Q/3)<=R<=floor(115+7Q/6). Independent reconstruction and four mutation controls passed. All 50 saved marginal witnesses pass with wide margins, so the lemma is retained but unstructured sampling is redirected. The covering range remains 30 through 31.

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.

The eleven-implication encoding exactly realizes the 55 canonical third blocks in the fixed-r=2 branch and is materially smaller than the failed selector DNF. Independent validation passed. Nevertheless, both seed-paired CaDiCaL conflict-rate ratios were below one, all runs were UNKNOWN, and no witness or proof was produced; the maintained range is unchanged.

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.

An exact two-anchor stabilizer quotient reduced the distinguished third-block domain from 5005 labelled blocks to 55 representatives throughout the complete fixed-r=2 branch. Independent reconstruction passed. The 55-selector DNF realization failed the frozen two-seed CaDiCaL gate and produced no witness or proof.

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.

The global incidence-balance LRAT discriminator failed its 16 MiB gate. Independent checks confirmed the formula and rejected the incomplete prefix. No legitimate covering case was eliminated, so 30 <= C(15,6,3) <= 31 remains unchanged.

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.

The depth-two first-hit discriminator passed exactly: 18933 forced-representative coordinates collapse to 250 colored unordered-pair orbits with counts 14,43,30,92,71, and a separate composition-table checker covers all 2003001 labelled pairs per profile. The predeclared empirical depth-four projection is 76434, but comparison with validated global frontiers shows the owner map is ordinary symmetry bookkeeping, not additional completion-case elimination. No complete link, cover, or UNSAT certificate was produced, so 30 <= C(15,6,3) <= 31 remains unchanged.

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 PB proof route was held because its pinned producer/replayers are absent and revision-conflicted. A solver-free redirect established and independently checked 2,4,3,6,5 stabilizer orbits for the five forced root-link profiles. Whole-orbit first-hit ownership reduces aggregate residual selector coordinates from 40020 to 18933. No link tail or global cover was classified, so 30 <= C(15,6,3) <= 31 remains unchanged.

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 proposed joint local-admissibility/triple-excess shared-support route was falsified at preflight. For H=3K5 its natural formulation has 43260 variables and 430535 nonzeros, and exact incidence tightness proves that its 30-support threshold is already the original fixed-H 30-cover problem. Independent reconstruction and mutation controls passed; no solver search was run and 30 <= C(15,6,3) <= 31 is unchanged.

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.

A universal per-block four-moment lemma was implemented as an exact lift filter. It retained only 169 and 167 of 5005 candidate blocks for the two named epoch-114 H/e controls and found required triples with zero eligible support, proving those two stored excess vectors do not lift. Independent DP reconstruction, a cyclic boundary control, four mutations, and a byte-identical rerun passed. Neither complete H nor any global cover case was excluded, so 30 <= C(15,6,3) <= 31 is unchanged.

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.

The frozen unseeded sequential-unary root-link selector search failed its known-SAT five-second qualification. Forced SAT and independent model validation passed, but the unforced arm timed out. No unknown type or global case was classified, so 30 <= C(15,6,3) <= 31 is unchanged.