Lax Lean Archive

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

A fixed RAM program for the moment-coordinate catalog

Lax263307.NativeCatalog · concepts/Lax263307/NativeCatalog.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

    A single finite RAM program enumerates the subsets of size at most r+2 in the exact order used by the moment relaxation. Each subset occupies one n-bit word. The program stores only the N catalog entries and uses time and sufficient word width at most c(n+r+N+2)^3, uniformly for every larger word width.

    Concept map
    12 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.CoordinateCatalog
    2import Lax808846.Ram
    3import Mathlib.Combinatorics.Colex
    4
    5/-!
    6---
    7title: A fixed RAM program for the moment-coordinate catalog
    8type: theorem
    9---
    10A single finite RAM program enumerates the subsets of size at most r+2
    11in the exact order used by the moment relaxation. Each subset occupies
    12one n-bit word. The program stores only the N catalog entries and uses
    13time and sufficient word width at most c(n+r+N+2)^3, uniformly for every
    14larger word width.
    15
    16# Formalization notes
    17
    18Input is [n,r]. Output is the list of subset masks in CoordinateCatalog
    19order. The construction uses native Pascal tables, ranked-subset decoding,
    20bit packing, and ordered buffer appends. Distinct cardinality blocks are
    21disjoint, so the catalog's duplicate-removal operation leaves this order
    22unchanged. Mask words represent subsets; their values are not used as
    23addresses for an array of size 2^n.
    24-/
    25
    26namespace Lax263307.NativeCatalog
    27
    28def subsetMask {n : ℕ} (I : Finset (Fin n)) : ℕ :=
    29 Finset.equivBitIndices.symm (I.image Fin.val)
    30
    31def words (n r : ℕ) : List ℕ :=
    32 (CoordinateCatalog.catalog n r).map (fun A => subsetMask A.val)
    33
    34axiom exists_program : ∃ p : Lax808846.Ram.Program, ∃ c : ℕ, 0<c ∧
    35 ∀ n r : ℕ, ∀ width : ℕ, c*(n+r+(words n r).length+2)^3≤width →
    36 ∃ t≤c*(n+r+(words n r).length+2)^3,
    37 Lax808846.Ram.RunsTo width p [n,r] (words n r) t
    38
    39end Lax263307.NativeCatalog
    40
    Show Proof
    Formalization notes

    Input is [n,r]. Output is the list of subset masks in CoordinateCatalog order. The construction uses native Pascal tables, ranked-subset decoding, bit packing, and ordered buffer appends. Distinct cardinality blocks are disjoint, so the catalog's duplicate-removal operation leaves this order unchanged. Mask words represent subsets; their values are not used as addresses for an array of size 2^n.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…