RepresentationQueryBound.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Half-exponential reader-query bounds for the full representation loop

theorem OAI.LowSpaceSubsetSum.prefix_tasks_polynomial line 16

Source documentation

Capacity accounting with a polynomial entry envelope. This only converts counts: it does not assign unit time to a reader or a dictionary operation.

theorem prefix_tasks_polynomial {C T q m : ℕ} {u lambda x s : ℝ}
    (hu : 3 ≤ u) (hm : (m : ℝ) + 1 ≤ u)
    (hT : (C : ℝ) * T ≤ q * C + 2 * (m + 1) * (u ^ 200 * (2 : ℝ) ^ lambda))
    (hC : (2 : ℝ) ^ (s - 1) ≤ C)
    (hq : (2 : ℝ) ^ x / u ^ 2 ≤ q) (hex : lambda ≤ x + s) :
    (T : ℝ) ≤ u ^ 205 * q := by
…

theorem OAI.LowSpaceSubsetSum.reader_query_budget_polynomial line 60
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.resourceGamma_regeneration_exponent line 98
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_taskStarts_polynomial line 110
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_regeneration_resource line 136
def OAI.LowSpaceSubsetSum.RepresentationSetup.scheduleQueries line 158
Source documentation
Proof-only total query count when early acceptance is ignored.
```
def scheduleQueries (B : ℕ) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_queries_half line 163