Finite statistical tests as Boolean oracles -- proof internals

theorem Complexity.decodeFixedWidthBoolean?_ofFn_internal {length : ℕ} (bits : Fin length → Bool) : decodeFixedWidthBoolean? length (List.ofFn bits) = some bits

theorem Complexity.finiteTestOracle_ofFn_internal {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) (output : Fin outputLength → Bool) : finiteTestOracle test (List.ofFn output) = decide (output ∈ test)

theorem Complexity.finiteTestOracle_ofFn_eq_true_iff_internal {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) (output : Fin outputLength → Bool) : finiteTestOracle test (List.ofFn output) = true ↔ output ∈ test

theorem Complexity.finiteTestOracle_eq_false_of_length_ne_internal {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) {query : List Bool} (hlength : query.length ≠ outputLength) : finiteTestOracle test query = false