Verification: subG_subspace_sup_tail_bound chain

This file verifies that the entire proof chain from subG_subspace_sup_tail_bound through G24 (cor_2_8_mse_prob) and G25 (cor_2_9_expected_mse_bound) is complete with no sorry and only standard Lean axioms.

Proof chain

• subG_subspace_sup_tail_bound (ε-net argument, Theorem 1.19) → per_support_concentration_bound (per-support step) → sparse_ls_tail_bound (union bound over supports) → thm_2_6_sparse_ls_high_prob (Theorem 2.6 high-prob) → cor_2_8_mse_prob (G24: Corollary 2.8) → cor_2_9_expected_mse_bound (G25: Corollary 2.9)

All verified: no sorry, no custom axioms. Only standard Lean axioms (propext, Classical.choice, Quot.sound).