Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

A fixed RAM program for exact small-target search

Lax263307.NativeExhaustive · concepts/Lax263307/NativeExhaustive.lean · lax-263307

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 finite RAM program enumerates the size-k vertex sets in the same order as the exact branch of the recursive algorithm and returns its first independent set, or reports that no candidate succeeds. The time and sufficient word width are bounded by c(n+k+2)^2(n+1)^k, uniformly for every larger word width.

    Concept map
    6 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 Lax263307.ExhaustiveTargets
    2import Lax263307.WeightedIndependentSet
    3import Lax808846.Ram
    4
    5/-!
    6---
    7title: A fixed RAM program for exact small-target search
    8type: theorem
    9---
    10One finite RAM program enumerates the size-k vertex sets in the same order
    11as the exact branch of the recursive algorithm and returns its first
    12independent set, or reports that no candidate succeeds. The time and
    13sufficient word width are bounded by c(n+k+2)^2(n+1)^k, uniformly for every
    14larger word width.
    15
    16# Formalization notes
    17
    18The input is n, k, the matrix length n^2, and the row-major adjacency
    19matrix. Failure is encoded as [0]; success is 1 followed by the selected
    20set's membership vector. Native Pascal-table construction and ranked subset
    21decoding avoid enumerating the whole powerset. The proof includes actual
    22matrix reads, independence tests, first-success retention, input/output,
    23compilation, and instruction and word bounds. The source subroutine also
    24operates directly on graph buffers for use by the recursive solver.
    25-/
    26
    27namespace Lax263307.NativeExhaustive
    28
    29def encodeInput {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k : ℕ) : List ℕ :=
    30 n::k::(n*n)::(List.ofFn fun u => List.ofFn fun v => if G.Adj u v then 1 else 0).flatten
    31
    32def encodeAnswer {n : ℕ} : Option (Finset (Fin n)) → List ℕ
    33 | none => [0]
    34 | some I => 1::WeightedIndependentSet.encodeOutput I
    35
    36axiom exists_program : ∃ p : Lax808846.Ram.Program, ∃ c : ℕ, 0<c ∧
    37 ∀ (n k : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    38 ∀ width : ℕ,c*(n+k+2)^2*(n+1)^k≤width →
    39 ∃ t≤c*(n+k+2)^2*(n+1)^k,Lax808846.Ram.RunsTo width p (encodeInput G k)
    40 (encodeAnswer (ExhaustiveTargets.findIndependentSet G k)) t
    41
    42end Lax263307.NativeExhaustive
    43
    Show Proof
    Formalization notes

    The input is n, k, the matrix length n^2, and the row-major adjacency matrix. Failure is encoded as [0]; success is 1 followed by the selected set's membership vector. Native Pascal-table construction and ranked subset decoding avoid enumerating the whole powerset. The proof includes actual matrix reads, independence tests, first-success retention, input/output, compilation, and instruction and word bounds. The source subroutine also operates directly on graph buffers for use by the recursive solver.

    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…