Polynomial-time bit-list operations

Raw bit strings and framed lists share the list and iteration calculus. Captured traversals, Boolean folds, pointwise operations, majority and selected mask sums have compositional certificates. Runtime dimensions are computed in unary. Enumeration additionally requires a polynomial bound on the complete encoded output. The operations are total on empty and short lists.

Main results

• Turing.MultiTapeTM.ofBits_reverse: agreement of the two binary-word conventions.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsBinaryValue: binary-valued word decoding.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsLow: fixed-width low-order binary digits.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsToList, .listToBits: encoding conversion.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsFlatten: concatenate computed raw words.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.flatMapToBitsWithInput: concatenate captured words over a framed list.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsFrame, .bitsPadWord: self-delimiting framing and bounded padding, including arbitrary encoded inputs and overlong words.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsGetElem?: optional lookup in raw bits.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapToBitsWithInput, .bitsFilterWithInput, .bitsAnyWithInput, .bitsFoldlWithInput, .bitsZipWithInput, and Turing.MultiTapeTM.ComputableInPolyTime.bitsAllWithInput: compositional bit operations.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsStrictMajority, .bitsSingle, .bitsSingles, .bitsXorSelected, .bitsXorWithInput: finite-mask algorithms.
• Turing.MultiTapeTM.ComputableInPolyTime.bitsCountPWithInput, Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsCountWithInput: unary counts under captured predicates or computed labels.
• Turing.MultiTapeTM.ComputableInPolyTime.bitsNonpositiveMarginWithInput: compare the correct-vote count with the word length.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsEnumList: output-bounded enumeration.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsBoundedBinaryValue: capped binary decoding to unary, with every intermediate accumulator bounded by the supplied cap.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsReplicate: repeat a fixed bit.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsWordLt: lexicographic word comparison.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsRowWithInput: read one fixed-width row.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsRowsWithInput: read a runtime number of rows.

References

Adapted from Computability/Probabilistic/BitString.lean and Computability/Probabilistic/UniformNat.lean and Crypto/Computational/GoldreichLevin/WordDecoder.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the tidy machine calculus.

theorem Turing.MultiTapeTM.ofBits_reverse (w : List Bool) : ofBits w.reverse = Cslib.BitString.binaryValue w

Reversing a most-significant-first word gives its little-endian binary decoding.

theorem Turing.MultiTapeTM.length_encList_enumList (count : ℕ) : ((encList encBits) (Cslib.BitString.enumList count)).length = 2 ^ count * (2 * count + 1)

The encoding charges every bit and every delimiter in the enumerated words.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsFrame {α : Type} (enc : α ↪ List Bool) : ComputableTidilyInPolyTime (fun (a : α) => frame (enc a)) enc encBits

Frame the existing input encoding, charging every delimiter.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsBoundedBinaryValue : ComputableTidilyInPolyTime (fun (p : ℕ × List Bool) => Cslib.BitString.boundedBinaryValue p.1 p.2) (encPair encUnary encBits) encUnary

Saturating binary decoding to unary is polynomial time on arbitrary input words.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsBoundedBinaryValueWithInput {α : Type} {input : α ↪ List Bool} {cap : α → ℕ} {word : α → List Bool} (hcap : ComputableTidilyInPolyTime cap input encUnary) (hword : ComputableTidilyInPolyTime word input encBits) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.boundedBinaryValue (cap a) (word a)) input encUnary

Decode computed bits under a computed unary cap, fixing both intermediate encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_to_unary_bounded {α : Type} {input : α ↪ List Bool} {value bound : α → ℕ} (hvalue : ComputableTidilyInPolyTime value input encNat) (hbound : ComputableTidilyInPolyTime bound input encUnary) (hle : ∀ (a : α), value a ≤ bound a) : ComputableTidilyInPolyTime value input encUnary

Convert a binary value to unary under a computed unary bound.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsToList : ComputableTidilyInPolyTime (fun (l : List Bool) => l) encBits (encList encBool)

Convert a raw bit string to the framed list encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsGetElem? {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {index : α → ℕ} (hlist : ComputableTidilyInPolyTime list input encBits) (hindex : ComputableTidilyInPolyTime index input encUnary) : ComputableTidilyInPolyTime (fun (x : α) => (list x)[index x]?) input (encOption encBool)

Optional lookup in a raw bit string, fixing the representation of the returned bit.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.listToBits : ComputableTidilyInPolyTime (fun (l : List Bool) => l) (encList encBool) encBits

Remove the framing from a list of bits.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsReplicate (bit : Bool) : ComputableTidilyInPolyTime (fun (n : ℕ) => List.replicate n bit) encUnary encBits

Repeat a fixed bit a unary number of times.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsFlatten {α : Type} {input : α ↪ List Bool} {words : α → List (List Bool)} (hwords : ComputableTidilyInPolyTime words input (encList encBits)) : ComputableTidilyInPolyTime (fun (a : α) => (words a).flatten) input encBits

Concatenate computed raw words, fixing the intermediate list encoding before proof search.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsPadWord {α : Type} {input : α ↪ List Bool} {bound : α → ℕ} {word : α → List Bool} (hbound : ComputableTidilyInPolyTime bound input encUnary) (hword : ComputableTidilyInPolyTime word input encBits) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.padWord (bound a) (word a)) input encBits

Self-delimiting padding uses ordinary framing and unary arithmetic.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapToBitsWithInput {α : Type} {input : α ↪ List Bool} {β : Type} {enc : β ↪ List Bool} {list : α → List β} {f : α → β → Bool} (hlist : ComputableTidilyInPolyTime list input (encList enc)) (hf : ComputableTidilyInPolyTime (fun (p : α × β) => f p.1 p.2) (encPair input enc) encBool) : ComputableTidilyInPolyTime (fun (a : α) => List.map (f a) (list a)) input encBits

Map a captured Boolean-valued function over a framed list, emitting a raw bit string.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.flatMapToBitsWithInput {α : Type} {input : α ↪ List Bool} {β : Type} {enc : β ↪ List Bool} {list : α → List β} {f : α → β → List Bool} (hlist : ComputableTidilyInPolyTime list input (encList enc)) (hf : ComputableTidilyInPolyTime (fun (p : α × β) => f p.1 p.2) (encPair input enc) encBits) : ComputableTidilyInPolyTime (fun (a : α) => List.flatMap (f a) (list a)) input encBits

Concatenate captured raw bit strings over a framed list. The complete intermediate words and their framing are charged before concatenation. Apply this rule explicitly: registering both raw and framed flatMap outputs makes existing enumeration proof search exceed its limit.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsLow {α : Type} {input : α ↪ List Bool} {width value : α → ℕ} (hwidth : ComputableTidilyInPolyTime width input encUnary) (hvalue : ComputableTidilyInPolyTime value input encNat) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.lowBits (width a) (value a)) input encBits

Emit a computed unary number of low-order digits of a computed binary natural. The width charges every output bit, including leading zero digits.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsMapWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {f : α → Bool → Bool} (hlist : ComputableTidilyInPolyTime list input encBits) (hf : ComputableTidilyInPolyTime (fun (p : α × Bool) => f p.1 p.2) (encPair input encBool) encBool) : ComputableTidilyInPolyTime (fun (a : α) => List.map (f a) (list a)) input encBits

Map a captured Boolean operation over a raw bit string.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsFilterWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {test : α → Bool → Bool} (hlist : ComputableTidilyInPolyTime list input encBits) (htest : ComputableTidilyInPolyTime (fun (p : α × Bool) => test p.1 p.2) (encPair input encBool) encBool) : ComputableTidilyInPolyTime (fun (a : α) => List.filter (test a) (list a)) input encBits

Filter a raw bit string with a predicate that may capture its original input.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsCountWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {value : α → Bool} (hlist : ComputableTidilyInPolyTime list input encBits) (hvalue : ComputableTidilyInPolyTime value input encBool) : ComputableTidilyInPolyTime (fun (x : α) => List.count (value x) (list x)) input encUnary

Count occurrences of a computed bit in a raw bit string.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsAnyWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {test : α → Bool → Bool} (hlist : ComputableTidilyInPolyTime list input encBits) (htest : ComputableTidilyInPolyTime (fun (p : α × Bool) => test p.1 p.2) (encPair input encBool) encBool) : ComputableTidilyInPolyTime (fun (a : α) => (list a).any (test a)) input encBool

Test whether any bit satisfies a captured predicate.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsFoldlWithInput {α : Type} {input : α ↪ List Bool} (op : Bool → Bool → Bool) {list : α → List Bool} {init : α → Bool} (hlist : ComputableTidilyInPolyTime list input encBits) (hinit : ComputableTidilyInPolyTime init input encBool) : ComputableTidilyInPolyTime (fun (a : α) => List.foldl op (init a) (list a)) input encBool

A Boolean fold has constant-sized state, so no separate state bound is needed.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsZipWith (op : Bool → Bool → Bool) : ComputableTidilyInPolyTime (fun (p : List Bool × List Bool) => List.zipWith op p.1 p.2) (encPair encBits encBits) encBits

Apply a fixed Boolean operation pointwise, stopping at the shorter word.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsZipWithInput {α : Type} {input : α ↪ List Bool} (op : Bool → Bool → Bool) {left right : α → List Bool} (hleft : ComputableTidilyInPolyTime left input encBits) (hright : ComputableTidilyInPolyTime right input encBits) : ComputableTidilyInPolyTime (fun (a : α) => List.zipWith op (left a) (right a)) input encBits

Pointwise operations on computed words, with both intermediate encodings fixed.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsStrictMajority : ComputableTidilyInPolyTime Cslib.BitString.listStrictMajority encBits encBool

Strict majority uses filtering, length, unary multiplication and comparison.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsStrictMajorityWithInput {α : Type} {input : α ↪ List Bool} {votes : α → List Bool} (hvotes : ComputableTidilyInPolyTime votes input encBits) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.listStrictMajority (votes a)) input encBool

Strict majority of computed votes fixes the intermediate raw-word encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsSingle : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => Cslib.BitString.listSingle p.1 p.2) (encPair encUnary encUnary) encBits

Generate one coordinate mask from its unary width and index.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsSingles : ComputableTidilyInPolyTime Cslib.BitString.listSingles encUnary (encList encBits)

Generate all coordinate masks, charging for their quadratic total size.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsXorSelected : ComputableTidilyInPolyTime (fun (p : ℕ × List Bool × List (List Bool)) => Cslib.BitString.listXorSelected p.1 p.2.1 p.2.2) (encPair encUnary (encPair encBits (encList encBits))) encBits

Sum selected rows with a shrinking selector and an accumulator that never grows.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsEnumList {α : Type} {input : α ↪ List Bool} {count : α → ℕ} (hcount : ComputableTidilyInPolyTime count input encUnary) {size : ℕ → ℕ} (hsize : Cslib.PolynomiallyBounded size) (hbudget : ∀ (a : α), 2 ^ count a * (2 * count a + 1) ≤ size (input a).length) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.enumList (count a)) input (encList encBits)

Enumerate words only when their complete encoded size is polynomially bounded. This does not claim polynomial time in the number of enumerated bits.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsRowWithInput {α : Type} {input : α ↪ List Bool} {width row : α → ℕ} {word : α → List Bool} (hwidth : ComputableTidilyInPolyTime width input encUnary) (hrow : ComputableTidilyInPolyTime row input encUnary) (hword : ComputableTidilyInPolyTime word input encBits) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.listRow (width a) (row a) (word a)) input encBits

Read a row of a computed word, including the cost of padding a short word.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsRowsWithInput {α : Type} {input : α ↪ List Bool} {count width : α → ℕ} {word : α → List Bool} (hcount : ComputableTidilyInPolyTime count input encUnary) (hwidth : ComputableTidilyInPolyTime width input encUnary) (hword : ComputableTidilyInPolyTime word input encBits) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.listRows (count a) (width a) (word a)) input (encList encBits)

Extract rows from a word with polynomial-time unary dimensions.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsXorWithInput {α : Type} {input : α ↪ List Bool} {width : α → ℕ} {words : α → List (List Bool)} (hwidth : ComputableTidilyInPolyTime width input encUnary) (hwords : ComputableTidilyInPolyTime words input (encList encBits)) : ComputableTidilyInPolyTime (fun (a : α) => Cslib.BitString.listXor (width a) (words a)) input encBits

Variable-width XOR uses runtime lookup and ordinary Boolean folds.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsWordLt {α : Type} {input : α ↪ List Bool} {x y : α → List Bool} (hx : ComputableTidilyInPolyTime x input encBits) (hy : ComputableTidilyInPolyTime y input encBits) : ComputableTidilyInPolyTime (fun (c : α) => Cslib.BitString.wordLt (x c) (y c)) input encBool

Lexicographic comparison of equal-length words is polynomial-time.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsBinaryValue : ComputableTidilyInPolyTime Cslib.BitString.binaryValue encBits encNat

Decode arbitrary most-significant-first bit words to binary naturals.

Plain polynomial-time automation

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsAnyWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {test : α → Bool → Bool} (hlist : ComputableInPolyTime list input encBits) (htest : ComputableInPolyTime (fun (p : α × Bool) => test p.1 p.2) (encPair input encBool) encBool) : ComputableInPolyTime (fun (a : α) => (list a).any (test a)) input encBool

Test whether any bit satisfies a captured predicate.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsPadWord {α : Type} {input : α ↪ List Bool} {bound : α → ℕ} {word : α → List Bool} (hbound : ComputableInPolyTime bound input encUnary) (hword : ComputableInPolyTime word input encBits) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.padWord (bound a) (word a)) input encBits

Self-delimiting padding uses ordinary framing and unary arithmetic.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsReplicate (bit : Bool) : ComputableInPolyTime (fun (n : ℕ) => List.replicate n bit) encUnary encBits

Repeat a fixed bit a unary number of times, including zero repetitions.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsZipWithInput (op : Bool → Bool → Bool) {α : Type} {input : α ↪ List Bool} {left right : α → List Bool} (hleft : ComputableInPolyTime left input encBits) (hright : ComputableInPolyTime right input encBits) : ComputableInPolyTime (fun (a : α) => List.zipWith op (left a) (right a)) input encBits

Apply a fixed Boolean operation pointwise to two computed raw words. The result stops at whichever word ends first; the two certificates retain their raw bit-string encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsRowWithInput {α : Type} {input : α ↪ List Bool} {width row : α → ℕ} {word : α → List Bool} (hwidth : ComputableInPolyTime width input encUnary) (hrow : ComputableInPolyTime row input encUnary) (hword : ComputableInPolyTime word input encBits) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.listRow (width a) (row a) (word a)) input encBits

Read a row of a computed word, charging padding and both computed unary indices.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsFrame {α : Type} (enc : α ↪ List Bool) : ComputableInPolyTime (fun (a : α) => MultiTapeTM.frame (enc a)) enc encBits

Frame the existing input encoding, charging every delimiter.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsBoundedBinaryValue : ComputableInPolyTime (fun (p : ℕ × List Bool) => Cslib.BitString.boundedBinaryValue p.1 p.2) (encPair encUnary encBits) encUnary

Saturating binary decoding to unary is polynomial time on arbitrary input words.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsBoundedBinaryValueWithInput {α : Type} {input : α ↪ List Bool} {cap : α → ℕ} {word : α → List Bool} (hcap : ComputableInPolyTime cap input encUnary) (hword : ComputableInPolyTime word input encBits) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.boundedBinaryValue (cap a) (word a)) input encUnary

Decode computed bits under a computed unary cap, fixing both intermediate encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_to_unary_bounded {α : Type} {input : α ↪ List Bool} {value bound : α → ℕ} (hvalue : ComputableInPolyTime value input encNat) (hbound : ComputableInPolyTime bound input encUnary) (hle : ∀ (a : α), value a ≤ bound a) : ComputableInPolyTime value input encUnary

Convert a binary value to unary under a computed unary bound.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsToList : ComputableInPolyTime (fun (l : List Bool) => l) encBits (encList encBool)

Convert a raw bit string to the framed list encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsGetElem? {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {index : α → ℕ} (hlist : ComputableInPolyTime list input encBits) (hindex : ComputableInPolyTime index input encUnary) : ComputableInPolyTime (fun (x : α) => (list x)[index x]?) input (encOption encBool)

Optional lookup in a raw bit string, fixing the representation of the returned bit.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsFlatten {α : Type} {input : α ↪ List Bool} {words : α → List (List Bool)} (hwords : ComputableInPolyTime words input (encList encBits)) : ComputableInPolyTime (fun (a : α) => (words a).flatten) input encBits

Concatenate computed raw words, fixing the intermediate list encoding before proof search.

theorem Turing.MultiTapeTM.ComputableInPolyTime.mapToBitsWithInput {α : Type} {input : α ↪ List Bool} {β : Type} {enc : β ↪ List Bool} {list : α → List β} {f : α → β → Bool} (hlist : ComputableInPolyTime list input (encList enc)) (hf : ComputableInPolyTime (fun (p : α × β) => f p.1 p.2) (encPair input enc) encBool) : ComputableInPolyTime (fun (a : α) => List.map (f a) (list a)) input encBits

Map a captured Boolean-valued function over a framed list, emitting a raw bit string.

theorem Turing.MultiTapeTM.ComputableInPolyTime.flatMapToBitsWithInput {α : Type} {input : α ↪ List Bool} {β : Type} {enc : β ↪ List Bool} {list : α → List β} {f : α → β → List Bool} (hlist : ComputableInPolyTime list input (encList enc)) (hf : ComputableInPolyTime (fun (p : α × β) => f p.1 p.2) (encPair input enc) encBits) : ComputableInPolyTime (fun (a : α) => List.flatMap (f a) (list a)) input encBits

Concatenate captured raw bit strings over a framed list. The complete intermediate words and their framing are charged before concatenation. Apply this rule explicitly: registering both raw and framed flatMap outputs makes existing enumeration proof search exceed its limit.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsLow {α : Type} {input : α ↪ List Bool} {width value : α → ℕ} (hwidth : ComputableInPolyTime width input encUnary) (hvalue : ComputableInPolyTime value input encNat) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.lowBits (width a) (value a)) input encBits

Emit a computed unary number of low-order digits of a computed binary natural. The width charges every output bit, including leading zero digits.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsMapWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {f : α → Bool → Bool} (hlist : ComputableInPolyTime list input encBits) (hf : ComputableInPolyTime (fun (p : α × Bool) => f p.1 p.2) (encPair input encBool) encBool) : ComputableInPolyTime (fun (a : α) => List.map (f a) (list a)) input encBits

Map a captured Boolean operation over a raw bit string.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsFilterWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {test : α → Bool → Bool} (hlist : ComputableInPolyTime list input encBits) (htest : ComputableInPolyTime (fun (p : α × Bool) => test p.1 p.2) (encPair input encBool) encBool) : ComputableInPolyTime (fun (a : α) => List.filter (test a) (list a)) input encBits

Filter a raw bit string with a predicate that may capture its original input.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsCountPWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {test : α → Bool → Bool} (hlist : ComputableInPolyTime list input encBits) (htest : ComputableInPolyTime (fun (p : α × Bool) => test p.1 p.2) (encPair input encBool) encBool) : ComputableInPolyTime (fun (x : α) => List.countP (test x) (list x)) input encUnary

Count predicate matches in a raw bit string, including a captured input.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsCountWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {value : α → Bool} (hlist : ComputableInPolyTime list input encBits) (hvalue : ComputableInPolyTime value input encBool) : ComputableInPolyTime (fun (x : α) => List.count (value x) (list x)) input encUnary

Count occurrences of a computed bit in a raw bit string.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsAllWithInput {α : Type} {input : α ↪ List Bool} {list : α → List Bool} {test : α → Bool → Bool} (hlist : ComputableInPolyTime list input encBits) (htest : ComputableInPolyTime (fun (p : α × Bool) => test p.1 p.2) (encPair input encBool) encBool) : ComputableInPolyTime (fun (a : α) => (list a).all (test a)) input encBool

Test whether every bit satisfies a captured predicate.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsFoldlWithInput {α : Type} {input : α ↪ List Bool} (op : Bool → Bool → Bool) {list : α → List Bool} {init : α → Bool} (hlist : ComputableInPolyTime list input encBits) (hinit : ComputableInPolyTime init input encBool) : ComputableInPolyTime (fun (a : α) => List.foldl op (init a) (list a)) input encBool

A Boolean fold has constant-sized state, so no separate state bound is needed.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsZipWith (op : Bool → Bool → Bool) : ComputableInPolyTime (fun (p : List Bool × List Bool) => List.zipWith op p.1 p.2) (encPair encBits encBits) encBits

Apply a fixed Boolean operation pointwise, stopping at the shorter word.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsStrictMajority : ComputableInPolyTime Cslib.BitString.listStrictMajority encBits encBool

Strict majority uses filtering, length, unary multiplication and comparison.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsStrictMajorityWithInput {α : Type} {input : α ↪ List Bool} {votes : α → List Bool} (hvotes : ComputableInPolyTime votes input encBits) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.listStrictMajority (votes a)) input encBool

Strict majority of computed votes fixes the intermediate raw-word encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsNonpositiveMarginWithInput {α : Type} {input : α ↪ List Bool} {votes : α → List Bool} {truth : α → Bool} (hvotes : ComputableInPolyTime votes input encBits) (htruth : ComputableInPolyTime truth input encBool) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.listNonpositiveMargin (votes a) (truth a)) input encBool

The training test is polynomial time in the vote list and its supplied label.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsSingle : ComputableInPolyTime (fun (p : ℕ × ℕ) => Cslib.BitString.listSingle p.1 p.2) (encPair encUnary encUnary) encBits

Generate one coordinate mask from its unary width and index.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsSingles : ComputableInPolyTime Cslib.BitString.listSingles encUnary (encList encBits)

Generate all coordinate masks, charging for their quadratic total size.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsXorSelected : ComputableInPolyTime (fun (p : ℕ × List Bool × List (List Bool)) => Cslib.BitString.listXorSelected p.1 p.2.1 p.2.2) (encPair encUnary (encPair encBits (encList encBits))) encBits

Sum selected rows with a shrinking selector and an accumulator that never grows.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsEnumList {α : Type} {input : α ↪ List Bool} {count : α → ℕ} (hcount : ComputableInPolyTime count input encUnary) {size : ℕ → ℕ} (hsize : Cslib.PolynomiallyBounded size) (hbudget : ∀ (a : α), 2 ^ count a * (2 * count a + 1) ≤ size (input a).length) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.enumList (count a)) input (encList encBits)

Enumerate words only when their complete encoded size is polynomially bounded. This does not claim polynomial time in the number of enumerated bits.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsRowsWithInput {α : Type} {input : α ↪ List Bool} {count width : α → ℕ} {word : α → List Bool} (hcount : ComputableInPolyTime count input encUnary) (hwidth : ComputableInPolyTime width input encUnary) (hword : ComputableInPolyTime word input encBits) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.listRows (count a) (width a) (word a)) input (encList encBits)

Extract rows from a word with polynomial-time unary dimensions.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsXorWithInput {α : Type} {input : α ↪ List Bool} {width : α → ℕ} {words : α → List (List Bool)} (hwidth : ComputableInPolyTime width input encUnary) (hwords : ComputableInPolyTime words input (encList encBits)) : ComputableInPolyTime (fun (a : α) => Cslib.BitString.listXor (width a) (words a)) input encBits

Variable-width XOR uses runtime lookup and ordinary Boolean folds.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsWordLt {α : Type} {input : α ↪ List Bool} {x y : α → List Bool} (hx : ComputableInPolyTime x input encBits) (hy : ComputableInPolyTime y input encBits) : ComputableInPolyTime (fun (c : α) => Cslib.BitString.wordLt (x c) (y c)) input encBool

Lexicographic comparison of equal-length words is polynomial-time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsBinaryValue : ComputableInPolyTime Cslib.BitString.binaryValue encBits encNat

Decode arbitrary most-significant-first bit words to binary naturals.