Existence of separated Boolean codes -- proof internals

theorem Complexity.BooleanHamming.exists_isSeparated_and_covering_internal (length minimumDistance : ℕ) : ∃ (code : Finset (Word length)), IsSeparated code minimumDistance ∧ ∀ (word : Word length), ∃ center ∈ code, distance word center ≤ minimumDistance - 1

theorem Complexity.BooleanHamming.gilbertVarshamov_bound_internal (length minimumDistance : ℕ) : ∃ (code : Finset (Word length)), IsSeparated code minimumDistance ∧ 2 ^ length ≤ code.card * volume length (minimumDistance - 1)