Lax Lean Archive

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

Triangle relations separate into individual label blocks

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

    Selector interpolation makes bounded-support block expansions unique. The union of three component supports has size at most 3R, so a triangle relation holds separately for every label, including absent labels.

    Concept map
    17 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 blocks_unique proven

    2 cut_triangle proven

    3 triangle_blocks proven

    Lean source view on GitHub

    1import Lax342547.TensorBlocks
    2import Lax342547.SelectorInterpolation
    3import Lax342547.ConcreteCut
    4
    5/-!
    6---
    7title: Triangle relations separate into individual label blocks
    8type: lemma
    9---
    10Selector interpolation makes bounded-support block expansions unique.
    11The union of three component supports has size at most 3R, so a triangle
    12relation holds separately for every label, including absent labels.
    13-/
    14
    15namespace Lax342547.LabelRelations
    16
    17open Lax342547.MomentSpace Lax342547.ConcreteGeometry Lax342547.TensorBlocks
    18open Lax342547.CutProfiles
    19
    20def supported {Label Base : Type} [DecidableEq Label] (L : Finset Label)
    21 (Z : Label → Matrix Base Base Binary) (s : Label) : Matrix Base Base Binary :=
    22 if s ∈ L then Z s else 0
    23
    24def edge {Tag : Type} [DecidableEq Tag] (a b : Tag) (h : a ≠ b) : Component Tag :=
    25 ⟨{a, b}, Finset.card_pair h⟩
    26
    27axiom blocks_unique {Base : Type} [Fintype Base] {b degree : ℕ}
    28 (L : Finset (Fin b → Binary)) (Z : (Fin b → Binary) → Matrix Base Base Binary)
    29 (hdegree : L.card ≤ degree + 1) (h : (∑ s ∈ L, block (selectorEval (degree := degree)) s (Z s)) = 0) :
    30 ∀ s ∈ L, Z s = 0
    31
    32axiom triangle_blocks {Base : Type} [Fintype Base] {b degree R : ℕ}
    33 (L : Fin 3 → Finset (Fin b → Binary))
    34 (Z : Fin 3 → (Fin b → Binary) → Matrix Base Base Binary)
    35 (hL : ∀ i, (L i).card ≤ R) (hdegree : 3 * R ≤ degree + 1)
    36 (h : (∑ i, ∑ s ∈ L i, block (selectorEval (degree := degree)) s (Z i s)) = 0) :
    37 ∀ s, (∑ i, supported (L i) (Z i) s) = 0
    38
    39axiom cut_triangle {Tag V : Type} [DecidableEq Tag] [AddCommGroup V] [Module Binary V]
    40 (w : Tag → V) (a b c : Tag) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) :
    41 cutMap w (edge a b hab) + cutMap w (edge b c hbc) + cutMap w (edge a c hac) = 0
    42
    43end Lax342547.LabelRelations
    44
    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…