Lean proofs of constructive binary X-ray families, counting bounds, and an extension theorem