RepresentationScanBound.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The full schedule's separator scan budget

The sharp incidence exponent combines with the actual distinct-entry resource budget at exponent exactly n/2. A single family is reused across all buckets and prefixes; the bound uses linearity rather than independence between checks.

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.resourceLambda_separator_exponent line 24
def OAI.LowSpaceSubsetSum.RepresentationSetup.scheduleScans line 55
Source documentation
The analysis records the actual scans of the full hypothetical loop; early acceptance only omits a suffix of this work.
```
def scheduleScans (B : ℕ) (families : Fin 4 → Array (Finset (Fin (2 * blockHalf n 0)))) : ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_mean_scans_half line 62
Source documentation
On the actual low-residue resource event, all buckets together satisfy the half-exponential scan bound.
```
theorem schedule_mean_scans_half (hgood : R.AllocatedResourceGood hn hlog ⟨h, r⟩) (B : ℕ) :
    let S := separatorParameters h.1.1.2 (by omega)
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.separatorParameters
def OAI.LowSpaceSubsetSum.RepresentationSetup.separatorScanBudget line 125
Source documentation
A real-valued threshold for the executable integer watchdog.
```
def separatorScanBudget : ℝ :=
…
```
def OAI.LowSpaceSubsetSum.RepresentationSetup.separatorScanLimit line 131
Source documentation
An integer watchdog threshold computed using only multiplication and natural exponentiation.
```
def separatorScanLimit : ℕ := inputScale R.input ^ 328 * 2 ^ ((n + 1) / 2)
```
Mentions: OAI.LowSpaceSubsetSum.inputScale
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.separatorScanBudget_le_limit line 133
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_scan_tail line 145