NashCompact witness compile-checks #

Compile-time type checks that the general nashCompact / sphere_nashCompact / sphereProd_nashCompact / torus2_matches_nashTorus theorems specialize cleanly to concrete instances (S¹, S², S³, S² × S³, Circle × Circle). Guards against typeclass-resolution regressions that would only surface at concrete manifolds.

Axiom guards for the top-level results live in scripts/axioms.lean; this file has no #print axioms blocks.