Lax Lean Archive

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

Majority normalization of sparse cut profiles

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

    Counting unequal unordered tag pairs forces a strict majority whenever four times the cut support is smaller than the square of the tag count. Subtracting its common value gives a unique majority-zero representative.

    Concept map
    3 concepts; 2 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 exists_majority proven

    2 exists_unique_normalized proven

    3 majority_unique proven

    4 minority_bound proven

    5 unequal_card_le proven

    Lean source view on GitHub

    1import Lax342547.CutProfiles
    2import Mathlib.Data.Fintype.Card
    3
    4/-!
    5---
    6title: Majority normalization of sparse cut profiles
    7type: lemma
    8---
    9Counting unequal unordered tag pairs forces a strict majority whenever
    10four times the cut support is smaller than the square of the tag count.
    11Subtracting its common value gives a unique majority-zero representative.
    12-/
    13
    14namespace Lax342547.CutSparsity
    15
    16open Lax342547.MomentSpace Lax342547.CutProfiles
    17
    18variable {Tag V : Type} [AddCommGroup V] [Module Binary V]
    19
    20def UnequalPairs (w : Tag → V) := {p : Tag × Tag // w p.1 ≠ w p.2}
    21
    22def NonzeroCuts (w : Tag → V) := {e : Component Tag // cutMap w e ≠ 0}
    23
    24noncomputable def cutSize (w : Tag → V) : ℕ := Nat.card (NonzeroCuts w)
    25
    26noncomputable def valueCount (w : Tag → V) (c : V) : ℕ := Nat.card {t : Tag // w t = c}
    27
    28noncomputable def supportSize (w : Tag → V) : ℕ := Nat.card {t : Tag // w t ≠ 0}
    29
    30axiom unequal_card_le [Fintype Tag] (w : Tag → V) :
    31 Nat.card (UnequalPairs w) ≤ 2 * cutSize w
    32
    33axiom exists_majority [Fintype Tag] (w : Tag → V)
    34 (h : 4 * cutSize w < Fintype.card Tag * Fintype.card Tag) :
    35 ∃ c : V, Fintype.card Tag < 2 * valueCount w c
    36
    37axiom minority_bound [Fintype Tag] (w : Tag → V) (c : V)
    38 (h : Fintype.card Tag < 2 * valueCount w c) :
    39 Fintype.card Tag * Nat.card {t : Tag // w t ≠ c} ≤ 2 * cutSize w
    40
    41axiom majority_unique [Fintype Tag] [Nonempty Tag] (w v : Tag → V)
    42 (hcut : cutMap w = cutMap v)
    43 (hw : Fintype.card Tag < 2 * valueCount w 0)
    44 (hv : Fintype.card Tag < 2 * valueCount v 0) : w = v
    45
    46axiom exists_unique_normalized [Fintype Tag] [Nonempty Tag]
    47 (W : Tag → Submodule Binary V)
    48 (hW : ∀ S : Finset Tag, Fintype.card Tag < 2 * S.card →
    49 (⨅ t : {t // t ∈ S}, W t.val) ≤ ⨅ t, W t)
    50 (w : Tag → V) (hw : ∀ t, w t ∈ W t)
    51 (h : 4 * cutSize w < Fintype.card Tag * Fintype.card Tag) :
    52 ∃! v : Tag → V, (∀ t, v t ∈ W t) ∧ cutMap v = cutMap w ∧
    53 Fintype.card Tag < 2 * valueCount v 0 ∧
    54 Fintype.card Tag * supportSize v ≤ 2 * cutSize w
    55
    56end Lax342547.CutSparsity
    57
    Show ProofShow ProofShow ProofShow ProofShow Proof
    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…