Plain native certificates with independent resource bounds

A certificate records arbitrary input-dependent time/workspace bounds and a proposition asserting that a finite machine realizes its function within them, including the encoded-output charge. The machine is existential in that proposition, not stored as data. Exact constructors charge output using its actual clock, so their workspace allowance is exactly s + t. Runtime model programs are defined separately.

Main definitions

• NativeCertificate: one implementation with independent, charged resource bounds.

Main results

• Cslib.GenericRAM.exists_mono_poly, Cslib.GenericRAM.exists_mono_poly_cert: monotone polynomial bounds extracted from PolyBounded and ComputableInPolyTime.

structure Cslib.GenericRAM.NativeCertificate {α β : Type} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) : Type

An actual native implementation, with bounds also charging its encoded output length.

• time : α → ℕ

  Input-dependent time bound, up to a constant factor and additive constant.

• space : α → ℕ

  Input-dependent work space and encoded output bound, up to constants.

• computes : Turing.MultiTapeTM.ComputableInO f encIn encOut self.time self.space

  One finite machine implements the function on every encoded input.

theorem Cslib.GenericRAM.NativeCertificate.isComputable {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (c : NativeCertificate f encIn encMid) : Turing.MultiTapeTM.IsComputable f encIn encMid

Forgetting resource bounds retains native computability.

def Cslib.GenericRAM.NativeCertificate.IsPolynomial {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (c : NativeCertificate f encIn encMid) : Prop

Polynomiality is a separate property of both bounds in the encoded input length.

theorem Cslib.GenericRAM.NativeCertificate.polyTime {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (c : NativeCertificate f encIn encMid) (h : c.IsPolynomial) : Turing.MultiTapeTM.ComputableInPolyTime f encIn encMid

Derive the existing native polynomial-time predicate, for use by its compositional calculus.

def Cslib.GenericRAM.NativeCertificate.comp {α β γ : Type} {f : α → β} {g : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} (d : NativeCertificate g encMid encOut) (c : NativeCertificate f encIn encMid) : NativeCertificate (g ∘ f) encIn encOut

Compose implementations, charging the second bound at the first result.

theorem Cslib.GenericRAM.NativeCertificate.comp_isPolynomial {α β γ : Type} {f : α → β} {g : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} (d : NativeCertificate g encMid encOut) (c : NativeCertificate f encIn encMid) (hd : d.IsPolynomial) (hc : c.IsPolynomial) : (d.comp c).IsPolynomial

Composing polynomial certificates preserves polynomiality in the original input encoding.

def Cslib.GenericRAM.NativeCertificate.ofTimeAndSpace {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {t s : α → ℕ} (h : Turing.MultiTapeTM.ComputableInTimeAndSpace f encIn encMid t s) : NativeCertificate f encIn encMid

Package exact native bounds, including the running time in the space allowance to charge encoded output length. No polynomial hypothesis is needed.

theorem Cslib.GenericRAM.NativeCertificate.nonempty_iff_isComputable {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} : Nonempty (NativeCertificate f encIn encMid) ↔ Turing.MultiTapeTM.IsComputable f encIn encMid

Arbitrary-bound certificates impose exactly native computability, not an efficiency assumption. Polynomial resource bounds remain a separate property.

theorem Cslib.GenericRAM.NativeCertificate.exists_polynomial {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : Turing.MultiTapeTM.ComputableInPolyTime f encIn encMid) : ∃ (c : NativeCertificate f encIn encMid), c.IsPolynomial

Every native polynomial-time proof supplies a certificate with polynomial bounds. The space bound includes the running time so that it also bounds the emitted output.

noncomputable def Cslib.GenericRAM.NativeCertificate.ofPolyTime {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : Turing.MultiTapeTM.ComputableInPolyTime f encIn encMid) : NativeCertificate f encIn encMid

Select resource bounds from an existing polynomial-time implementation proof.

theorem Cslib.GenericRAM.NativeCertificate.ofPolyTime_isPolynomial {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : Turing.MultiTapeTM.ComputableInPolyTime f encIn encMid) : (ofPolyTime h).IsPolynomial

Bounds selected by ofPolyTime are polynomial in the encoded input length.

theorem Cslib.GenericRAM.exists_mono_poly {α : Type} {size u : α → ℕ} (hu : Turing.MultiTapeTM.PolyBounded size u) : ∃ (p : ℕ → ℕ), PolynomiallyBounded p ∧ Monotone p ∧ ∀ (a : α), u a ≤ p (size a)

Extract an explicit monotone polynomial bound from a PolyBounded witness.

theorem Cslib.GenericRAM.exists_mono_poly_cert {α β : Type} {f : α → β} {ei : α ↪ List Bool} {eo : β ↪ List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f ei eo) : ∃ (p : ℕ → ℕ), PolynomiallyBounded p ∧ Monotone p ∧ ∀ (a : α), (NativeCertificate.ofPolyTime hf).time a ≤ p (ei a).length ∧ (NativeCertificate.ofPolyTime hf).space a ≤ p (ei a).length

Extract a single monotone polynomial bounding both time and workspace of NativeCertificate.ofPolyTime hf.