Quantitative computability rules

fun_prop (disch := lia) composes degree certificates (ComputableInDegree and ComputableTidilyInDegree) without replacing output-size bounds by runtime bounds. Computation premises determine the intermediate encodings and degrees before the arithmetic obligations compare the resulting degrees with the requested ones. The same fun_prop interface recognizes ordinary finite-state bit folds with linear time and constant work space. For nested projections with inferred degrees, disch := first | apply le_refl | lia first instantiates a missing degree with the derived bound, then checks arithmetic inequalities. Framed-list and option rules infer the payload encoding from the representation explicitly.

Main results

• Turing.MultiTapeTM.ComputableInDegree.foldl', Turing.MultiTapeTM.ComputableInDegree.foldlWith: plain left folds with degree bounds.
• Turing.MultiTapeTM.ComputableInDegree.natSucc: binary successor with degrees one.
• Turing.MultiTapeTM.computableInDegree_add, Turing.MultiTapeTM.computableInDegree_mul: plain binary addition (quadratic) and multiplication (cubic).
• Turing.MultiTapeTM.ComputableInO.comp_enc: reuse a bit-word computation on encoded instances, with bounds evaluated on their encodings.
• Turing.MultiTapeTM.ComputableInO.lengthUnary: compute bit-word length in unary within linear time and space.
• Turing.MultiTapeTM.ComputableInO.unary_two_pow: compute 2 ^ n from unary n within time O((n + 1) * 2 ^ n) and space O(2 ^ n).
• Turing.MultiTapeTM.ComputableInDegree.comp_le, .prod_le, .ite_le: plain composition, pairing, and branching at requested degrees, retaining output-size bounds.
• Turing.MultiTapeTM.ComputableInDegree.bitsReverse, Turing.MultiTapeTM.ComputableInDegree.bitsDropLast, Turing.MultiTapeTM.ComputableInDegree.bitsGetLast?ToList, Turing.MultiTapeTM.ComputableInDegree.bitsGetLast?, Turing.MultiTapeTM.ComputableInDegree.optionBoolToList, Turing.MultiTapeTM.ComputableInDegree.bitsAppend, Turing.MultiTapeTM.ComputableInDegree.unaryAdd: plain degree rules for raw bit-list reversal, prefix, last-bit extraction, concatenation, and unary addition (alongside tidy counterparts).

References

Uses Christian Reitwiessner's degree calculus and streaming backend; see the source markers in Degree.lean and CslibFrontier/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean.

theorem Turing.MultiTapeTM.ComputableInDegree.fst' {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {d e : ℕ} {f : α → β₁ × β₂} (h : ComputableInDegree f encIn (encPair enc₁ enc₂) d e) : ComputableInDegree (fun (x : α) => (f x).1) encIn enc₁ (max d e) e

The first component of a pair computed with given degrees.

theorem Turing.MultiTapeTM.ComputableInDegree.snd' {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {d e : ℕ} {f : α → β₁ × β₂} (h : ComputableInDegree f encIn (encPair enc₁ enc₂) d e) : ComputableInDegree (fun (x : α) => (f x).2) encIn enc₂ (max d e) e

The second component of a pair computed with given degrees.

theorem Turing.MultiTapeTM.ComputableInDegree.headD {β : Type u_1} {enc₁ : β ↪ List Bool} {enc : List β ↪ List Bool} [ListEncoding enc₁ enc] (d : β) : ComputableInDegree (fun (l : List β) => l.headD d) enc enc₁ 1 1

List.headD on any list encoding.

theorem Turing.MultiTapeTM.ComputableInDegree.tail {β : Type u_1} {enc₁ : β ↪ List Bool} {enc : List β ↪ List Bool} [ListEncoding enc₁ enc] : ComputableInDegree List.tail enc enc 1 1

List.tail on any list encoding.

theorem Turing.MultiTapeTM.ComputableInDegree.isEmpty {β : Type u_1} {enc₁ : β ↪ List Bool} {enc : List β ↪ List Bool} [ListEncoding enc₁ enc] : ComputableInDegree List.isEmpty enc encBool 1 1

List.isEmpty on any list encoding.

theorem Turing.MultiTapeTM.ComputableInDegree.foldl' {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [hS : SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} {dL eL dI eI dS eS b : ℕ} (hlist : ComputableInDegree list encIn encL dL eL) (hinit : ComputableInDegree init encIn encB dI eI) (hstep : ComputableInDegree (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB dS eS) {B : γ → ℕ} (hB : DegreeBounded (fun (x : γ) => (encIn x).length) B b) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableInDegree (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB (max (max dL dI) (eL + max 1 dS * max b eL)) b

Left folds with bounds of given degrees, compiled directly from plain degree certificates.

theorem Turing.MultiTapeTM.ComputableInDegree.foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} {dP eP dL eL dI eI dS eS b : ℕ} (hpar : ComputableInDegree par encIn encP dP eP) (hlist : ComputableInDegree list encIn encL dL eL) (hinit : ComputableInDegree init encIn encB dI eI) (hstep : ComputableInDegree (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB dS eS) {B : γ → ℕ} (hB : DegreeBounded (fun (x : γ) => (encIn x).length) B b) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableInDegree (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB (max (max dL (max dP dI)) (eL + max 1 dS * max (max eP b) eL)) b

Left folds with a parameter, keeping par x in the fold state.

theorem Turing.MultiTapeTM.ComputableInDegree.cons {α : Type} (enc : α ↪ List Bool) : ComputableInDegree (fun (p : α × List α) => p.1 :: p.2) (encPair enc (encList enc)) (encList enc) 1 1

Adding an element in front of a framed list: the identity on encoded words.

theorem Turing.MultiTapeTM.ComputableInDegree.snoc {α : Type} (enc : α ↪ List Bool) : ComputableInDegree (fun (p : List α × α) => p.1 ++ [p.2]) (encPair (encList enc) enc) (encList enc) 1 1

Adding an element at the end of a framed list.

theorem Turing.MultiTapeTM.ComputableInDegree.listAppend {α : Type} (enc : α ↪ List Bool) : ComputableInDegree (fun (p : List α × List α) => p.1 ++ p.2) (encPair (encList enc) (encList enc)) (encList enc) 1 1

Concatenating two framed lists.

theorem Turing.MultiTapeTM.ComputableInDegree.unary_sub : ComputableInDegree (fun (p : ℕ × ℕ) => p.1 - p.2) (encPair encUnary encUnary) encUnary 2 1

Truncated subtraction of unary numbers.

theorem Turing.MultiTapeTM.ComputableInDegree.unary_min : ComputableInDegree (fun (p : ℕ × ℕ) => min p.1 p.2) (encPair encUnary encUnary) encUnary 2 1

The minimum of unary numbers.

theorem Turing.MultiTapeTM.ComputableInDegree.int_succ : ComputableInDegree (fun (x : ℤ) => x + 1) encIntUnary encIntUnary 1 1

Adding one on unary-magnitude signed integers.

theorem Turing.MultiTapeTM.ComputableInDegree.int_pred : ComputableInDegree (fun (x : ℤ) => x - 1) encIntUnary encIntUnary 1 1

Subtracting one on unary-magnitude signed integers.

theorem Turing.MultiTapeTM.ComputableInDegree.eqWords : ComputableInDegree (fun (p : List Bool × List Bool) => decide (p.1 = p.2)) (encPair encBits encBits) encBool 2 0

Equality of bit words in quadratic time/space and constant output length.

theorem Turing.MultiTapeTM.ComputableInDegree.eq {α : Type} [DecidableEq α] (enc : α ↪ List Bool) : ComputableInDegree (fun (p : α × α) => decide (p.1 = p.2)) (encPair enc enc) encBool 2 0

Equality for any encoding in quadratic time/space and constant output length.

theorem Turing.MultiTapeTM.computableInDegree_add : ComputableInDegree (fun (p : ℕ × ℕ) => p.1 + p.2) (encPair encNat encNat) encNat 2 1

Addition is computable in quadratic time and space, with linear output length, in the binary encoding.

theorem Turing.MultiTapeTM.computableInDegree_mul : ComputableInDegree (fun (p : ℕ × ℕ) => p.1 * p.2) (encPair encNat encNat) encNat 3 1

Multiplication is computable in cubic time and space, with linear output length, in the binary encoding.

theorem Turing.MultiTapeTM.ComputableInDegree.listTail {α : Type u_1} (enc : α ↪ List Bool) : ComputableInDegree List.tail (encList enc) (encList enc) 1 1

The result encoding fixes the element encoding, without reversing ListEncoding inference.

theorem Turing.MultiTapeTM.ComputableInDegree.listHeadD {α : Type u_1} (enc : α ↪ List Bool) (fallback : α) : ComputableInDegree (fun (l : List α) => l.headD fallback) (encList enc) enc 1 1

The framed input list determines the encoding of its head, including a fixed fallback.

theorem Turing.MultiTapeTM.ComputableInDegree.listIsEmpty {α : Type u_1} (enc : α ↪ List Bool) : ComputableInDegree List.isEmpty (encList enc) encBool 1 1

Testing a framed list for emptiness.

theorem Turing.MultiTapeTM.ComputableInDegree.optionGetD {α : Type u_1} (enc : α ↪ List Bool) (fallback : α) : ComputableInDegree (fun (o : Option α) => o.getD fallback) (encOption enc) enc 1 1

The option encoding determines the encoding used for the payload and fallback.

theorem Turing.MultiTapeTM.ComputableInDegree.id' {α : Type u_1} {enc : α ↪ List Bool} : ComputableInDegree (fun (x : α) => x) enc enc 1 1

Copy an encoded value. This identity rule also lets fun_prop retain a shared let binding.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsReverse : ComputableInDegree List.reverse encBits encBits 1 1

Reverse a raw bit list in linear time and linear output size.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsDropLast : ComputableInDegree List.dropLast encBits encBits 1 1

Drop the last bit of a raw bit list in linear time and linear output size.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsGetLast?ToList : ComputableInDegree (fun (l : List Bool) => l.getLast?.toList) encBits encBits 1 0

Extract the last bit of a raw bit list as a 0-or-1-element list in linear time and constant output size.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsGetLast? : ComputableInDegree List.getLast? encBits (encOption encBool) 1 0

Extract the last bit of a raw bit list as an Option Bool in linear time and constant output size.

theorem Turing.MultiTapeTM.ComputableInDegree.optionBoolToList : ComputableInDegree Option.toList (encOption encBool) encBits 1 1

Convert an Option Bool to a 0-or-1-element bit list in linear time and linear output size.

theorem Turing.MultiTapeTM.ComputableInDegree.bitsAppend {α : Type u_1} {encIn : α ↪ List Bool} {f g : α → List Bool} {df ef dg eg d e : ℕ} (hf : ComputableInDegree f encIn encBits df ef) (hg : ComputableInDegree g encIn encBits dg eg) (hd : max df dg ≤ d) (he : max ef eg ≤ e) : ComputableInDegree (fun (x : α) => f x ++ g x) encIn encBits d e

Concatenate two raw bit lists while preserving their time and output degrees independently.

theorem Turing.MultiTapeTM.ComputableInDegree.unaryAdd {α : Type u_1} {encIn : α ↪ List Bool} {f g : α → ℕ} {df ef dg eg d e : ℕ} (hf : ComputableInDegree f encIn encUnary df ef) (hg : ComputableInDegree g encIn encUnary dg eg) (hd : max df dg ≤ d) (he : max ef eg ≤ e) : ComputableInDegree (fun (x : α) => f x + g x) encIn encUnary d e

Add two unary natural numbers while preserving their time and output degrees independently.

theorem Turing.MultiTapeTM.ComputableInDegree.comp_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} {df ef dg eg d e : ℕ} (hg : ComputableInDegree g encIn encMid dg eg) (hf : ComputableInDegree f encMid encOut df ef) (hd : max dg (eg * df) ≤ d) (he : eg * ef ≤ e) : ComputableInDegree (fun (x : α) => f (g x)) encIn encOut d e

Compose using the intermediate output size. The computation premises determine the degrees before arithmetic compares them with the requested bound.

theorem Turing.MultiTapeTM.ComputableInDegree.prod_le {α β γ : Type u} {encIn : α ↪ List Bool} {encF : β ↪ List Bool} {encG : γ ↪ List Bool} {f : α → β} {g : α → γ} {df ef dg eg d e : ℕ} (hf : ComputableInDegree f encIn encF df ef) (hg : ComputableInDegree g encIn encG dg eg) (hd : max df dg ≤ d) (he : max ef eg ≤ e) : ComputableInDegree (fun (x : α) => (f x, g x)) encIn (encPair encF encG) d e

Pair two results while preserving their output degrees independently of computation time.

theorem Turing.MultiTapeTM.ComputableInDegree.ite_le {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {condition : α → Bool} {f g : α → β} {dc ec df ef dg eg d e : ℕ} (hc : ComputableInDegree condition encIn encBool dc ec) (hf : ComputableInDegree f encIn encOut df ef) (hg : ComputableInDegree g encIn encOut dg eg) (hd : max dc (max df dg) ≤ d) (he : max ef eg ≤ e) : ComputableInDegree (fun (x : α) => if condition x = true then f x else g x) encIn encOut d e

Branching on a computed Boolean, retaining each branch's output degree.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.listTail {α : Type u_1} (enc : α ↪ List Bool) : ComputableTidilyInDegree List.tail (encList enc) (encList enc) 1 1

The result encoding fixes the element encoding, without reversing ListEncoding inference.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.listHeadD {α : Type u_1} (enc : α ↪ List Bool) (fallback : α) : ComputableTidilyInDegree (fun (l : List α) => l.headD fallback) (encList enc) enc 1 1

The framed input list determines the encoding of its head, including a fixed fallback.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.listIsEmpty {α : Type u_1} (enc : α ↪ List Bool) : ComputableTidilyInDegree List.isEmpty (encList enc) encBool 1 1

Testing a framed list for emptiness.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.optionGetD {α : Type u_1} (enc : α ↪ List Bool) (fallback : α) : ComputableTidilyInDegree (fun (o : Option α) => o.getD fallback) (encOption enc) enc 1 1

The option encoding determines the encoding used for the payload and fallback.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.id' {α : Type u_1} {enc : α ↪ List Bool} : ComputableTidilyInDegree (fun (x : α) => x) enc enc 1 1

Copy an encoded value. This identity rule also lets fun_prop retain a shared let binding.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.bitsReverse : ComputableTidilyInDegree List.reverse encBits encBits 1 1

Reverse a raw bit list in linear time and linear output size.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.bitsDropLast : ComputableTidilyInDegree List.dropLast encBits encBits 1 1

Drop the last bit of a raw bit list in linear time and linear output size.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.bitsGetLast?ToList : ComputableTidilyInDegree (fun (l : List Bool) => l.getLast?.toList) encBits encBits 1 0

Extract the last bit of a raw bit list as a 0-or-1-element list in linear time and constant output size.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.bitsGetLast? : ComputableTidilyInDegree List.getLast? encBits (encOption encBool) 1 0

Extract the last bit of a raw bit list as an Option Bool in linear time and constant output size.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.optionBoolToList : ComputableTidilyInDegree Option.toList (encOption encBool) encBits 1 1

Convert an Option Bool to a 0-or-1-element bit list in linear time and linear output size.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.bitsAppend {α : Type u_1} {encIn : α ↪ List Bool} {f g : α → List Bool} {df ef dg eg d e : ℕ} (hf : ComputableTidilyInDegree f encIn encBits df ef) (hg : ComputableTidilyInDegree g encIn encBits dg eg) (hd : max df dg ≤ d) (he : max ef eg ≤ e) : ComputableTidilyInDegree (fun (x : α) => f x ++ g x) encIn encBits d e

Concatenate two raw bit lists while preserving their time and output degrees independently.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.unaryAdd {α : Type u_1} {encIn : α ↪ List Bool} {f g : α → ℕ} {df ef dg eg d e : ℕ} (hf : ComputableTidilyInDegree f encIn encUnary df ef) (hg : ComputableTidilyInDegree g encIn encUnary dg eg) (hd : max df dg ≤ d) (he : max ef eg ≤ e) : ComputableTidilyInDegree (fun (x : α) => f x + g x) encIn encUnary d e

Add two unary natural numbers while preserving their time and output degrees independently.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.comp_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} {df ef dg eg d e : ℕ} (hg : ComputableTidilyInDegree g encIn encMid dg eg) (hf : ComputableTidilyInDegree f encMid encOut df ef) (hd : max dg (eg * df) ≤ d) (he : eg * ef ≤ e) : ComputableTidilyInDegree (fun (x : α) => f (g x)) encIn encOut d e

Compose using the intermediate output size. The computation premises determine the degrees before arithmetic compares them with the requested bound.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.prod_le {α β γ : Type u} {encIn : α ↪ List Bool} {encF : β ↪ List Bool} {encG : γ ↪ List Bool} {f : α → β} {g : α → γ} {df ef dg eg d e : ℕ} (hf : ComputableTidilyInDegree f encIn encF df ef) (hg : ComputableTidilyInDegree g encIn encG dg eg) (hd : max df dg ≤ d) (he : max ef eg ≤ e) : ComputableTidilyInDegree (fun (x : α) => (f x, g x)) encIn (encPair encF encG) d e

Pair two results while preserving their output degrees independently of computation time.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.ite_le {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {condition : α → Bool} {f g : α → β} {dc ec df ef dg eg d e : ℕ} (hc : ComputableTidilyInDegree condition encIn encBool dc ec) (hf : ComputableTidilyInDegree f encIn encOut df ef) (hg : ComputableTidilyInDegree g encIn encOut dg eg) (hd : max dc (max df dg) ≤ d) (he : max ef eg ≤ e) : ComputableTidilyInDegree (fun (x : α) => if condition x = true then f x else g x) encIn encOut d e

Branching on a computed Boolean, retaining each branch's output degree.

theorem Turing.MultiTapeTM.ComputableInO.comp_enc {α β : Type} {encOut : β ↪ List Bool} {f : List Bool → β} {T S : List Bool → ℕ} (h : ComputableInO f encBits encOut T S) (enc : α ↪ List Bool) : ComputableInO (fun (a : α) => f (enc a)) enc encOut (fun (a : α) => T (enc a)) fun (a : α) => S (enc a)

A function of bit words computed within given bounds is computed by the same machine on encoded instances.

theorem Turing.MultiTapeTM.ComputableInO.lengthUnary : ComputableInO (fun (l : List Bool) => l.length) encBits encUnary (fun (l : List Bool) => l.length) fun (l : List Bool) => l.length

The length of a bit word in unary, within linear time and space, by the streaming machine of Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.length_bits.

theorem Turing.MultiTapeTM.ComputableInO.unary_two_pow : ComputableInO (fun (n : ℕ) => 2 ^ n) encUnary encUnary (fun (n : ℕ) => (n + 1) * 2 ^ n) fun (n : ℕ) => 2 ^ n

2 ^ n in unary, by doubling n times, within time O((n + 1) * 2 ^ n) and space O(2 ^ n).