Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax58.BitPolynomialTime

Polynomial time with polynomial word length

concepts/Lax58/BitPolynomialTime.lean · lax-58

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    This variant bounds both running time and sufficient word length by polynomials in a specified input size, normally its binary size. Input still uses the distinguished structural arena. A bound of qq bits means capacity 2q2 ^ q, so this is an instance of the existing RAM resource predicate, not a different machine model.

    The arena must fit already at the stated sufficient width. This prevents oversized payloads from making the guarantee vacuous. The one program works at every larger width, and must produce the exact encoded output.

    In contrast, RamComplexityExample.PolynomialTimeRamComplexityExample.PolynomialTime measures time in sequence length and permits only a constant-times-input-magnitude capacity threshold. Polynomially many sufficient bits can accommodate exponentially large natural-number outputs; that linear capacity convention cannot in general.

    Lean source view on GitHub

    1import Lax58.RamComplexity
    2import Mathlib.Algebra.Polynomial.Eval.Defs
    3
    4/-!
    5---
    6title: Polynomial time with polynomial word length
    7type: definition
    8---
    9
    10This variant bounds both running time and sufficient word length by
    11polynomials in a specified input size, normally its binary size. Input still
    12uses the distinguished structural arena. A bound of `q` bits means capacity
    13`2 ^ q`, so this is an instance of the existing RAM resource predicate, not
    14a different machine model.
    15
    16The arena must fit already at the stated sufficient width. This prevents
    17oversized payloads from making the guarantee vacuous. The one program works
    18at every larger width, and must produce the exact encoded output.
    19
    20In contrast, `RamComplexityExample.PolynomialTime` measures time in sequence
    21length and permits only a constant-times-input-magnitude capacity threshold.
    22Polynomially many sufficient bits can accommodate exponentially large
    23natural-number outputs; that linear capacity convention cannot in general.
    24-/
    25
    26namespace Lax58.BitPolynomialTime
    27
    28open Lax58.StructuralPresentation Lax58.WordArena Lax58.RamComplexity
    29
    30universe u v
    31
    32/-- Polynomial instruction count and polynomial sufficient word length,
    33relative to a presentation, output encoding, and input-size measure.
    34Both polynomials are chosen once, independently of the input and runtime
    35word width. The input remains a root word followed by its structural arena. -/
    36def BitPolynomialTimeUsing {α : Type u} {β : Type v}
    37 (input : Presentation α) (output : β → List Nat)
    38 (inputSize : α → Nat) (f : α → β) : Prop :=
    39 ∃ wordBits time : Polynomial Nat,
    40 (∀ x, (input.toRaw x).PayloadsFitInWord (wordBits.eval (inputSize x)) ∧
    41 3 * (input.toRaw x).nodes ≤ 2 ^ wordBits.eval (inputSize x)) ∧
    42 RamComputableWithinUsing input output f
    43 (fun x => time.eval (inputSize x))
    44 (fun x => 2 ^ wordBits.eval (inputSize x))
    45
    46end Lax58.BitPolynomialTime
    47

    Builds on

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…