Every finite set of at least $10^{2^{450}}$ points in the real plane has four distinct collinear points or six points which are pairwise visible with respect to the entire set. The visibility-colouring and vertex-removal stability inputs are proved in this package. The empty-convex-hexagon bound $h(6) \le 2^{428}+1$ is derived from the fully proved four-layer lemma. The empty-hexagon and stability inputs are used through their theorem interfaces so Lax records the proof tree. Both have proofs in this package; composing the tree leaves only Lean's standard logical axioms.