Majority intersections in the cyclic tag geometry

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

proven

Loading review…

Natural Language Statement

Lemma

For $g=2k+1$ , the tag $l$ allows the block $O_{d,t}$ exactly when $l\in\{d+1,\ldots,d+k\}$ . The other three blocks are unrestricted. The intersection over more than $k$ tags is the all- $O$ -zero moment space, as asserted in the first part of Lemma 2.3.

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

lem✓Lax342547.TagGeometry

⊢Lax342547Proofs.TagGeometry.majority_intersection

Lean source view on GitHub

Show types on hover

1	import Lax342547.CutProfiles
2	import Mathlib.Data.ZMod.Basic
3
4	/-!
5	---
6	title: Majority intersections in the cyclic tag geometry
7	type: lemma
8	---
9	For $g=2k+1$ , the tag $l$ allows the block $O_{d,t}$ exactly when
10	$l\in\{d+1,\ldots,d+k\}$ . The other three blocks are unrestricted.
11	The intersection over more than $k$ tags is the all- $O$ -zero moment
12	space, as asserted in the first part of Lemma 2.3.
13	-/
14
15	namespace Lax342547.TagGeometry
16
17	open Lax342547.MomentSpace
18
19	abbrev Tag (k : ℕ) := ZMod (2 * k + 1)
20
21	def interval (k : ℕ) (d : Tag k) : Finset (Tag k) :=
22	Finset.univ.image (fun i : Fin k => d + (i.val + 1 : ℕ))
23
24	abbrev Base (k n : ℕ) := ((Tag k × Tag k) × Fin n) ⊕ (Fin 3 × Fin n)
25
26	def allowedBase (k n : ℕ) (l : Tag k) : Set (Base k n)
27	\| Sum.inl ((d, _), _) => l ∈ interval k d
28	\| Sum.inr _ => True
29
30	def commonBase (k n : ℕ) : Set (Base k n)
31	\| Sum.inl _ => False
32	\| Sum.inr _ => True
33
34	axiom majority_intersection {Label Coord : Type} (k n : ℕ)
35	(p : Label → Coord → Binary) (S : Finset (Tag k)) (hS : k < S.card) :
36	(⨅ l : {l // l ∈ S}, momentSpace p (allowedBase k n l.val)) =
37	momentSpace p (commonBase k n)
38
39	end Lax342547.TagGeometry
40