Small banks extending every short partial Boolean specification

A bank of at most (4 * length + 1) * 2 ^ specified total bit strings contains an extension of every assignment on at most specified positions. This is the finite covering step in the classical partial-function synthesis construction; see Chashkin (2024), Section 2.2.

theorem Complexity.CircuitSparseSynthesis.Internal.card_extensions (length specified : ℕ) (domain : Finset (Fin length)) (small : domain.card ≤ specified) (values : Fin length → Bool) : 2 ^ length ≤ 2 ^ specified * {extension : Fin length → Bool | ∀ i ∈ domain, extension i = values i}.card

theorem Complexity.CircuitSparseSynthesis.Internal.exists_extension_bank (length specified : ℕ) : ∃ (bank : Finset (Fin length → Bool)), bank.card ≤ (4 * length + 1) * 2 ^ specified ∧ ∀ (domain : Finset (Fin length)), domain.card ≤ specified → ∀ (values : Fin length → Bool), ∃ extension ∈ bank, ∀ i ∈ domain, extension i = values i