RepresentationRuntimeFavorable.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Joint runtime acceptance and full-execution budgets

All counters below are defined on the input-only schedule. The fixed solution is used only to transfer the analyzed favorable event through the exact sign-coordinate bijection and the bounded sampler coupling.

def OAI.LowSpaceSubsetSum.RepresentationScheduleData.queryCount line 22
def OAI.LowSpaceSubsetSum.RepresentationScheduleData.scanCount line 26
def OAI.LowSpaceSubsetSum.RepresentationData.sampledQueries line 35
def OAI.LowSpaceSubsetSum.RepresentationData.sampledScans line 41
def OAI.LowSpaceSubsetSum.RepresentationData.RuntimeFavorable line 49
Source documentation
The two budgets cover the entire hypothetical execution; an early stop can only remove operations. Sampler exhaustion is not a favorable output.
```
def RuntimeFavorable (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (B : ℕ) (h : D.zeroSetup.BucketTrialHistory (by omega)) : Prop :=
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_sampledQueries_eq line 63
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_sampledScans_eq line 73
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_favorable_of_favorable line 84

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bounded_runtime_favorable_probability line 98

Source documentation

One bounded run simultaneously accepts and meets both deterministic watchdog budgets with the required inverse-polynomial probability.

theorem bounded_runtime_favorable_probability (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize))
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000) (B : ℕ) :
    let hlog := representation_log_budget (by omega : 10000 ≤ n)
…

Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.representation_log_budget