Lax Lean Archive

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

Fresh point-ray spans are disjoint from the nominal table spaces

Lax342547.KeySpans · concepts/Lax342547/KeySpans.lean · lax-342547

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

    Lemma

    The finite-set sparse exclusions give independence for arbitrary indexed families of at most fourteen rays per endpoint. In particular the span of all selected rays intersects each table space only at zero.

    Concept map
    11 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 exclusions_exists proven

    2 independent_sum proven

    3 span_disjoint proven

    Lean source view on GitHub

    1import Lax342547.FreshKeys
    2import Lax342547.NominalPrimal
    3
    4/-!
    5---
    6title: Fresh point-ray spans are disjoint from the nominal table spaces
    7type: lemma
    8---
    9The finite-set sparse exclusions give independence for arbitrary indexed
    10families of at most fourteen rays per endpoint. In particular the span
    11of all selected rays intersects each table space only at zero.
    12-/
    13
    14namespace Lax342547.KeySpans
    15
    16open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.TableSpaces
    17
    18variable {Base Comp H N : Type} {b degree : ℕ}
    19
    20def Excludes
    21 (P : Pin (Comp × Bool) (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) N)
    22 (A : Fin 2 → Finset (Fin b → Binary)) : Prop :=
    23 ∀ (a : Comp × Bool) (L : Fin 2 → Finset (Fin b → Binary))
    24 (c : Fin 2 → (Fin b → Binary) → Binary)
    25 (z : Fin 2 → (Fin b → Binary) → Base → Binary),
    26 (∀ i, (L i).card ≤ 14) → (∀ i, Disjoint (L i) (A i)) →
    27 (∑ i : Fin 2, ∑ s ∈ L i, c i s •
    28 primalEmbedding i (point (selectorEval (degree := degree)) s (z i s))) ∈ tableSpace P a →
    29 ∀ i s, s ∈ L i → c i s = 0
    30
    31def ray {I : Fin 2 → Type} (label : ∀ i, I i → Fin b → Binary)
    32 (base : ∀ i, I i → Base → Binary) (x : Σ i, I i) :
    33 (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) → Binary :=
    34 primalEmbedding x.1 (point (selectorEval (degree := degree)) (label x.1 x.2) (base x.1 x.2))
    35
    36axiom exclusions_exists [Fintype Base] [Fintype Comp] [Fintype H] {K R : ℕ}
    37 (P : Pin (Comp × Bool) (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) N)
    38 (hK : P.rank ≤ K) (hdegree : (K + 1) * (R + 14) ≤ degree + 1) :
    39 ∃ A : Fin 2 → Finset (Fin b → Binary),
    40 (∀ i, (A i).card ≤ 2 * Fintype.card Comp * K * (R + 14)) ∧ Excludes P A
    41
    42axiom independent_sum {I : Fin 2 → Type} [∀ i, Fintype (I i)]
    43 (P : Pin (Comp × Bool) (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) N)
    44 (A : Fin 2 → Finset (Fin b → Binary)) (hA : Excludes P A)
    45 (label : ∀ i, I i → Fin b → Binary) (base : ∀ i, I i → Base → Binary)
    46 (hlabel : ∀ i, Function.Injective (label i)) (hcard : ∀ i, Fintype.card (I i) ≤ 14)
    47 (hfresh : ∀ i x, label i x ∉ A i) (a : Comp × Bool) (c : (Σ i, I i) → Binary)
    48 (h : (∑ x, c x • ray (H := H) label base x) ∈ tableSpace P a) : ∀ x, c x = 0
    49
    50axiom span_disjoint {I : Fin 2 → Type} [∀ i, Fintype (I i)]
    51 (P : Pin (Comp × Bool) (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) N)
    52 (A : Fin 2 → Finset (Fin b → Binary)) (hA : Excludes P A)
    53 (label : ∀ i, I i → Fin b → Binary) (base : ∀ i, I i → Base → Binary)
    54 (hlabel : ∀ i, Function.Injective (label i)) (hcard : ∀ i, Fintype.card (I i) ≤ 14)
    55 (hfresh : ∀ i x, label i x ∉ A i) (a : Comp × Bool) :
    56 Disjoint (tableSpace P a) (Submodule.span Binary (Set.range (ray (H := H) label base)))
    57
    58end Lax342547.KeySpans
    59
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…