Combinatorial subset-pair unranking and streaming folds

For Boolean Möbius reconstruction of low-degree polynomials ([OAI26c], Lemma 3.3, eq. (3.10) and Proposition 3.4, pp. 24–26), the outer loop visits all subset pairs (E, U) of Fin n with #E ≤ q and U ⊆ E, weighted by (-1) ^ (#E - #U), in C_q = ∑ s ≤ min q n, 2 ^ s * n.choose s steps without materializing exponentially many subsets.

Main definitions

• Cslib.GenericRAM.SubsetPairFold.pascalTable, Cslib.GenericRAM.SubsetPairFold.subsetPairCount: dynamic-programming Pascal table and executable count C_q.
• Cslib.GenericRAM.SubsetPairFold.DecodedPair, Cslib.GenericRAM.SubsetPairFold.unrankSubsetPair, Cslib.GenericRAM.SubsetPairFold.ValidSubsetPair, Cslib.GenericRAM.SubsetPairFold.unrankValidSubsetPair, Cslib.GenericRAM.SubsetPairFold.validSubsetPairEquiv: (E, U) unranker and bijection (via Cslib.BitString.supportOfList).
• Cslib.GenericRAM.SubsetPairFold.pascalTableCertificate, Cslib.GenericRAM.SubsetPairFold.subsetPairCountCertificate, Cslib.GenericRAM.SubsetPairFold.unrankSubsetPairCertificate, Cslib.GenericRAM.SubsetPairFold.indexBody, Cslib.GenericRAM.SubsetPairFold.runPrefix, Cslib.GenericRAM.SubsetPairFold.run, Cslib.GenericRAM.SubsetPairFold.certificate: native resource certificates and streaming fold built on Cslib.GenericRAM.IndexFold.run.

Main results

• Cslib.GenericRAM.SubsetPairFold.getD_pascalTable_eq_choose, Cslib.GenericRAM.SubsetPairFold.length_encNat_mem_pascalTable_le, Cslib.GenericRAM.SubsetPairFold.subsetPairCount_eq_sum, Cslib.GenericRAM.SubsetPairFold.subsetPairCount_eq, Cslib.GenericRAM.SubsetPairFold.subsetPairCount_pos, Cslib.GenericRAM.SubsetPairFold.subsetPairCount_le_three_pow, Cslib.GenericRAM.SubsetPairFold.length_encNat_subsetPairCount_le: DP table, C_q refinement with Cslib.subsetPairCount, and binary-length bounds.
• Cslib.GenericRAM.SubsetPairFold.bijective_unrankValidSubsetPair, Cslib.GenericRAM.SubsetPairFold.nodup_map_unrankSubsetPair, Cslib.GenericRAM.SubsetPairFold.existsUnique_unrankSubsetPair, Cslib.GenericRAM.SubsetPairFold.pascalTable_polyTime, Cslib.GenericRAM.SubsetPairFold.subsetPairCount_polyTime, Cslib.GenericRAM.SubsetPairFold.unrankSubsetPair_polyTime: bijection and fun_prop polytime.
• Cslib.GenericRAM.SubsetPairFold.run_eq_foldl_map, Cslib.GenericRAM.SubsetPairFold.run_mobius_eq_sum_restricted_subsets, Cslib.GenericRAM.SubsetPairFold.computableInO, Cslib.GenericRAM.SubsetPairFold.polyBounded_space_of_polyBounded: streaming fold and space.

References

• OpenAI, The Exponential Time Hypothesis is False, Section 3.4 (Lemma 3.3, eq. (3.10)) and Section 3.5 (eq. (3.14) and Proposition 3.4), printed pp. 24–26.

def Cslib.GenericRAM.SubsetPairFold.Internal.pascalStep (width : ℕ) (rows : List (List ℕ)) : List (List ℕ)

Append one dynamic-programming Pascal row of width width to rows.

def Cslib.GenericRAM.SubsetPairFold.Internal.bucketStep (rowN : List ℕ) (state : ℕ × Option (ℕ × ℕ)) (s : ℕ) : ℕ × Option (ℕ × ℕ)

One step of scanning bucket capacities 2 ^ s * C(n, s) for s = 0, …, min q n.

def Cslib.GenericRAM.SubsetPairFold.Internal.findBucket (n q j : ℕ) (table : List (List ℕ)) : Option (ℕ × ℕ)

Locate (s, offset) for j < C_q, or none when j ≥ C_q.

def Cslib.GenericRAM.SubsetPairFold.Internal.unrankCombStep (table : List (List ℕ)) (state : (ℕ × ℕ) × List Bool) (m : ℕ) : (ℕ × ℕ) × List Bool

One step of combinatorial unranking of rank r < C(n, k) into an n-bit indicator.

def Cslib.GenericRAM.SubsetPairFold.Internal.unrankComb (n k r : ℕ) (table : List (List ℕ)) : List Bool

Unrank r < C(n, k) using table = pascalTable n into a length-n weight-k bit list.

def Cslib.GenericRAM.SubsetPairFold.Internal.scatterStep (state : ℕ × List Bool) (bitE : Bool) : ℕ × List Bool

One step of scattering low-order bits of uMask onto the true entries of indE.

def Cslib.GenericRAM.SubsetPairFold.Internal.scatterMask (indE : List Bool) (uMask : ℕ) : List Bool

Scatter the bits of uMask across the true positions of indE.

Section 1: Dynamic-programming Pascal table and exact binary clock C_q

def Cslib.GenericRAM.SubsetPairFold.pascalTable (n : ℕ) : List (List ℕ)

Dynamic-programming (n + 1) × (n + 1) Pascal table of i.choose s by row addition.

@[simp]

theorem Cslib.GenericRAM.SubsetPairFold.length_pascalTable (n : ℕ) : (pascalTable n).length = n + 1

pascalTable n has n + 1 rows.

theorem Cslib.GenericRAM.SubsetPairFold.getElem_pascalTable_eq_choose {n i s : ℕ} (hi : i < (pascalTable n).length) (hs : s < (pascalTable n)[i].length) : (pascalTable n)[i][s] = i.choose s

In-bounds lookup in pascalTable n returns i.choose s.

theorem Cslib.GenericRAM.SubsetPairFold.getD_pascalTable_eq_choose {n i : ℕ} (hi : i ≤ n) (s : ℕ) : ((pascalTable n).getD i []).getD s 0 = i.choose s

Defaulted lookup in row i ≤ n of pascalTable n equals i.choose s for every s : ℕ.

theorem Cslib.GenericRAM.SubsetPairFold.length_encNat_choose_le {n i : ℕ} (hi : i ≤ n) (s : ℕ) : (Turing.MultiTapeTM.encNat (i.choose s)).length ≤ n + 1

Every binomial coefficient i.choose s for i ≤ n has binary length at most n + 1.

theorem Cslib.GenericRAM.SubsetPairFold.length_encNat_mem_pascalTable_le {n : ℕ} {row : List ℕ} {x : ℕ} (hrow : row ∈ pascalTable n) (hx : x ∈ row) : (Turing.MultiTapeTM.encNat x).length ≤ n + 1

Every entry stored in pascalTable n has binary encoding length at most n + 1.

def Cslib.GenericRAM.SubsetPairFold.subsetPairCount (n q : ℕ) : ℕ

Executable subset-pair count C_q = ∑ s ≤ min q n, 2 ^ s * n.choose s ([OAI26c]).

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCount_eq_sum (n q : ℕ) : subsetPairCount n q = ∑ s ∈ Finset.range (min q n + 1), 2 ^ s * n.choose s

subsetPairCount n q equals ∑ s ∈ Finset.range (min q n + 1), 2 ^ s * n.choose s.

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCount_eq (n q : ℕ) : subsetPairCount n q = Cslib.subsetPairCount n q

Refinement equality equating the DP subsetPairCount to Cslib.subsetPairCount.

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCount_pos (n q : ℕ) : 0 < subsetPairCount n q

subsetPairCount n q is strictly positive for all n, q (since (∅, ∅) is always valid).

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCount_eq_three_pow_of_le {n q : ℕ} (h : n ≤ q) : subsetPairCount n q = 3 ^ n

When n ≤ q, subsetPairCount n q = 3 ^ n ([OAI26c], eq. (3.14)).

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCount_le_three_pow (n q : ℕ) : subsetPairCount n q ≤ 3 ^ n

subsetPairCount n q ≤ 3 ^ n for all n, q : ℕ.

theorem Cslib.GenericRAM.SubsetPairFold.length_encNat_subsetPairCount_le (n q : ℕ) : (Turing.MultiTapeTM.encNat (subsetPairCount n q)).length ≤ 2 * n + 1

The binary index bound subsetPairCount n q occupies at most 2 * n + 1 bits in encNat.

Section 2: Polynomial-time combinatorial (E, U) unranker and bijection

@[reducible, inline]

abbrev Cslib.GenericRAM.SubsetPairFold.DecodedPair : Type

Decoded (indE, indU, negSign) triple: length-n indicators and Odd (#E - #U) flag.

def Cslib.GenericRAM.SubsetPairFold.unrankSubsetPair (n q j : ℕ) : DecodedPair

Combinatorial (E, U) unranker: decodes j < subsetPairCount n q into (indE, indU, negSign) without materializing subsets, with deterministic empty-pair fallback for j ≥ C_q.

theorem Cslib.GenericRAM.SubsetPairFold.unrankSubsetPair_of_le {n q j : ℕ} (hj : subsetPairCount n q ≤ j) : unrankSubsetPair n q j = (List.replicate n false, List.replicate n false, false)

Out-of-range indices j ≥ subsetPairCount n q return the empty-pair fallback.

@[simp]

theorem Cslib.GenericRAM.SubsetPairFold.length_fst_unrankSubsetPair (n q j : ℕ) : (unrankSubsetPair n q j).1.length = n

The first indicator indE returned by unrankSubsetPair n q j has exact length n.

@[simp]

theorem Cslib.GenericRAM.SubsetPairFold.length_snd_unrankSubsetPair (n q j : ℕ) : (unrankSubsetPair n q j).2.1.length = n

The second indicator indU returned by unrankSubsetPair n q j has exact length n.

theorem Cslib.GenericRAM.SubsetPairFold.getD_snd_imp_fst_unrankSubsetPair (n q j i : ℕ) : (unrankSubsetPair n q j).2.1.getD i false = true → (unrankSubsetPair n q j).1.getD i false = true

Pointwise containment: every true position of indU is also true in indE.

theorem Cslib.GenericRAM.SubsetPairFold.count_true_fst_unrankSubsetPair_le (n q j : ℕ) : List.count true (unrankSubsetPair n q j).1 ≤ min q n

Weight bound: indE has at most min q n (hence at most q) true entries.

theorem Cslib.GenericRAM.SubsetPairFold.snd_snd_unrankSubsetPair_eq_decide_odd (n q j : ℕ) : (unrankSubsetPair n q j).2.2 = decide (Odd (List.count true (unrankSubsetPair n q j).1 - List.count true (unrankSubsetPair n q j).2.1))

The third component negSign is decide (Odd (indE.count true - indU.count true)).

@[reducible, inline]

abbrev Cslib.GenericRAM.SubsetPairFold.ValidSubsetPair (n q : ℕ) : Type

Valid (E, U) subset pairs on Fin n with #E ≤ q and U ⊆ E ([OAI26c]).

theorem Cslib.GenericRAM.SubsetPairFold.card_fst_supportOfList_unrankSubsetPair_le (n q j : ℕ) : (BitString.supportOfList n (unrankSubsetPair n q j).1).card ≤ q

Every decoded unrankSubsetPair n q j has #E ≤ q.

theorem Cslib.GenericRAM.SubsetPairFold.supportOfList_snd_subset_fst_unrankSubsetPair (n q j : ℕ) : BitString.supportOfList n (unrankSubsetPair n q j).2.1 ⊆ BitString.supportOfList n (unrankSubsetPair n q j).1

Every decoded unrankSubsetPair n q j satisfies U ⊆ E.

def Cslib.GenericRAM.SubsetPairFold.unrankValidSubsetPair (n q : ℕ) (j : Fin (subsetPairCount n q)) : ValidSubsetPair n q

Map a valid index j : Fin (subsetPairCount n q) to its ValidSubsetPair n q.

theorem Cslib.GenericRAM.SubsetPairFold.injective_unrankValidSubsetPair (n q : ℕ) : Function.Injective (unrankValidSubsetPair n q)

unrankValidSubsetPair n q is injective on Fin (subsetPairCount n q).

theorem Cslib.GenericRAM.SubsetPairFold.sum_two_pow_card_eq_subsetPairCount (n q : ℕ) : ∑ E ∈ Finset.univ.powerset with E.card ≤ q, 2 ^ E.card = subsetPairCount n q

Summing 2 ^ #E over all E ⊆ Fin n with #E ≤ q yields subsetPairCount n q.

theorem Cslib.GenericRAM.SubsetPairFold.card_validSubsetPair (n q : ℕ) : Fintype.card (ValidSubsetPair n q) = subsetPairCount n q

The finite type ValidSubsetPair n q has exact cardinality subsetPairCount n q.

theorem Cslib.GenericRAM.SubsetPairFold.bijective_unrankValidSubsetPair (n q : ℕ) : Function.Bijective (unrankValidSubsetPair n q)

unrankValidSubsetPair n q is a bijection onto ValidSubsetPair n q.

noncomputable def Cslib.GenericRAM.SubsetPairFold.validSubsetPairEquiv (n q : ℕ) : Fin (subsetPairCount n q) ≃ ValidSubsetPair n q

Equivalence between binary indices Fin (subsetPairCount n q) and ValidSubsetPair n q.

theorem Cslib.GenericRAM.SubsetPairFold.nodup_map_unrankSubsetPair (n q : ℕ) : (List.map (unrankSubsetPair n q) (List.range (subsetPairCount n q))).Nodup

Mapping unrankSubsetPair n q over List.range (subsetPairCount n q) has no duplicates.

theorem Cslib.GenericRAM.SubsetPairFold.existsUnique_unrankSubsetPair (n q : ℕ) {E U : Finset (Fin n)} (hE : E.card ≤ q) (hU : U ⊆ E) : ∃! j : ℕ, j < subsetPairCount n q ∧ unrankSubsetPair n q j = (List.ofFn fun (i : Fin n) => decide (i ∈ E), List.ofFn fun (i : Fin n) => decide (i ∈ U), decide (Odd (E.card - U.card)))

Exact completeness: every valid pair (E, U) with #E ≤ q and U ⊆ E is decoded at a unique index j < subsetPairCount n q.

Section 3: Plain ComputableInPolyTime and NativeCertificate witnesses

@[reducible, inline]

abbrev Cslib.GenericRAM.SubsetPairFold.encParams : ℕ × ℕ ↪ List Bool

Encoding for unary (n, q) dimension/degree parameters.

@[reducible, inline]

abbrev Cslib.GenericRAM.SubsetPairFold.encDecodedPair : DecodedPair ↪ List Bool

Encoding for decoded (indE, indU, negSign) triples.

theorem Cslib.GenericRAM.SubsetPairFold.pascalTable_polyTime : Turing.MultiTapeTM.ComputableInPolyTime pascalTable Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

pascalTable is computable in polynomial time from n in unary.

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCount_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => subsetPairCount p.1 p.2) encParams Turing.MultiTapeTM.encNat

subsetPairCount is computable in polynomial time from (n, q) in unary.

theorem Cslib.GenericRAM.SubsetPairFold.unrankSubsetPair_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℕ) => unrankSubsetPair p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair encParams Turing.MultiTapeTM.encNat) encDecodedPair

unrankSubsetPair is computable in polynomial time from (n, q) in unary and j in binary.

noncomputable def Cslib.GenericRAM.SubsetPairFold.pascalTableCertificate : NativeCertificate pascalTable Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

Native certificate for pascalTable, selected via NativeCertificate.ofPolyTime.

theorem Cslib.GenericRAM.SubsetPairFold.pascalTableCertificate_isPolynomial : pascalTableCertificate.IsPolynomial

pascalTableCertificate has polynomial time and workspace bounds.

noncomputable def Cslib.GenericRAM.SubsetPairFold.subsetPairCountCertificate : NativeCertificate (fun (p : ℕ × ℕ) => subsetPairCount p.1 p.2) encParams Turing.MultiTapeTM.encNat

Native certificate for subsetPairCount, selected via NativeCertificate.ofPolyTime.

theorem Cslib.GenericRAM.SubsetPairFold.subsetPairCountCertificate_isPolynomial : subsetPairCountCertificate.IsPolynomial

subsetPairCountCertificate has polynomial time and workspace bounds.

noncomputable def Cslib.GenericRAM.SubsetPairFold.unrankSubsetPairCertificate : NativeCertificate (fun (p : (ℕ × ℕ) × ℕ) => unrankSubsetPair p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair encParams Turing.MultiTapeTM.encNat) encDecodedPair

Native certificate for unrankSubsetPair, selected via NativeCertificate.ofPolyTime.

theorem Cslib.GenericRAM.SubsetPairFold.unrankSubsetPairCertificate_isPolynomial : unrankSubsetPairCertificate.IsPolynomial

unrankSubsetPairCertificate has polynomial time and workspace bounds.

Section 4: Streaming IndexFold combinator (SubsetPairFold.run & computableInO)

@[reducible, inline]

abbrev Cslib.GenericRAM.SubsetPairFold.encLoopAcc {β : Type} (encB : β ↪ List Bool) : (ℕ × ℕ) × β ↪ List Bool

Retained accumulator encoding pairing unary (n, q) parameters with the caller's encB.

def Cslib.GenericRAM.SubsetPairFold.indexBody {β : Type} (body : DecodedPair × β → β) (p : ℕ × (ℕ × ℕ) × β) : (ℕ × ℕ) × β

Per-index round body for IndexFold.run, retaining (n, q) and decoding j on the fly.

def Cslib.GenericRAM.SubsetPairFold.runPrefix {β : Type} (body : DecodedPair × β → β) (n q m : ℕ) (initial : β) : ℕ × (ℕ × ℕ) × β

Streaming prefix after m binary-indexed steps of IndexFold.run.

def Cslib.GenericRAM.SubsetPairFold.run {β : Type} (body : DecodedPair × β → β) (n q : ℕ) (initial : β) : β

Stream all subsetPairCount n q valid (E, U) subset pairs through IndexFold.run.

@[simp]

theorem Cslib.GenericRAM.SubsetPairFold.runPrefix_index {β : Type} (body : DecodedPair × β → β) (n q m : ℕ) (initial : β) : (runPrefix body n q m initial).1 = m

@[simp]

theorem Cslib.GenericRAM.SubsetPairFold.runPrefix_params {β : Type} (body : DecodedPair × β → β) (n q m : ℕ) (initial : β) : (runPrefix body n q m initial).2.1 = (n, q)

The retained unary parameter pair (n, q) is invariant across all streaming prefixes.

theorem Cslib.GenericRAM.SubsetPairFold.runPrefix_acc {β : Type} (body : DecodedPair × β → β) (n q m : ℕ) (initial : β) : (runPrefix body n q m initial).2.2 = List.foldl (fun (acc : β) (j : ℕ) => body (unrankSubsetPair n q j, acc)) initial (List.range m)

Every prefix accumulator equals the ordered range fold over decoded indices 0, …, m - 1.

theorem Cslib.GenericRAM.SubsetPairFold.run_eq_foldl_range {β : Type} (body : DecodedPair × β → β) (n q : ℕ) (initial : β) : run body n q initial = List.foldl (fun (acc : β) (j : ℕ) => body (unrankSubsetPair n q j, acc)) initial (List.range (subsetPairCount n q))

SubsetPairFold.run agrees with folding over List.range (subsetPairCount n q).

theorem Cslib.GenericRAM.SubsetPairFold.run_eq_foldl_map {β : Type} (body : DecodedPair × β → β) (n q : ℕ) (initial : β) : run body n q initial = List.foldl (fun (acc : β) (item : DecodedPair) => body (item, acc)) initial (List.map (unrankSubsetPair n q) (List.range (subsetPairCount n q)))

SubsetPairFold.run agrees with folding over the mapped list of decoded pairs.

theorem Cslib.GenericRAM.SubsetPairFold.run_add_eq_sum_validSubsetPairs {M : Type} [AddCommMonoid M] (n q : ℕ) (f : Finset (Fin n) → Finset (Fin n) → Bool → M) : run (fun (p : DecodedPair × M) => p.2 + f (BitString.supportOfList n p.1.1) (BitString.supportOfList n p.1.2.1) p.1.2.2) n q 0 = ∑ E ∈ Finset.univ.powerset with E.card ≤ q, ∑ U ∈ E.powerset, f E U (decide (Odd (E.card - U.card)))

Commutative-monoid accumulation via run sums over all E ⊆ Fin n (#E ≤ q) and U ⊆ E.

theorem Cslib.GenericRAM.SubsetPairFold.run_mobius_eq_sum_restricted_subsets {R : Type} [CommRing R] (n q : ℕ) (g : Finset (Fin n) → Finset (Fin n) → R) : run (fun (p : DecodedPair × R) => have term := g (BitString.supportOfList n p.1.1) (BitString.supportOfList n p.1.2.1); if p.1.2.2 = true then p.2 - term else p.2 + term) n q 0 = ∑ E ∈ Finset.univ.powerset with E.card ≤ q, ∑ U ∈ E.powerset, (-1) ^ (E.card - U.card) * g E U

Signed Möbius accumulation via run computes ∑_{#E ≤ q} ∑_{U ⊆ E} (-1) ^ (#E - #U) * g E U over any commutative ring R ([OAI26c], Lemma 3.3 eq. (3.10), Proposition 3.4).

noncomputable def Cslib.GenericRAM.SubsetPairFold.indexBodyCertificate {β : Type} {encB : β ↪ List Bool} {body : DecodedPair × β → β} (cb : NativeCertificate body (Turing.MultiTapeTM.encPair encDecodedPair encB) encB) : NativeCertificate (indexBody body) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (encLoopAcc encB)) (encLoopAcc encB)

Native certificate for one indexBody round, retaining (n, q) in unary.

noncomputable def Cslib.GenericRAM.SubsetPairFold.certificate {α β : Type} {encB : β ↪ List Bool} {encIn : α ↪ List Bool} {dim deg : α → ℕ} {initial : α → β} {body : DecodedPair × β → β} (cn : NativeCertificate dim encIn Turing.MultiTapeTM.encUnary) (cq : NativeCertificate deg encIn Turing.MultiTapeTM.encUnary) (ci : NativeCertificate initial encIn encB) (cb : NativeCertificate body (Turing.MultiTapeTM.encPair encDecodedPair encB) encB) : NativeCertificate (fun (a : α) => run body (dim a) (deg a) (initial a)) encIn encB

Native certificate for SubsetPairFold.run, built on IndexFold.certificate.

noncomputable def Cslib.GenericRAM.SubsetPairFold.decodeOverhead : ℕ → ℕ

Polynomial overhead in n + q for subsetPairCount, unranking, and index maintenance.

theorem Cslib.GenericRAM.SubsetPairFold.polynomiallyBounded_decodeOverhead : PolynomiallyBounded decodeOverhead

decodeOverhead is polynomially bounded in n + q.

theorem Cslib.GenericRAM.SubsetPairFold.computableInO {α β : Type} {encB : β ↪ List Bool} {encIn : α ↪ List Bool} {dim deg : α → ℕ} {initial : α → β} {body : DecodedPair × β → β} (cn : NativeCertificate dim encIn Turing.MultiTapeTM.encUnary) (cq : NativeCertificate deg encIn Turing.MultiTapeTM.encUnary) (ci : NativeCertificate initial encIn encB) (cb : NativeCertificate body (Turing.MultiTapeTM.encPair encDecodedPair encB) encB) (R Q B : α → ℕ) (hR : ∀ (a : α), ∀ j ≤ subsetPairCount (dim a) (deg a), cb.time (unrankSubsetPair (dim a) (deg a) j, (runPrefix body (dim a) (deg a) j (initial a)).2.2) ≤ R a) (hQ : ∀ (a : α), ∀ j ≤ subsetPairCount (dim a) (deg a), cb.space (unrankSubsetPair (dim a) (deg a) j, (runPrefix body (dim a) (deg a) j (initial a)).2.2) ≤ Q a) (hB : ∀ (a : α), ∀ j ≤ subsetPairCount (dim a) (deg a), (encB (runPrefix body (dim a) (deg a) j (initial a)).2.2).length ≤ B a) : Turing.MultiTapeTM.ComputableInO (fun (a : α) => run body (dim a) (deg a) (initial a)) encIn encB (fun (a : α) => (encIn a).length + cn.time a + cq.time a + ci.time a + decodeOverhead (dim a + deg a) + (subsetPairCount (dim a) (deg a) + 1) * (decodeOverhead (dim a + deg a) + B a + R a)) fun (a : α) => (encIn a).length + cn.space a + cq.space a + ci.space a + decodeOverhead (dim a + deg a) + B a + Q a

Streaming resource bound for SubsetPairFold.run via IndexFold.computableInO: time scales with subsetPairCount (dim a) (deg a) + 1 while live workspace is independent of C_q.

theorem Cslib.GenericRAM.SubsetPairFold.polyBounded_space_of_polyBounded {α β : Type} {encB : β ↪ List Bool} {encIn : α ↪ List Bool} {dim deg : α → ℕ} {initial : α → β} {B Q : α → ℕ} (cn : NativeCertificate dim encIn Turing.MultiTapeTM.encUnary) (cq : NativeCertificate deg encIn Turing.MultiTapeTM.encUnary) (ci : NativeCertificate initial encIn encB) (hcn : cn.IsPolynomial) (hcq : cq.IsPolynomial) (hci : ci.IsPolynomial) (hB : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) B) (hQ : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) Q) : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length + cn.space a + cq.space a + ci.space a + decodeOverhead (dim a + deg a) + B a + Q a

When dim, deg, and initial have polynomial certificates and B and Q are polynomially bounded in the input length, the live workspace of SubsetPairFold.computableInO is polynomial.