Finite statistical tests as Boolean oracles

The canonical oracle accepts exactly the fixed-length strings in a finite statistical test and rejects every malformed-length query.

@[simp]

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

Fixed-width decoding round-trips a canonical function encoding.

@[simp]

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

The finite-test oracle answers canonical fixed-length queries by test membership.

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

The finite-test oracle returns true exactly on members of the test.

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

Every query of the wrong length is rejected.