RepresentationLeafWork.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Counted raw-leaf generation and sorting setup

Feasibility is checked before constructing any component family. Conversion of an index list to a finite mask is charged quadratically in the ambient index count; every generated list has length at most that count.

def OAI.LowSpaceSubsetSum.RepresentationLeaf.domainSort line 22
Source documentation
Scan the ambient indices in order. The quadratic charge includes membership tests against a list representation of the finite domain.
```
def domainSort (V : Finset (Fin n)) : List (Fin n) × ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.domainSort_value line 25
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.domainSort_length line 35
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.domainSort_work line 38
def OAI.LowSpaceSubsetSum.RepresentationLeaf.countedEnumerate line 42
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.countedEnumerate_value line 57
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.countedEnumerate_work line 71
def OAI.LowSpaceSubsetSum.RepresentationLeaf.countedArray line 136
Source documentation
The filter counter records predicate calls and output-array writes. The cost of the predicate itself is handled separately.
```
def countedArray (L : RepresentationLeaf (Fin n)) (accept : Occurrence (Fin n) → Bool) :
    Array (Occurrence (Fin n)) × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationLeaf.Occurrence
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.countedArray_value line 141
theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.countedArray_work line 146
def OAI.LowSpaceSubsetSum.RepresentationPairData.countedArrays line 164
Source documentation
Counted generation, prefix filtering, and sorting of the two stored leaf arrays. No row is materialized by this setup.
```
def countedArrays : (Array (Occ (n := n)) × Array (Occ (n := n))) × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationPairData.Occ
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.countedArrays_value line 170
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.countedArrays_work line 174
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_capacity line 195

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_pair_setup_work line 207

Source documentation

Every residue, prefix, and sampler outcome uses the same setup bound. The statement includes unsuccessful and overflowing tasks.

theorem schedule_pair_setup_work (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000)
    (q : ℕ) (hq : 0 < q) (z : ℕ) (side : Fin 2) (P : MaskRestriction n) (child : Fin 2) :
    let D := ({ (R.scheduleData h r hn hlog q hq).parentData side z with maskRestriction := P }).pair child
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.MaskRestriction