IV.R69 — The role of NF Discreteness

NF Discreteness (III.P16) is the lynchpin of the gap theorem: it guarantees |C_n^{adm}| < infinity at each stage, converting infima into minima, so the minimum of a positive finite set is necessarily positive.