Lax Lean Archive

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

Sparse normalized representatives of shared concrete tensors

Lax342547.SparseRepresentatives · concepts/Lax342547/SparseRepresentatives.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

    Low total component rank yields a unique representative vanishing at a strict majority of tags, with the quantitative support bound. Shared ambient tensors have equal chiStar values on these representatives.

    Concept map
    11 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 cutSize_le_rank proven

    2 normalized_representation proven

    3 shared_chiStar proven

    4 shared_sparse_profiles proven

    Lean source view on GitHub

    1import Lax342547.CutSparsity
    2import Lax342547.ConcreteCut
    3import Lax342547.TensorIntersections
    4
    5/-!
    6---
    7title: Sparse normalized representatives of shared concrete tensors
    8type: lemma
    9---
    10Low total component rank yields a unique representative vanishing at a
    11strict majority of tags, with the quantitative support bound. Shared
    12ambient tensors have equal chiStar values on these representatives.
    13-/
    14
    15namespace Lax342547.SparseRepresentatives
    16
    17open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    18open Lax342547.CutProfiles Lax342547.CutSparsity Lax342547.ConcreteCut
    19open Lax342547.RawFrames Lax342547.TensorIntersections
    20
    21def Normalized {k n b degree : ℕ} (x : Profile k n b degree)
    22 (w : Representation k n b degree) : Prop :=
    23 representationCut k n b degree w = x.val ∧
    24 2 * k + 1 < 2 * valueCount w.val 0
    25
    26axiom cutSize_le_rank {Tag I : Type} [Fintype Tag] [Fintype I]
    27 [Fintype (Component Tag)] (w : Tag → Matrix I I Binary) :
    28 cutSize w ≤ ∑ e : Component Tag, (cutMap w e).rank
    29
    30axiom normalized_representation {k n b degree : ℕ} (R : ℕ)
    31 (hsmall : 4 * R < (2 * k + 1) * (2 * k + 1)) (x : Profile k n b degree)
    32 (hrank : (∑ e, (x.val e).rank) ≤ R) :
    33 ∃! w : Representation k n b degree, Normalized x w ∧
    34 (2 * k + 1) * supportSize w.val ≤ 2 * R
    35
    36axiom shared_chiStar {k n b degree r h N : ℕ}
    37 (hr : 2 * r ≤ n) (hd : 1 ≤ degree) (M : Fin b → Matrix (Fin n) (Fin n) Binary)
    38 (F G : Component (Tag k) → Frame (Coordinate k n b degree) (Fin h) (Fin N) (selfGram hr hd M))
    39 (w v : Representation k n b degree)
    40 (hw : 2 * k + 1 < 2 * valueCount w.val 0)
    41 (hv : 2 * k + 1 < 2 * valueCount v.val 0)
    42 (heq : profileMap F (representationCut k n b degree w) =
    43 profileMap G (representationCut k n b degree v)) :
    44 chiStar hr w = chiStar hr v
    45
    46axiom shared_sparse_profiles {k n b degree r h N : ℕ}
    47 (hr : 2 * r ≤ n) (hd : 1 ≤ degree) (M : Fin b → Matrix (Fin n) (Fin n) Binary)
    48 (F G : Component (Tag k) → Frame (Coordinate k n b degree) (Fin h) (Fin N) (selfGram hr hd M))
    49 (R : ℕ) (hsmall : 4 * R < (2 * k + 1) * (2 * k + 1))
    50 (hinter : (∑ e, Module.finrank Binary (intersectionSpace (F e).P (G e).P)) ≤ R)
    51 (x y : Profile k n b degree) (heq : profileMap F x.val = profileMap G y.val) :
    52 ∃ w v : Representation k n b degree, Normalized x w ∧ Normalized y v ∧
    53 (2 * k + 1) * supportSize w.val ≤ 2 * R ∧
    54 (2 * k + 1) * supportSize v.val ≤ 2 * R ∧ chiStar hr w = chiStar hr v
    55
    56end Lax342547.SparseRepresentatives
    57
    Show ProofShow 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…