The hunt produced finite counting inequalities and an exact counting distinction invisible to the complete spectrum. It does not improve the laboratory's asymptotic zeta-zero proportion.
One fixed positive Fourier density gives multisets (0,0,0,3,6) and (0,0,1,1,4) with the same spectrum (3,1,1,0,0) and simple counts two and one. Their overlap statistics differ. For the associated spectral class, the squared-row overlap recovers the count exactly. The construction, arbitrary-size identity, and explicit limits are in COUNTING-OVERLAP.md and OVERLAP-BOUND.md.
README.md records the concave and mixed inequalities, the third-moment obstruction, all reproduction commands, and the exact scope of the eight Lean files. Successful AXLE receipts support only those formal declarations. Fourier quadrature, rational matrix enumeration, and interval evaluation provide separate checks. External review of the complete mathematical chain remains pending. Novelty is not claimed.
Negative results and limits
- Second and third moments alone do not force a gain in the general signed class. The exact nonreal-pair construction makes the fourth moment grow without a bounded normalization.
- The tested narrow and shifted mixed observers gave negative numerators. Those runs do not supply the proposed asymptotic improvement.
- The first same-kernel example lost a fourth-cycle statistic but kept the same simple count. The later counting example was needed to establish that distinction.
- Exact Möbius inversion retains its add-backs. No error in its algebra or in a published zeta estimate was established.
- The full-width fourth-cycle Fourier test exceeds the support available from the cited correlation theorem. Rearranging repeated indices does not discharge that analytic obstruction.
- The positive spectral band used by the overlap bound excludes nonreal points in the finite model. No theorem places the actual zeta counting operator in that band, and the unconditional hard-height transfer remains unproved.
These limits close the corresponding shortcuts, while leaving the explicitly conditional finite results intact. No claim here explains RH; no claim about zeta structure is promoted on the basis of these finite or random-matrix examples. The run record, including null outcomes, is RUNS.md.