Lax Lean Archive

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

A computable catalog and index for moment coordinates

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

    Enumerate only subsets of size at most r+2, remove duplicates, and attach the cardinality proof to each entry. This lists each moment coordinate exactly once and gives a computable equivalence between coordinate indices and the coordinate type. The catalog has at most (r+3)(n+1)^(r+2) entries.

    Concept map
    10 concepts; 10 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 catalog_bound proven

    2 catalog_complete proven

    3 catalog_nodup proven

    4 catalog_positive proven

    5 catalog_two proven

    Lean source view on GitHub

    1import Lax263307.RationalConditioning
    2import Mathlib.Data.List.NodupEquivFin
    3import Mathlib.Data.List.Dedup
    4
    5/-!
    6---
    7title: A computable catalog and index for moment coordinates
    8type: theorem
    9---
    10Enumerate only subsets of size at most r+2, remove duplicates, and attach
    11the cardinality proof to each entry. This lists each moment coordinate
    12exactly once and gives a computable equivalence between coordinate indices
    13and the coordinate type. The catalog has at most (r+3)(n+1)^(r+2) entries.
    14
    15# Formalization notes
    16
    17The inverse index uses list search. This avoids a choice-based Fintype
    18equivalence in LP input construction. Duplicate removal is permitted as
    19its polynomial overhead in the catalog length still fits the intended
    20quasipolynomial bound. Its actual RAM implementation remains an obligation.
    21-/
    22
    23namespace Lax263307.CoordinateCatalog
    24
    25open LinearRelaxation RationalConditioning
    26
    27private theorem candidate_complete_aux (n r : ℕ) (A : Finset (Fin n)) :
    28 A ∈ candidates n r ↔ A.card ≤ r := by
    29 constructor
    30 · intro h
    31 obtain ⟨j, hj, hm⟩ := List.mem_flatMap.mp h
    32 obtain ⟨l, hl, rfl⟩ := List.mem_map.mp hm
    33 have hsub := (List.mem_sublistsLen.mp hl).1
    34 have hlen := (List.mem_sublistsLen.mp hl).2
    35 have hnd := hsub.nodup (List.nodup_finRange n)
    36 rw [List.toFinset_card_of_nodup hnd, hlen]
    37 have := List.mem_range.mp hj
    38 omega
    39 · intro hA
    40 let l := (List.finRange n).filter fun v => decide (v ∈ A)
    41 have hsub : List.Sublist l (List.finRange n) := List.filter_sublist
    42 have hnd : l.Nodup := hsub.nodup (List.nodup_finRange n)
    43 have heq : l.toFinset = A := by ext v; simp [l]
    44 have hlen : l.length = A.card := by rw [← List.toFinset_card_of_nodup hnd, heq]
    45 apply List.mem_flatMap.mpr
    46 refine ⟨A.card, List.mem_range.mpr (by omega), ?_⟩
    47 apply List.mem_map.mpr
    48 exact ⟨l, List.mem_sublistsLen.mpr ⟨hsub, hlen⟩, heq⟩
    49
    50def sets (n r : ℕ) : List (Finset (Fin n)) := (candidates n (r + 2)).dedup
    51
    52def catalog (n r : ℕ) : List (Coordinate n r) :=
    53 (sets n r).attach.map (fun A => ⟨A.val,
    54 (candidate_complete_aux n (r + 2) A.val).mp
    55 (List.mem_dedup.mp A.property)⟩)
    56
    57axiom catalog_complete (n r : ℕ) (A : Coordinate n r) : A ∈ catalog n r
    58
    59axiom catalog_nodup (n r : ℕ) : (catalog n r).Nodup
    60
    61private theorem catalog_complete_aux (n r : ℕ) (A : Coordinate n r) : A ∈ catalog n r := by
    62 have hmem : A.val ∈ sets n r :=
    63 List.mem_dedup.mpr ((candidate_complete_aux n (r + 2) A.val).mpr A.property)
    64 apply List.mem_map.mpr
    65 exact ⟨⟨A.val, hmem⟩, List.mem_attach _ _, Subtype.ext rfl⟩
    66
    67private theorem catalog_nodup_aux (n r : ℕ) : (catalog n r).Nodup := by
    68 have hnd : (sets n r).Nodup := List.nodup_dedup _
    69 apply hnd.attach.map
    70 intro A B h
    71 exact Subtype.ext (congrArg (fun C : Coordinate n r => C.val) h)
    72
    73def indexing (n r : ℕ) : Fin (catalog n r).length ≃ Coordinate n r :=
    74 List.Nodup.getEquivOfForallMemList (catalog n r) (catalog_nodup_aux n r) (catalog_complete_aux n r)
    75
    76
    77axiom catalog_bound (n r : ℕ) : (catalog n r).length ≤ (r + 3) * (n + 1) ^ (r + 2)
    78
    79axiom catalog_positive (n r : ℕ) : 0 < (catalog n r).length
    80
    81axiom catalog_two (n r : ℕ) (positive : 0 < n) : 2 ≤ (catalog n r).length
    82
    83end Lax263307.CoordinateCatalog
    84
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Formalization notes

    The inverse index uses list search. This avoids a choice-based Fintype equivalence in LP input construction. Duplicate removal is permitted as its polynomial overhead in the catalog length still fits the intended quasipolynomial bound. Its actual RAM implementation remains an obligation.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…