Verification: sanity instantiations and axiom audit

This file contains small example-level sanity checks instantiating the main results, plus #print axioms commands confirming the development depends only on mathlib's standard axioms (propext, Classical.choice, Quot.sound) — i.e. it is genuinely sorry-free.