RepresentationSamplerWork.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Candidate and divisor counts for the representation sampler

The counts include all n³ attempts on exhaustion. Family occurrences are counted separately even when their sampled subsets coincide. These are candidate-read and remainder-test counts, before the word-operation ledger.

def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.rangeCalls line 24
Source documentation
The actual number of permutation range calls for all four families.
```
def rangeCalls : ℕ := ∑ i : Fin 4, S.counts i * g
```
theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.rangeCalls_le line 26
def OAI.LowSpaceSubsetSum.RepresentationSetup.samplerPrimeWidths line 40
Source documentation
The low factors and the extra prime, in their sampling order. Factors whose width is below four use the constant one and incur no prime test.
```
def samplerPrimeWidths (z : Layout n) : Fin 4 → ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.factorExponents_le_half line 44
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.halfSize_rate line 58
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.samplerPrimeWidths_rate line 67
Source documentation
The 0.258 n bound includes both floor losses.
```
theorem samplerPrimeWidths_rate (z : Layout n) (hn : 100 ≤ n) (i : Fin 4) :
    (R.samplerPrimeWidths z i : ℝ) ≤ (129 / 500 : ℝ) * n := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.sampler_divisor_exponent line 81
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.sampler_divisor_bound line 90
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.separator_width_rate line 99
def OAI.LowSpaceSubsetSum.RepresentationSetup.actualRangeCalls line 105
Source documentation
The calls outside the families are the whole-input permutation, three block permutations, three size guesses, and three low-residue draws.
```
def actualRangeCalls (h : R.PrimeHistory) (hn : 2200 ≤ n) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actualRangeCalls_le line 108
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rangeCallBound_half line 113
def OAI.LowSpaceSubsetSum.RepresentationSetup.samplerCandidateBudget line 143
Source documentation
Upper tally of the random candidates read, including all four possible prime calls and one direct Boolean draw for each sign coordinate.
```
def samplerCandidateBudget : ℕ := n + n ^ 3 * (R.rangeCallBound + 4)
```
def OAI.LowSpaceSubsetSum.RepresentationSetup.samplerDivisorBudget line 146
Source documentation
Each term is the all-attempts bound for the counted primeRun.
```
def samplerDivisorBudget (z : Layout n) : ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.samplerDivisorBudget_half line 149
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.sampler_operations_half line 163