Polynomial-time string access and slicing

An FP string can be read at a polynomial-time unary position, with false past its end. Its leading run of true bits can also be measured in polynomial time, even without a false terminator. Taking or dropping a prefix of polynomial-time unary length preserves FP. These are machine-level consequences of the existing Cobham constructions, useful for encoded structures and certificates.

theorem Complexity.take_mem_FP {bits : List Bool → List Bool} {n : List Bool → ℕ} (hbits : bits ∈ FP) (hn : UnaryFn n) : (fun (z : List Bool) => List.take (n z) (bits z)) ∈ FP

Taking a prefix of polynomial-time unary length preserves polynomial time.

theorem Complexity.drop_mem_FP {bits : List Bool → List Bool} {n : List Bool → ℕ} (hbits : bits ∈ FP) (hn : UnaryFn n) : (fun (z : List Bool) => List.drop (n z) (bits z)) ∈ FP

Dropping a prefix of polynomial-time unary length preserves polynomial time.

theorem Complexity.getBit_mem_FP {bits : List Bool → List Bool} {i : List Bool → ℕ} (hbits : bits ∈ FP) (hi : UnaryFn i) : (fun (z : List Bool) => [(bits z)[i z]?.getD false]) ∈ FP

Reading one bit at a polynomial-time position is polynomial-time, with false past the end.

theorem Complexity.FPPred.getBit {bits : List Bool → List Bool} {i : List Bool → ℕ} (hbits : bits ∈ FP) (hi : UnaryFn i) : FPPred fun (z : List Bool) => (bits z)[i z]?.getD false = true

Testing a selected input bit is a polynomial-time predicate.

theorem Complexity.UnaryFn.leadingTrueLength {bits : List Bool → List Bool} (hbits : bits ∈ FP) : UnaryFn fun (z : List Bool) => (List.takeWhile id (bits z)).length

The length of the leading true run of an FP string is a polynomial-time number.