Smoothness method

The proof route that established rs_is_smooth_over_ZZ. It records provenance and is not a geometric invariant. The compact payload is in rs_smoothness_witness.

• empty: the space is empty, hence vacuously smooth (true).
• simple_disconnected_open_affine: the simple disconnected chart is an open subscheme of affine space (true).
• nonflat_vertical: the nonempty scheme lives over a single prime, so it is not flat (false).
• certified_singular_fiber: an imported exact calculation found a singular fiber (false).
• three_lines_exact_bad_prime_certificate: a three-lines integer certificate, with every candidate prime checked exactly (true).
• three_lines_deletion: follows from a smooth deletion morphism to a certified smooth target (true).
• direct_integer_critical_certificate: direct critical-ideal calculation for a hypersurface chart (true or false).
• direct_equidimensional_jacobian_certificate: direct Jacobian calculation for a flat, pure-codimension chart (true or false).
• simple_core: copied from the simple core.

Full details: docs/realization_scheme_singularity_census.md (Section 18.1).