C-D23-EARLY-CUTS

D23 early-cut SOUNDNESS proved: every early cut (arithmetic realizability or refinement impropriety) is a NECESSARY condition for a bounded counterexample, so their combination discards no counterexample. Applied BEFORE the 2H reconstruction threshold, correcting D22 where the only global check waited until reconstruction

In plain language

Every early cut is proved safe: it only removes objects that a real counterexample could never be.

Exact statement

D23 early-cut SOUNDNESS proved: every early cut (arithmetic realizability or refinement impropriety) is a NECESSARY condition for a bounded counterexample, so their combination discards no counterexample. Applied BEFORE the 2H reconstruction threshold, correcting D22 where the only global check waited until reconstruction