Query bounds and oracle-spec inclusions

This file contains preservation lemmas for structural query bounds under SubSpec lifting.

theorem OracleComp.IsQueryBoundP.liftComp_subSpec {ι τ : Type u} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type u} [h : spec ⊂ₒ superSpec] {oa : OracleComp spec α} {p : spec.Domain → Prop} [DecidablePred p] {q : superSpec.Domain → Prop} [DecidablePred q] {n : ℕ} (hpq : ∀ (t : spec.Domain), p t ↔ q (OracleSpec.SubSpec.onQuery t)) (hoa : oa.IsQueryBoundP p n) : (oa.liftComp superSpec).IsQueryBoundP q n

Predicate-targeted query bounds are preserved by lifting along a SubSpec when the target predicate agrees with the source predicate on lifted queries.

No LawfulSubSpec assumption is needed: query bounds only inspect query indices, not the distribution of responses.