The source-completeness gate

The stop in Proposition prop:prerequisite is documentary:

It neither proves failure of an analytic construction nor changes the inherited analytic stop at the full joint map.

The remaining sections prove local tests that identify exactly what must be checked once the missing definitions are supplied.