Streaming first-match search on Boolean words

The width is a runtime unary natural. The test receives the retained context and one Boolean word, and the search retains at most one matching word. The implementation uses BooleanFold; the list of all words occurs only in the correctness specification.

This supplies the unrestricted representative scan of [OAI26f], Lemma 3.2, printed p. 23. In that application the test checks measurements, without the fixed-bit restriction used in the second scan. This module does not implement that second scan or the counting algorithm.

Main definitions

• Cslib.GenericRAM.BooleanSearch.run: first matching word, or none.
• Cslib.GenericRAM.BooleanSearch.runPrefix: the complete state after a prefix of the traversal.
• Cslib.GenericRAM.BooleanSearch.certificate: native search from a supplied native test.

Main results

• Cslib.GenericRAM.BooleanSearch.run_eq_find?: equality with the existing enumeration's search.
• Cslib.GenericRAM.BooleanSearch.run_eq_none_iff, Cslib.GenericRAM.BooleanSearch.run_some: completeness and soundness.
• Cslib.GenericRAM.BooleanSearch.length_prefix_le: complete live-state bound at every prefix.
• Cslib.GenericRAM.BooleanSearch.exists_computableInO: traversal-proportional time and polynomial workspace when the test has polynomial resource bounds.

References

• OpenAI, The Exponential Time Hypothesis is False, Lemma 3.2, pp. 22–23.

@[reducible, inline]

abbrev Cslib.GenericRAM.BooleanSearch.encResult : Option (List Bool) ↪ List Bool

An optional Boolean word: none is empty; some has a leading true followed by the list encoding, which frames each bit.

@[reducible, inline]

abbrev Cslib.GenericRAM.BooleanSearch.encTestInput {C : Type} (encC : C ↪ List Bool) : C × List Bool ↪ List Bool

A context paired with a Boolean word: the context is framed, followed by the list encoding, which frames each bit.

def Cslib.GenericRAM.BooleanSearch.step {C : Type} (test : C × List Bool → Bool) (p : (ℕ × List Bool) × C × Option (List Bool)) : C × Option (List Bool)

Retain the context and the first match, using the existing list-search step.

def Cslib.GenericRAM.BooleanSearch.runPrefix {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) : ℕ × ℕ × C × Option (List Bool)

Prefix state: binary index, unary width, context and at most one matching word.

def Cslib.GenericRAM.BooleanSearch.run {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) : Option (List Bool)

Stream all words of the runtime width and return the first match in enumeration order. After finding a match the traversal retains it and makes no further calls to the test.

theorem Cslib.GenericRAM.BooleanSearch.prefix_accumulator {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) : (runPrefix test p j).2.2 = (p.1, List.find? (fun (w : List Bool) => test (p.1, w)) (List.map (BitString.lowBits p.2) (List.range j)))

Every prefix retains the original context and the first match among the visited words. The list on the right is specification-only, not a stored traversal history.

theorem Cslib.GenericRAM.BooleanSearch.run_eq_find? {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) : run test p = List.find? (fun (w : List Bool) => test (p.1, w)) (BitString.enumList p.2)

The streaming result has exactly the first-match semantics of the existing enumeration.

theorem Cslib.GenericRAM.BooleanSearch.run_eq_some_iff {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (word : List Bool) : run test p = some word ↔ test (p.1, word) = true ∧ ∃ (before : List (List Bool)) (after : List (List Bool)), BitString.enumList p.2 = before ++ word :: after ∧ ∀ w ∈ before, test (p.1, w) = false

A returned word passes the test and every earlier word in enumeration order fails it.

theorem Cslib.GenericRAM.BooleanSearch.prefix_some {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) {word : List Bool} (h : (runPrefix test p j).2.2.2 = some word) : word.length = p.2 ∧ test (p.1, word) = true

A match retained at any prefix has the requested width and passes the test.

theorem Cslib.GenericRAM.BooleanSearch.run_some {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) {word : List Bool} (h : run test p = some word) : word.length = p.2 ∧ test (p.1, word) = true

Every returned word has the requested width and passes the test.

theorem Cslib.GenericRAM.BooleanSearch.run_eq_none_iff {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) : run test p = none ↔ ∀ (word : List Bool), word.length = p.2 → test (p.1, word) = false

Failure means that no word of the requested width passes the test.

theorem Cslib.GenericRAM.BooleanSearch.run_ne_none_iff {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) : run test p ≠ none ↔ ∃ (word : List Bool), word.length = p.2 ∧ test (p.1, word) = true

A word satisfying the test exists exactly when the streaming search returns a word.

theorem Cslib.GenericRAM.BooleanSearch.length_prefix_result_le {C : Type} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) : (encResult (runPrefix test p j).2.2.2).length ≤ 3 * p.2 + 1

A prefix stores at most one width-sized result, including the option tag and list framing.

theorem Cslib.GenericRAM.BooleanSearch.length_prefix_accumulator_le {C : Type} {encC : C ↪ List Bool} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) : ((Turing.MultiTapeTM.encPair encC encResult) (runPrefix test p j).2.2).length ≤ 2 * (encC p.1).length + 3 * p.2 + 2

The complete captured accumulator has polynomial size at every prefix, independently of the number of visited assignments.

theorem Cslib.GenericRAM.BooleanSearch.length_prefix_le {C : Type} {encC : C ↪ List Bool} (test : C × List Bool → Bool) (p : C × ℕ) (j : ℕ) (hj : j ≤ 2 ^ p.2) : ((BooleanFold.encStreamState (Turing.MultiTapeTM.encPair encC encResult)) (runPrefix test p j)).length ≤ 2 * (encC p.1).length + 7 * p.2 + 6

The full index/width/context/result state stays polynomial even at the terminal prefix.

noncomputable def Cslib.GenericRAM.BooleanSearch.stepCertificate {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (encTestInput encC) Turing.MultiTapeTM.encBool) : NativeCertificate (step test) (BooleanFold.encCallbackInput (Turing.MultiTapeTM.encPair encC encResult)) (Turing.MultiTapeTM.encPair encC encResult)

Certify the captured search step with an arbitrary native test. The outer branch skips the test when a word has already been found; the decoder's bit word is converted to the agreed list encoding before invoking the test.

theorem Cslib.GenericRAM.BooleanSearch.stepCertificate_isPolynomial {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (encTestInput encC) Turing.MultiTapeTM.encBool) (hct : ct.IsPolynomial) : (stepCertificate ct).IsPolynomial

A polynomial native test gives a polynomial step in the complete captured input encoding. This does not assert polynomial time for the exponential traversal.

noncomputable def Cslib.GenericRAM.BooleanSearch.certificate {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (encTestInput encC) Turing.MultiTapeTM.encBool) : NativeCertificate (run test) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) encResult

One fixed native machine searches all runtime widths and contexts. Its independently charged time and space bounds are those of the binary streaming iterator, including count preparation, initialization, decoding, the selected test calls and output projection.

theorem Cslib.GenericRAM.BooleanSearch.exists_computableInO_of_visit_bounds {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (encTestInput encC) Turing.MultiTapeTM.encBool) {R Q : C × ℕ → ℕ} (hR : ∀ (p : C × ℕ), ∀ j ≤ 2 ^ p.2, (BooleanFold.visitCertificate (stepCertificate ct)).time (runPrefix test p j) ≤ R p) (hQ : ∀ (p : C × ℕ), ∀ j ≤ 2 ^ p.2, (BooleanFold.visitCertificate (stepCertificate ct)).space (runPrefix test p j) ≤ Q p) : ∃ (overhead : C × ℕ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) overhead ∧ Turing.MultiTapeTM.ComputableInO (run test) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) encResult (fun (p : C × ℕ) => (2 ^ p.2 + 1) * (overhead p + R p)) fun (p : C × ℕ) => overhead p + Q p

Search with independent bounds on the reachable visits. The bounds R and Q need not be polynomial; the traversal count multiplies time only. All fixed preparation and state costs are included in the polynomial overhead.

theorem Cslib.GenericRAM.BooleanSearch.exists_computableInO_of_bounds {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (encTestInput encC) Turing.MultiTapeTM.encBool) {T S : C × ℕ → ℕ} (hT : ∀ (p : C × ℕ) (w : List Bool), w.length = p.2 → ct.time (p.1, w) ≤ T p) (hS : ∀ (p : C × ℕ) (w : List Bool), w.length = p.2 → ct.space (p.1, w) ≤ S p) : ∃ (overhead : C × ℕ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) overhead ∧ Turing.MultiTapeTM.ComputableInO (run test) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) encResult (fun (p : C × ℕ) => (2 ^ p.2 + 1) * (overhead p + T p)) fun (p : C × ℕ) => overhead p + S p

Search with arbitrary, independent bounds on the original test. Only the fixed traversal machinery is polynomial: T and S are any uniform bounds over the candidates of the runtime width. Exponentially many visits multiply time, while their workspace is reused.

theorem Cslib.GenericRAM.BooleanSearch.exists_computableInO {C : Type} {encC : C ↪ List Bool} {test : C × List Bool → Bool} (ct : NativeCertificate test (encTestInput encC) Turing.MultiTapeTM.encBool) (hct : ct.IsPolynomial) : ∃ (overhead : C × ℕ → ℕ) (workspace : C × ℕ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) overhead ∧ Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) workspace ∧ Turing.MultiTapeTM.ComputableInO (run test) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) encResult (fun (p : C × ℕ) => (2 ^ p.2 + 1) * overhead p) workspace

With a polynomial test, search takes the traversal count times polynomial overhead and only polynomial charged workspace. The two polynomials and the realizing machine are fixed before the runtime context and width. In particular, the traversal count does not enter space.