Low-rank Boolean moments have bounded label support

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

proven

Loading review…

Natural Language Statement

Theorem

Lemma 5.2, with the sufficient selector-degree hypothesis used in its proof. Every rank-at-most-R moment matrix splits over at most R labels. The base blocks obey the binary moment identities and their ranks sum to at most R.

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax342547.LabelDecomposition

⊢Lax342547Proofs.LabelDecomposition.low_rank_label_decomposition

Lean source view on GitHub

Show types on hover

1	import Lax342547.BaseMoments
2	import Mathlib.LinearAlgebra.Matrix.Rank
3
4	/-!
5	---
6	title: Low-rank Boolean moments have bounded label support
7	type: theorem
8	---
9	Lemma 5.2, with the sufficient selector-degree hypothesis used in its proof.
10	Every rank-at-most-R moment matrix splits over at most R labels. The base
11	blocks obey the binary moment identities and their ranks sum to at most R.
12	-/
13
14	namespace Lax342547.LabelDecomposition
15
16	open Lax342547.MomentSpace Lax342547.BaseMoments
17
18	axiom low_rank_label_decomposition {Base : Type} [Fintype Base] {b degree R : ℕ}
19	(w : Matrix (SelectorCoordinates b degree × Option Base)
20	(SelectorCoordinates b degree × Option Base) Binary)
21	(hw : w ∈ momentSpace (selectorEval (degree := degree)) Set.univ)
22	(hrank : w.rank ≤ R) (hdegree : 6 * R + 4 ≤ degree) :
23	∃ L : Finset (Fin b → Binary),
24	∃ Z : (Fin b → Binary) → Matrix (Option Base) (Option Base) Binary,
25	L.card ≤ R ∧ (∀ s ∈ L, IsBaseMoment (Z s)) ∧
26	(∑ s ∈ L, (Z s).rank) ≤ R ∧
27	∀ i k, w i k = ∑ s ∈ L, selectorEval s i.1 * selectorEval s k.1 * Z s i.2 k.2
28
29	end Lax342547.LabelDecomposition
30