Research proof index

Taking the first component of the WriterT output recovers the original computation, when the query implementation preserves the underlying oracle behavior (hso).

The number of uniform-oracle calls made by generateSeed spec qc js is exactly (js.map fun j => qc j * sampleCost j).sum, with each of the qc j samples at oracle j costing sampleCost j.

Predicate-targeted analogue of isTotalQueryBound_iff_counting_total_le: a counting-oracle filtered-sum bound characterizes the structural IsQueryBoundP bound.

Soundness: any path of the counting-oracle simulation of a p-bounded computation has sum of per-index counts over p-indices at most 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.

Every counting-oracle support point of the body oa lifts to a counting-oracle support point of replicate n oa whose query count is n times the body's. -/ private lemma countingOracle.support_simulate_replicate_const [DecidableEq ι] {oa : OracleComp spec α} {z : α × QueryCount ι} (hz : z ∈ support (countingOracle.simulate oa 0)) : ∀ n, ∃ ys, (ys, fun...