On 7 and 8 September 2026 programmatic search produced singularities: a forced Navier-Stokes singularity at every fixed viscosity, statements (C) and (D) of the Clay problem, and two Euler singularities. The unforced problem, statements (A) and (B), stands open, and a search for it needs a target. This paper fixes one: the positive defect problem, that a Leray-Hopf solution from smooth data on the periodic cube loses energy on a finite window, at fixed viscosity, beyond what viscosity removes. A positive defect implies blowup and so a negative answer to statement (B); the converse is not known. The paper proves the target equivalent to a floor on the energy flux through the Littlewood-Paley shells, the Fourier-side form of the coarse-grained flux of the Onsager theory of turbulence, averaged over the window; states necessary conditions on a candidate: a singular time of Type II in velocity, energy concentrating on a set of zero length, a pressure outside L^2, a velocity outside the Onsager-critical class L^3_t B^{1/3}_{3,c_0}, an obstruction to collapse onto a fixed steady Euler profile; and states what cannot certify one: no finite computation witnesses a Galerkin-uniform ceiling, and selection and forcing return the question to a positive defect. A pseudo-spectral search at 128^3 and 256^3 shows which condition of the reduction binds: the fine-shell flux floor holds to within 1 to 6 percent of the ceiling for a third of a turnover time, and fails in scale at the Kolmogorov wavenumber, so a candidate must differ from generic turbulence in the depth of its cascade, not in its timing. Every implication not marked otherwise is a theorem in Lean 4 over Mathlib; the library contains no Navier-Stokes object, and the equation enters only through hypotheses.