Lax Lean Archive

Linear-Time Construction on the Word RAM

Lax920634.LinearConstruction · concepts/Lax920634/LinearConstruction.lean · lax-920634

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.

    Natural Language Statement

    Theorem

    One fixed deterministic word-RAM program constructs the specified subcubic graphs in linear time in their output order. The program receives a requested order as one word and outputs the complete word-sized matching table.

    There are constants ct,cw>0c_t,c_w>0 such that its actual instruction count is at most ct(N+1)c_t(N+1) at every word width satisfying cw(N+1)≤2wc_w(N+1)\le2^w, where NN is the selected graph's order. Consequently O(log⁡(N+1))O(\log(N+1))-bit words suffice. The program and constants are chosen before the request and the word width. The proof supplies ct=25381c_t=25381 and cw=128c_w=128.

    Concept map
    9 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax920634.WordEncoding
    2import Lax808846.RamComputes
    3
    4/-!
    5---
    6title: Linear-Time Construction on the Word RAM
    7type: theorem
    8---
    9One fixed deterministic word-RAM program constructs the specified subcubic
    10graphs in linear time in their output order. The program receives a requested
    11order as one word and outputs the complete word-sized matching table.
    12
    13There are constants ct,cw>0c_t,c_w>0 such that its actual instruction count is at
    14most ct(N+1)c_t(N+1) at every word width satisfying cw(N+1)≤2wc_w(N+1)\le2^w, where NN is
    15the selected graph's order. Consequently O(log⁡(N+1))O(\log(N+1))-bit words suffice.
    16The program and constants are chosen before the request and the word width.
    17The proof supplies ct=25381c_t=25381 and cw=128c_w=128.
    18
    19# Proof strategy
    20
    21Materialize the fixed seed and build the rotation tables from the bottom up.
    22Each new row uses a constant number of lookups in the seed and preceding table.
    23Geometric growth bounds the total number of rows by a constant multiple of
    24NN. A verified compiler transfers this bound to actual registered RAM
    25instructions, including initialization and output. The fixed seed and
    26level-zero table are program literals determined by the specified seed scan;
    27writing these literals into RAM is charged. No data depending on the request
    28or word width are built into the program.
    29-/
    30
    31namespace Lax920634.LinearConstruction
    32
    33open ZigZagConstruction Lax808846.Ram
    34open GraphEncoding (selectedLevel)
    35open WordEncoding (construct)
    36
    37/-- A uniform deterministic RAM constructs the precise family in linear output time. -/
    38axiom linear_time : ∃ (program : Program) (timeConstant wordConstant : ℕ),
    39 0 < timeConstant ∧ 0 < wordConstant ∧
    40 ∀ (n w : ℕ),
    41 wordConstant * (order (selectedLevel n) + 1) ≤ 2 ^ w →
    42 ∃ t ≤ timeConstant * (order (selectedLevel n) + 1),
    43 RunsTo w program [n] (construct n) t
    44
    45end Lax920634.LinearConstruction
    46
    Show Proof

    Proof strategy

    Materialize the fixed seed and build the rotation tables from the bottom up. Each new row uses a constant number of lookups in the seed and preceding table. Geometric growth bounds the total number of rows by a constant multiple of NN. A verified compiler transfers this bound to actual registered RAM instructions, including initialization and output. The fixed seed and level-zero table are program literals determined by the specified seed scan; writing these literals into RAM is charged. No data depending on the request or word width are built into the program.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…