Lax Lean Archive

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

Lax307052.SearchBounds

Quadratic space for the recursion stack

concepts/Lax307052/SearchBounds.lean · lax-307052

proven

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

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lemma

    The number of recursion frames is logarithmic in the configuration count. Multiplying this depth by the space for configurations and counters gives O(s2)O(s^2) when ss bounds the input logarithm.

    Lean source view on GitHub

    1import Lax307052.ConfigurationGraph
    2import Lax434930.SpaceBounds
    3
    4/-!
    5---
    6title: Quadratic space for the recursion stack
    7type: lemma
    8---
    9The number of recursion frames is logarithmic in the configuration count.
    10Multiplying this depth by the space for configurations and counters gives
    11O(s2)O(s^2) when ss bounds the input logarithm.
    12-/
    13
    14namespace Lax307052.SearchBounds
    15
    16open Lax434930.SpaceMachines Lax434930.SpaceBounds BoundedConfigurations
    17
    18def stackSpace (M : Machine) (n s : ℕ) : ℕ :=
    19 (Nat.clog 2 (Fintype.card (Config M n s)) + 1) * (s + logSpace n + 1)
    20
    21axiom quadratic (M : Machine) :
    22 ∃ c : ℕ, 0 < c ∧ ∀ n s, logSpace n ≤ s → stackSpace M n s ≤ c * s ^ 2
    23
    24end Lax307052.SearchBounds
    25
    Show Proof

    Builds on

    Used by

    none

    From Mathlib

    none

    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…