Compositional combinators for native resource certificates

These combinators assemble NativeCertificate witnesses for tuples, branches, retained-input option elimination, sum tags, and clocked binary-counter iteration while tracking arbitrary input-dependent time and space bounds. Linear postprocessing is absorbed into the producer's bounds via its output-length guarantee; no polynomiality assumption or ofPolyTime selection is used in the certificate constructors, while companion *_isPolynomial lemmas show that all combinators preserve NativeCertificate.IsPolynomial.

Main definitions

• NativeCertificate.linear, .const, .prod, .post: basic linear, literal, pair, and postprocessing combinators.
• NativeCertificate.branch, .option: selected-branch conditional and retained-input option elimination.
• NativeCertificate.fst, .snd, .some, .inl, .inr, .congr, .pull, .payload: projections, constructors, and retained-input helpers.
• NativeCertificate.maxRoundTime, .maxRoundSpace, .maxStateLength, .iterate: clocked binary-counter iteration with trajectory-maximum bounds.

Main results

• NativeCertificate.linear_isPolynomial..NativeCertificate.iterate_isPolynomial: polynomiality preservation across all certificate combinators.

References

Uses Christian Reitwiessner's native machine calculus and the parameterized option/sum resource lemmas.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.comp_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} (d : NativeCertificate g em eo) (c : NativeCertificate f ei em) (a : α) : (d.comp c).time a = c.time a + d.time (f a)

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.comp_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} (d : NativeCertificate g em eo) (c : NativeCertificate f ei em) (a : α) : (d.comp c).space a = c.space a + d.space (f a)

def Cslib.GenericRAM.NativeCertificate.linear {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (h : Turing.MultiTapeTM.ComputableTidilyInO f ei em (fun (a : α) => (ei a).length) fun (a : α) => (ei a).length) : NativeCertificate f ei em

Package a native linear-time/space implementation with its explicit input-length bound.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.linear_time {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (h : Turing.MultiTapeTM.ComputableTidilyInO f ei em (fun (a : α) => (ei a).length) fun (a : α) => (ei a).length) (a : α) : (linear h).time a = (ei a).length

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.linear_space {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (h : Turing.MultiTapeTM.ComputableTidilyInO f ei em (fun (a : α) => (ei a).length) fun (a : α) => (ei a).length) (a : α) : (linear h).space a = (ei a).length

def Cslib.GenericRAM.NativeCertificate.const {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} (b : β) : NativeCertificate (fun (x : α) => b) ei em

A fixed literal, charged by the full input length.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.const_time {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} (b : β) (a : α) : (const b).time a = (ei a).length

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.const_space {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} (b : β) (a : α) : (const b).space a = (ei a).length

def Cslib.GenericRAM.NativeCertificate.prod {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} (c : NativeCertificate f ei em) (d : NativeCertificate g ei eo) : NativeCertificate (fun (a : α) => (f a, g a)) ei (Turing.MultiTapeTM.encPair em eo)

Construct a framed pair, adding the two producer bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.prod_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} (c : NativeCertificate f ei em) (d : NativeCertificate g ei eo) (a : α) : (c.prod d).time a = c.time a + d.time a

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.prod_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} (c : NativeCertificate f ei em) (d : NativeCertificate g ei eo) (a : α) : (c.prod d).space a = c.space a + d.space a

def Cslib.GenericRAM.NativeCertificate.post {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} (c : NativeCertificate f ei em) (h : Turing.MultiTapeTM.ComputableTidilyInO g em eo (fun (b : β) => (em b).length) fun (b : β) => (em b).length) : NativeCertificate (g ∘ f) ei eo

Linear postprocessing is absorbed using the producer output-length guarantee.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.post_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} (c : NativeCertificate f ei em) (h : Turing.MultiTapeTM.ComputableTidilyInO g em eo (fun (b : β) => (em b).length) fun (b : β) => (em b).length) : (c.post h).time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.post_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} (c : NativeCertificate f ei em) (h : Turing.MultiTapeTM.ComputableTidilyInO g em eo (fun (b : β) => (em b).length) fun (b : β) => (em b).length) : (c.post h).space = c.space

def Cslib.GenericRAM.NativeCertificate.branch {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {condition : α → Bool} {f g : α → β} (test : NativeCertificate condition ei Turing.MultiTapeTM.encBool) (yes : NativeCertificate f ei em) (no : NativeCertificate g ei em) : NativeCertificate (fun (a : α) => if condition a = true then f a else g a) ei em

Charge the Boolean test and only the selected branch.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.branch_time {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {condition : α → Bool} {f g : α → β} (test : NativeCertificate condition ei Turing.MultiTapeTM.encBool) (yes : NativeCertificate f ei em) (no : NativeCertificate g ei em) (a : α) : (test.branch yes no).time a = test.time a + if condition a = true then yes.time a else no.time a

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.branch_space {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {condition : α → Bool} {f g : α → β} (test : NativeCertificate condition ei Turing.MultiTapeTM.encBool) (yes : NativeCertificate f ei em) (no : NativeCertificate g ei em) (a : α) : (test.branch yes no).space a = test.space a + if condition a = true then yes.space a else no.space a

def Cslib.GenericRAM.NativeCertificate.option {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α × β → γ} (c : NativeCertificate value ei (Turing.MultiTapeTM.encOption em)) (no : NativeCertificate fallback ei eo) (yes : NativeCertificate body (Turing.MultiTapeTM.encPair ei em) eo) : NativeCertificate (fun (a : α) => (value a).elim (fallback a) fun (b : β) => body (a, b)) ei eo

Retain the original input across option elimination; charge duplication and selected branch.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.option_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α × β → γ} (c : NativeCertificate value ei (Turing.MultiTapeTM.encOption em)) (no : NativeCertificate fallback ei eo) (yes : NativeCertificate body (Turing.MultiTapeTM.encPair ei em) eo) (a : α) : (c.option no yes).time a = 2 * c.time a + (ei a).length + (value a).elim (no.time a) fun (b : β) => yes.time (a, b)

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.option_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α × β → γ} (c : NativeCertificate value ei (Turing.MultiTapeTM.encOption em)) (no : NativeCertificate fallback ei eo) (yes : NativeCertificate body (Turing.MultiTapeTM.encPair ei em) eo) (a : α) : (c.option no yes).space a = 2 * c.space a + (ei a).length + (value a).elim (no.space a) fun (b : β) => yes.space (a, b)

def Cslib.GenericRAM.NativeCertificate.fst {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair em eo)) : NativeCertificate (fun (a : α) => (f a).1) ei em

Project the first field, absorbing linear work in the producer bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.fst_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair em eo)) : c.fst.time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.fst_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair em eo)) : c.fst.space = c.space

def Cslib.GenericRAM.NativeCertificate.snd {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair em eo)) : NativeCertificate (fun (a : α) => (f a).2) ei eo

Project the second field, absorbing linear work in the producer bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.snd_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair em eo)) : c.snd.time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.snd_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair em eo)) : c.snd.space = c.space

def Cslib.GenericRAM.NativeCertificate.some {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) : NativeCertificate (fun (a : α) => Option.some (f a)) ei (Turing.MultiTapeTM.encOption em)

Add an option tag, absorbing linear work in the producer bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.some_time {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) : c.some.time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.some_space {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) : c.some.space = c.space

def Cslib.GenericRAM.NativeCertificate.inl {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) (right : γ ↪ List Bool) : NativeCertificate (fun (a : α) => Sum.inl (f a)) ei (Turing.MultiTapeTM.encSum em right)

Add a left sum tag, absorbing linear work in the producer bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.inl_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) (right : γ ↪ List Bool) : (c.inl right).time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.inl_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) (right : γ ↪ List Bool) : (c.inl right).space = c.space

def Cslib.GenericRAM.NativeCertificate.inr {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (left : γ ↪ List Bool) (c : NativeCertificate f ei em) : NativeCertificate (fun (a : α) => Sum.inr (f a)) ei (Turing.MultiTapeTM.encSum left em)

Add a right sum tag, absorbing linear work in the producer bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.inr_time {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (left : γ ↪ List Bool) (c : NativeCertificate f ei em) : (inr left c).time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.inr_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (left : γ ↪ List Bool) (c : NativeCertificate f ei em) : (inr left c).space = c.space

def Cslib.GenericRAM.NativeCertificate.congr {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f g : α → β} (c : NativeCertificate f ei em) (h : ∀ (a : α), f a = g a) : NativeCertificate g ei em

Transport along pointwise equality without changing bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.congr_time {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f g : α → β} (c : NativeCertificate f ei em) (h : ∀ (a : α), f a = g a) : (c.congr h).time = c.time

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.congr_space {α β : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f g : α → β} (c : NativeCertificate f ei em) (h : ∀ (a : α), f a = g a) : (c.congr h).space = c.space

def Cslib.GenericRAM.NativeCertificate.pull {α β δ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) (other : δ ↪ List Bool) : NativeCertificate (fun (a : α × δ) => f a.1) (Turing.MultiTapeTM.encPair ei other) em

Retain a producer on the first component of an extended input.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.pull_time {α β δ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) (other : δ ↪ List Bool) (a : α × δ) : (c.pull other).time a = ((Turing.MultiTapeTM.encPair ei other) a).length + c.time a.1

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.pull_space {α β δ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei em) (other : δ ↪ List Bool) (a : α × δ) : (c.pull other).space a = ((Turing.MultiTapeTM.encPair ei other) a).length + c.space a.1

def Cslib.GenericRAM.NativeCertificate.payload {α β : Type} (input : α ↪ List Bool) (out : β ↪ List Bool) : NativeCertificate (fun (a : α × β) => a.2) (Turing.MultiTapeTM.encPair input out) out

Extract a retained-input continuation payload in linear time and space.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.payload_time {α β : Type} (input : α ↪ List Bool) (out : β ↪ List Bool) (a : α × β) : (payload input out).time a = ((Turing.MultiTapeTM.encPair input out) a).length

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.payload_space {α β : Type} (input : α ↪ List Bool) (out : β ↪ List Bool) (a : α × β) : (payload input out).space a = ((Turing.MultiTapeTM.encPair input out) a).length

Clocked iteration and polynomiality combinators for NativeCertificate

def Cslib.GenericRAM.NativeCertificate.maxRoundTime {β : Type} {eb : β ↪ List Bool} {step : β → β} (cstep : NativeCertificate step eb eb) (m : ℕ) (b : β) : ℕ

Maximum single-round time along the first m + 1 iterates from b.

def Cslib.GenericRAM.NativeCertificate.maxRoundSpace {β : Type} {eb : β ↪ List Bool} {step : β → β} (cstep : NativeCertificate step eb eb) (m : ℕ) (b : β) : ℕ

Maximum single-round space along the first m + 1 iterates from b.

def Cslib.GenericRAM.NativeCertificate.maxStateLength {β : Type} (eb : β ↪ List Bool) (step : β → β) (m : ℕ) (b : β) : ℕ

Maximum encoded state length along the first m + 1 iterates from b.

theorem Cslib.GenericRAM.NativeCertificate.le_maxRoundTime {β : Type} {eb : β ↪ List Bool} {step : β → β} (cstep : NativeCertificate step eb eb) {m j : ℕ} (hj : j ≤ m) (b : β) : cstep.time (step^[j] b) ≤ cstep.maxRoundTime m b

theorem Cslib.GenericRAM.NativeCertificate.le_maxRoundSpace {β : Type} {eb : β ↪ List Bool} {step : β → β} (cstep : NativeCertificate step eb eb) {m j : ℕ} (hj : j ≤ m) (b : β) : cstep.space (step^[j] b) ≤ cstep.maxRoundSpace m b

theorem Cslib.GenericRAM.NativeCertificate.le_maxStateLength {β : Type} (eb : β ↪ List Bool) (step : β → β) {m j : ℕ} (hj : j ≤ m) (b : β) : (eb (step^[j] b)).length ≤ maxStateLength eb step m b

theorem Cslib.GenericRAM.NativeCertificate.maxRoundTime_le {β : Type} {eb : β ↪ List Bool} {step : β → β} (cstep : NativeCertificate step eb eb) (m : ℕ) (b : β) {R : ℕ} (h : ∀ j ≤ m, cstep.time (step^[j] b) ≤ R) : cstep.maxRoundTime m b ≤ R

theorem Cslib.GenericRAM.NativeCertificate.maxRoundSpace_le {β : Type} {eb : β ↪ List Bool} {step : β → β} (cstep : NativeCertificate step eb eb) (m : ℕ) (b : β) {Q : ℕ} (h : ∀ j ≤ m, cstep.space (step^[j] b) ≤ Q) : cstep.maxRoundSpace m b ≤ Q

theorem Cslib.GenericRAM.NativeCertificate.maxStateLength_le {β : Type} (eb : β ↪ List Bool) (step : β → β) (m : ℕ) (b : β) {B : ℕ} (h : ∀ j ≤ m, (eb (step^[j] b)).length ≤ B) : maxStateLength eb step m b ≤ B

def Cslib.GenericRAM.NativeCertificate.iterate {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {n : α → ℕ} {init : α → β} {step : β → β} (cn : NativeCertificate n ei Turing.MultiTapeTM.encNat) (cinit : NativeCertificate init ei eb) (cstep : NativeCertificate step eb eb) : NativeCertificate (fun (a : α) => step^[n a] (init a)) ei eb

Iterate step for n a rounds using a binary counter, charging the trajectory maxima over 0 ≤ j ≤ n a without requiring [Inhabited β] or pre-supplied polynomial bounds.

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.iterate_time {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {n : α → ℕ} {init : α → β} {step : β → β} (cn : NativeCertificate n ei Turing.MultiTapeTM.encNat) (cinit : NativeCertificate init ei eb) (cstep : NativeCertificate step eb eb) (a : α) : (cn.iterate cinit cstep).time a = cn.time a + cinit.time a + (n a + 1) * (cstep.maxRoundTime (n a) (init a) + maxStateLength eb step (n a) (init a) + ((Turing.MultiTapeTM.encNat (n a)).length + 1) ^ 2)

@[simp]

theorem Cslib.GenericRAM.NativeCertificate.iterate_space {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {n : α → ℕ} {init : α → β} {step : β → β} (cn : NativeCertificate n ei Turing.MultiTapeTM.encNat) (cinit : NativeCertificate init ei eb) (cstep : NativeCertificate step eb eb) (a : α) : (cn.iterate cinit cstep).space a = cn.space a + cinit.space a + cstep.maxRoundSpace (n a) (init a) + maxStateLength eb step (n a) (init a) + (Turing.MultiTapeTM.encNat (n a)).length

Polynomiality preservation across certificate combinators

theorem Cslib.GenericRAM.NativeCertificate.polyBounded_pow_of_polyBounded {α : Type} {size u : α → ℕ} (hu : Turing.MultiTapeTM.PolyBounded size u) (c d : ℕ) : Turing.MultiTapeTM.PolyBounded size fun (a : α) => c * (u a + 1) ^ d

theorem Cslib.GenericRAM.NativeCertificate.linear_isPolynomial {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} (h : Turing.MultiTapeTM.ComputableTidilyInO f ei eb (fun (a : α) => (ei a).length) fun (a : α) => (ei a).length) : (linear h).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.const_isPolynomial {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} (b : β) : (const b).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.prod_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eo : γ ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} {g : α → γ} (c : NativeCertificate f ei eb) (d : NativeCertificate g ei eo) (hc : c.IsPolynomial) (hd : d.IsPolynomial) : (c.prod d).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.post_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eo : γ ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} {g : β → γ} (c : NativeCertificate f ei eb) (h : Turing.MultiTapeTM.ComputableTidilyInO g eb eo (fun (b : β) => (eb b).length) fun (b : β) => (eb b).length) (hc : c.IsPolynomial) : (c.post h).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.fst_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eo : γ ↪ List Bool} {eb : β ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair eb eo)) (hc : c.IsPolynomial) : c.fst.IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.snd_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eo : γ ↪ List Bool} {eb : β ↪ List Bool} {f : α → β × γ} (c : NativeCertificate f ei (Turing.MultiTapeTM.encPair eb eo)) (hc : c.IsPolynomial) : c.snd.IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.some_isPolynomial {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei eb) (hc : c.IsPolynomial) : c.some.IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.inl_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei eb) (right : γ ↪ List Bool) (hc : c.IsPolynomial) : (c.inl right).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.inr_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} (left : γ ↪ List Bool) (c : NativeCertificate f ei eb) (hc : c.IsPolynomial) : (inr left c).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.congr_isPolynomial {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {f g : α → β} (c : NativeCertificate f ei eb) (h : ∀ (a : α), f a = g a) (hc : c.IsPolynomial) : (c.congr h).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.pull_isPolynomial {α β δ : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {f : α → β} (c : NativeCertificate f ei eb) (other : δ ↪ List Bool) (hc : c.IsPolynomial) : (c.pull other).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.payload_isPolynomial {α β : Type} (input : α ↪ List Bool) (out : β ↪ List Bool) : (payload input out).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.branch_isPolynomial {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {condition : α → Bool} {f g : α → β} (test : NativeCertificate condition ei Turing.MultiTapeTM.encBool) (yes : NativeCertificate f ei eb) (no : NativeCertificate g ei eb) (ht : test.IsPolynomial) (hy : yes.IsPolynomial) (hn : no.IsPolynomial) : (test.branch yes no).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.option_isPolynomial {α β γ : Type} {ei : α ↪ List Bool} {eo : γ ↪ List Bool} {eb : β ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α × β → γ} (c : NativeCertificate value ei (Turing.MultiTapeTM.encOption eb)) (no : NativeCertificate fallback ei eo) (yes : NativeCertificate body (Turing.MultiTapeTM.encPair ei eb) eo) (hc : c.IsPolynomial) (hno : no.IsPolynomial) (hyes : yes.IsPolynomial) : (c.option no yes).IsPolynomial

theorem Cslib.GenericRAM.NativeCertificate.iterate_isPolynomial {α β : Type} {ei : α ↪ List Bool} {eb : β ↪ List Bool} {n : α → ℕ} {init : α → β} {step : β → β} (cn : NativeCertificate n ei Turing.MultiTapeTM.encNat) (cinit : NativeCertificate init ei eb) (cstep : NativeCertificate step eb eb) (hcn : cn.IsPolynomial) (hcinit : cinit.IsPolynomial) (hcstep : cstep.IsPolynomial) (hn : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) n) {B : α → ℕ} (hB : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) B) (hstate : ∀ (a : α), ∀ j ≤ n a, (eb (step^[j] (init a))).length ≤ B a) : (cn.iterate cinit cstep).IsPolynomial

Clocked iteration preserves polynomiality when the step count and reachable state lengths are polynomially bounded in the encoded input length.