CoreGapBlockCoverCoupled

The arithmetic of the construction

The block scale τ is large (8 ≤ τ·δ), the blocks have size between ¾τδ and ⁵⁄₄τ, and the regularity scale ε₁ is small compared with δ, μ₂ and η. The four lemmas below are the only computations the reduction needs; they are stated in isolation to keep the context small.

def Nibble.AX1.BlockCoverResidualCoupled : Prop

The coupled block-allocation residual. Given the accuracy ε, a density threshold δ ≤ ε, the block uniformity scale ε₂ that the caller needs and a scale floor T₀, the residual names a regularity window ε₁₀ > 0; for every regularity scale ε₁ ≤ ε₁₀ it then names a relative block size α with ε₁/8 ≤ α, 2α ≤ 1 and (ε₁/8)/α ≤ ε₂ — the three inequalities the transfer of regularity from the clusters to the blocks needs — and, for all large enough (ε₁/8)-regular equipartitions, a family of block sub-triples at that α with pairwise disjoint vertex-pair rectangles carrying the fractional optimum up to ε|V|².

Compared with Nibble.AX1.BlockCoverResidualFine the two scales ε₁ and α are no longer universally quantified independently: the residual may demand that the regularity scale be fine (hence the number of clusters large) and may pick the relative block size itself (hence the number of blocks per cluster large). Both are exactly what the reduction to AX1 leaves free, which is why Nibble.AX1.ax1_of_blockCoverCoupled still goes through.

Equations

• One or more equations did not get rendered due to their size.

theorem Nibble.AX1.subTripleDesignLocalResidual_of_blockCoverCoupled (h : BlockCoverResidualCoupled) : SubTripleDesignLocalResidual

theorem Nibble.AX1.ax1_of_blockCoverCoupled (h : BlockCoverResidualCoupled) : AX1Statement

AX1 from the coupled block-allocation residual.

Axiom check

CoreGapBlockAlloc

The covering sum of one member

theorem Nibble.AX1.prod_approx_of_sizes {τ y z a b : ℝ} (hτ : 0 ≤ τ) (hy0 : 0 ≤ y) (hy1 : y ≤ 1) (hz0 : 0 ≤ z) (hz1 : z ≤ 1) (ha : |a - τ * z| ≤ 1) (hb : |b - τ * y| ≤ 1) : |a * b - τ ^ 2 * (y * z)| ≤ 2 * τ + 1

A product of two prescribed sizes is the product of the two scaled densities, up to 2τ + 1.

theorem Nibble.AX1.cover_approx_of_gridSubTriple {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {ep de α τ : ℝ} {U W X A B C : Finset V} (hτ : 0 ≤ τ) (h : IsGridSubTriple G P ep de α τ U W X A B C) : |↑(G.edgeDensity U W) * ↑A.card * ↑B.card + ↑(G.edgeDensity U X) * ↑A.card * ↑C.card + ↑(G.edgeDensity W X) * ↑B.card * ↑C.card - 3 * τ ^ 2 * (↑(G.edgeDensity U W) * ↑(G.edgeDensity U X) * ↑(G.edgeDensity W X))| ≤ 6 * τ + 3

The covering sum of one block sub-triple is balanced. With the prescribed sizes of Nibble.AX1.IsGridSubTriple, the covering sum of a member is three times τ² times the product of its three cluster densities, up to an additive 6τ + 3.

Members on nearly disjoint cluster triples never clash

theorem Nibble.AX1.exists_clusters_of_mem_tripleRect {V : Type} [DecidableEq V] {U W X A B C : Finset V} (hUW : U ≠ W) (hUX : U ≠ X) (hWX : W ≠ X) (hA : A ⊆ U) (hB : B ⊆ W) (hC : C ⊆ X) {u v : V} (h : (u, v) ∈ tripleRect A B C) : ∃ S ∈ {U, W, X}, ∃ T ∈ {U, W, X}, S ≠ T ∧ u ∈ S ∧ v ∈ T

The two coordinates of a point of a rectangle lie in two different clusters of the triple.

theorem Nibble.AX1.tripleRect_disjoint_of_clusters {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) {U W X U' W' X' A B C A' B' C' : Finset V} (hU : U ∈ P.parts) (hW : W ∈ P.parts) (hX : X ∈ P.parts) (hU' : U' ∈ P.parts) (hW' : W' ∈ P.parts) (hX' : X' ∈ P.parts) (hUW : U ≠ W) (hUX : U ≠ X) (hWX : W ≠ X) (hUW' : U' ≠ W') (hUX' : U' ≠ X') (hWX' : W' ≠ X') (hA : A ⊆ U) (hB : B ⊆ W) (hC : C ⊆ X) (hA' : A' ⊆ U') (hB' : B' ⊆ W') (hC' : C' ⊆ X') (hshare : ({U, W, X} ∩ {U', W', X'}).card ≤ 1) : Disjoint (tripleRect A B C) (tripleRect A' B' C')

Automatic disjointness. If the cluster triples of two members share at most one cluster, their vertex-pair rectangles are disjoint. Hence the disjointness clause of the residual only ever has to be verified for two members sharing a whole cluster pair.

The bookkeeping bridge: value of the family ⟹ the covering clause

theorem Nibble.AX1.nu3star_le_cover_of_family_value {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {ep de ep₀ de₀ α τ θ E : ℝ} {k : ℕ} (U W X A B C : ℕ → Finset V) (hτ : 0 ≤ τ) (hθ : 0 ≤ θ) (hgrid : ∀ i < k, IsGridSubTriple G P ep₀ de₀ α τ (U i) (W i) (X i) (A i) (B i) (C i)) (hval : (∑ p ∈ P.parts.offDiag with θ ≤ ↑(G.edgeDensity p.1 p.2), ↑(G.edgeDensity p.1 p.2) * ↑p.1.card * ↑p.2.card) / 6 ≤ ∑ i ∈ Finset.range k, τ ^ 2 * (↑(G.edgeDensity (U i) (W i)) * ↑(G.edgeDensity (U i) (X i)) * ↑(G.edgeDensity (W i) (X i))) + E) : YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ (∑ i ∈ Finset.range k, (↑(G.edgeDensity (U i) (W i)) * ↑(A i).card * ↑(B i).card + ↑(G.edgeDensity (U i) (X i)) * ↑(A i).card * ↑(C i).card + ↑(G.edgeDensity (W i) (X i)) * ↑(B i).card * ↑(C i).card)) / 3 + (θ * ↑(Fintype.card V) ^ 2 / 6 + E + ↑k * (2 * τ + 1))

The covering clause of the residual follows from a lower bound on the value of the family. Write x, y, z for the three cluster densities of a member; its value is τ²·xyz, one third of its balanced covering sum (Nibble.AX1.cover_approx_of_gridSubTriple). If the total value of the family recovers the cluster capacity LP of the cluster pairs of density at least θ, up to E, then the covering clause of Nibble.AX1.BlockCoverResidualFine holds with total error θ·|V|²/6 + E + k·(2τ + 1).

This is the tight bookkeeping of the block-allocation route: by Nibble.AX1.cover_sum_le_cluster_capacity the covering sum of a disjoint family can never exceed the same capacity LP, so the hypothesis hval is not only sufficient but essentially necessary.

Axiom check

ClusterTripleLP

The program

def Nibble.AX1.clusterPairCap {V : Type} (G : SimpleGraph V) [DecidableRel G.Adj] (S T : Finset V) : ℝ

The density capacity of a cluster pair: d(S,T)·|S|·|T|, the number of edges of G between S and T.

Equations

• Nibble.AX1.clusterPairCap G S T = ↑(G.edgeDensity S T) * ↑S.card * ↑T.card

def Nibble.AX1.triplesThrough {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (S T : ↥P.parts) : Finset (Finset ↥P.parts)

The cluster triples through a given pair of clusters.

Equations

• Nibble.AX1.triplesThrough P S T = {th : Finset ↥P.parts | S ∈ th ∧ T ∈ th}

def Nibble.AX1.IsClusterTripleLP {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) (x : Finset ↥P.parts → ℝ) : Prop

Feasibility for the cluster-triple LP: nonnegative weights on the cluster triples, supported on the triangles of the cluster graph, whose total through any cluster pair is at most the density capacity of that pair.

Equations

• One or more equations did not get rendered due to their size.

def Nibble.AX1.clusterLPValue {V : Type} [Fintype V] [DecidableEq V] {P : Finpartition Finset.univ} (x : Finset ↥P.parts → ℝ) : ℝ

The value of a point of the cluster-triple LP.

Equations

• Nibble.AX1.clusterLPValue x = ∑ th : Finset ↥P.parts, x th

noncomputable def Nibble.AX1.clusterLPSupport {V : Type} [Fintype V] [DecidableEq V] {P : Finpartition Finset.univ} (x : Finset ↥P.parts → ℝ) : Finset (Finset ↥P.parts)

The support of a point of the cluster-triple LP.

Equations

• Nibble.AX1.clusterLPSupport x = {th : Finset ↥P.parts | x th ≠ 0}

The bridge: ν₃* of the reduced graph is below the LP

theorem Nibble.AX1.exists_clusterTripleLP {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {η : ℝ} (hη : 0 < η) : ∃ (x : Finset ↥P.parts → ℝ), IsClusterTripleLP G P ep de x ∧ YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ clusterLPValue x + η

The bridge. For every slack η > 0 there is a feasible point of the cluster-triple LP whose value is within η of ν₃* of the regularity-reduced graph.

Sparsification

theorem Nibble.AX1.exists_sparse_clusterTripleLP {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {x : Finset ↥P.parts → ℝ} (hx : IsClusterTripleLP G P ep de x) : ∃ (y : Finset ↥P.parts → ℝ), IsClusterTripleLP G P ep de y ∧ clusterLPValue x ≤ clusterLPValue y ∧ (clusterLPSupport y).card ≤ P.parts.card ^ 2

Sparsification of the cluster-triple LP. A feasible point can be replaced by a feasible point of at least the same value whose support has at most #P.parts ^ 2 triples.

theorem Nibble.AX1.exists_sparse_clusterTripleLP_nu3star {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {η : ℝ} (hη : 0 < η) : ∃ (y : Finset ↥P.parts → ℝ), IsClusterTripleLP G P ep de y ∧ (clusterLPSupport y).card ≤ P.parts.card ^ 2 ∧ YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ clusterLPValue y + η

The bridge and the sparsification, combined. For every slack η > 0 there is a feasible point of the cluster-triple LP with at most #P.parts ^ 2 triples in its support whose value is within η of ν₃* of the regularity-reduced graph.

The covering clause, in LP form

theorem Nibble.AX1.nu3star_le_cover_of_family_lp_value {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {ep de ep₀ de₀ α τ E η : ℝ} {k : ℕ} (U W X A B C : ℕ → Finset V) (hτ : 0 ≤ τ) (hgrid : ∀ i < k, IsGridSubTriple G P ep₀ de₀ α τ (U i) (W i) (X i) (A i) (B i) (C i)) {x : Finset ↥P.parts → ℝ} (hnu : YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ clusterLPValue x + η) (hval : clusterLPValue x ≤ ∑ i ∈ Finset.range k, τ ^ 2 * (↑(G.edgeDensity (U i) (W i)) * ↑(G.edgeDensity (U i) (X i)) * ↑(G.edgeDensity (W i) (X i))) + E) : YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ (∑ i ∈ Finset.range k, (↑(G.edgeDensity (U i) (W i)) * ↑(A i).card * ↑(B i).card + ↑(G.edgeDensity (U i) (X i)) * ↑(A i).card * ↑(C i).card + ↑(G.edgeDensity (W i) (X i)) * ↑(B i).card * ↑(C i).card)) / 3 + (E + η + ↑k * (2 * τ + 1))

The covering clause of the residual, in LP form. If the total value τ²·xyz of a family of block sub-triples recovers the value of a point of the cluster-triple LP that itself dominates ν₃* (up to η), then the covering clause of Nibble.AX1.BlockCoverResidualCoupled holds with total error E + η + k·(2τ + 1).

This is the LP-form replacement of Nibble.AX1.nu3star_le_cover_of_family_value, whose right-hand side is the full cluster capacity: the full capacity is not reachable by a coherent family of block sub-triples — a cluster triple with d(S,T) = 1 and d(S,Y) = d(T,Y) = θ cannot tile S × T — whereas the LP optimum is exactly what the coarse-cell construction realises.

Axiom check

ClusterTripleLPCount

theorem Nibble.AX1.sum_pair_fibers {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (y : Finset ↥P.parts → ℝ) (F : Finset (↥P.parts × ↥P.parts)) : ∑ p ∈ F, ∑ th ∈ triplesThrough P p.1 p.2, y th = ∑ th : Finset ↥P.parts, y th * ↑{p ∈ F | p.1 ∈ th ∧ p.2 ∈ th}.card

The fibre identity. Summing the LP mass through the pairs of a set F of ordered cluster pairs charges every triple with the number of pairs of F it contains.

theorem Nibble.AX1.sum_card_mul_card_le {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) : ∑ p : ↥P.parts × ↥P.parts, ↑(↑p.1).card * ↑(↑p.2).card ≤ ↑(Fintype.card V) ^ 2

The sizes of two clusters multiply out to at most |V|² over all ordered pairs.

theorem Nibble.AX1.clusterLPValue_le_sq {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {y : Finset ↥P.parts → ℝ} (hy : IsClusterTripleLP G P ep de y) : 6 * clusterLPValue y ≤ ↑(Fintype.card V) ^ 2

The value of a feasible point of the cluster-triple LP is at most |V|²/6.

noncomputable def Nibble.AX1.sparseTriples {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (δ : ℝ) : Finset (Finset ↥P.parts)

The triples of the LP that use a cluster pair of density below δ.

Equations

• Nibble.AX1.sparseTriples G P δ = {th : Finset ↥P.parts | ∃ S ∈ th, ∃ T ∈ th, S ≠ T ∧ ↑(G.edgeDensity ↑S ↑T) < δ}

theorem Nibble.AX1.sum_sparse_triples_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {δ : ℝ} (hδ0 : 0 ≤ δ) {y : Finset ↥P.parts → ℝ} (hy : IsClusterTripleLP G P ep de y) : 2 * ∑ th ∈ sparseTriples G P δ, y th ≤ δ * ↑(Fintype.card V) ^ 2

The mass of the triples using a sparse cluster pair is at most δ|V|²/2. Every such triple contains at least two ordered pairs of density below δ, and the capacities of those pairs add up to at most δ|V|².

CoarseCellBlocks

A subset of a prescribed size

noncomputable def Nibble.AX1.takeSub {V : Type} (A : Finset V) (n : ℕ) : Finset V

A chosen subset of A with n elements (all of A if n is too large).

Equations

• Nibble.AX1.takeSub A n = if h : n ≤ A.card then ⋯.choose else A

theorem Nibble.AX1.takeSub_subset {V : Type} (A : Finset V) (n : ℕ) : takeSub A n ⊆ A

theorem Nibble.AX1.card_takeSub {V : Type} {A : Finset V} {n : ℕ} (h : n ≤ A.card) : (takeSub A n).card = n

The union of a set of coarse cells

noncomputable def Nibble.AX1.cellUnion {V : Type} [DecidableEq V] (S : Finset V) (l : ℕ) {P : ℕ} (I : Finset (Fin P)) : Finset V

The union of the coarse cells of S indexed by I, at cell length l.

Equations

• Nibble.AX1.cellUnion S l I = I.biUnion fun (i : Fin P) => Nibble.AX1.blockOf S l ↑i

theorem Nibble.AX1.cellUnion_subset {V : Type} [DecidableEq V] (S : Finset V) (l : ℕ) {P : ℕ} (I : Finset (Fin P)) : cellUnion S l I ⊆ S

theorem Nibble.AX1.card_cellUnion {V : Type} [DecidableEq V] (S : Finset V) {l P : ℕ} (hl : 0 < l) (I : Finset (Fin P)) (hfit : P * l ≤ S.card) : (cellUnion S l I).card = I.card * l

theorem Nibble.AX1.cellUnion_disjoint {V : Type} [DecidableEq V] (S : Finset V) (l : ℕ) {P : ℕ} {I J : Finset (Fin P)} (h : Disjoint I J) : Disjoint (cellUnion S l I) (cellUnion S l J)

noncomputable def Nibble.AX1.cellBlock {V : Type} [DecidableEq V] (S : Finset V) (l : ℕ) {P : ℕ} (I : Finset (Fin P)) (n : ℕ) : Finset V

The vertex block of a member: n vertices inside the union of its coarse cells.

Equations

• Nibble.AX1.cellBlock S l I n = Nibble.AX1.takeSub (Nibble.AX1.cellUnion S l I) n

theorem Nibble.AX1.cellBlock_subset_cellUnion {V : Type} [DecidableEq V] (S : Finset V) (l : ℕ) {P : ℕ} (I : Finset (Fin P)) (n : ℕ) : cellBlock S l I n ⊆ cellUnion S l I

theorem Nibble.AX1.cellBlock_subset {V : Type} [DecidableEq V] (S : Finset V) (l : ℕ) {P : ℕ} (I : Finset (Fin P)) (n : ℕ) : cellBlock S l I n ⊆ S

theorem Nibble.AX1.card_cellBlock {V : Type} [DecidableEq V] (S : Finset V) {l P : ℕ} (hl : 0 < l) (I : Finset (Fin P)) {n : ℕ} (hfit : P * l ≤ S.card) (hn : n ≤ I.card * l) : (cellBlock S l I n).card = n

The disjointness engine

theorem Nibble.AX1.exists_positions_of_mem_tripleRect {V : Type} [DecidableEq V] {f : ZMod 3 → Finset V} {x y : V} (h : (x, y) ∈ tripleRect (f 0) (f 1) (f 2)) : ∃ (a : ZMod 3) (b : ZMod 3), a ≠ b ∧ x ∈ f a ∧ y ∈ f b

The two positions of a vertex pair inside the rectangle of a member.

theorem Nibble.AX1.tripleRect_disjoint_of_shared_pairs {V : Type} [DecidableEq V] {clA clB blkA blkB : ZMod 3 → Finset V} (hA : ∀ (a : ZMod 3), blkA a ⊆ clA a) (hB : ∀ (a : ZMod 3), blkB a ⊆ clB a) (hpart : ∀ (a b : ZMod 3), ∀ v ∈ clA a, v ∈ clB b → clA a = clB b) (hdisj : ∀ (a b a' b' : ZMod 3), a ≠ b → a' ≠ b' → clA a = clB a' → clA b = clB b' → Disjoint (blkA a) (blkB a') ∨ Disjoint (blkA b) (blkB b')) : Disjoint (tripleRect (blkA 0) (blkA 1) (blkA 2)) (tripleRect (blkB 0) (blkB 1) (blkB 2))

The disjointness engine. Two members whose blocks sit inside clusters of a partition have disjoint vertex-pair rectangles as soon as, whenever they share a cluster pair, one of the two blocks carrying it is disjoint from the corresponding block of the other member.

CoarseCellAssembly

theorem Nibble.AX1.exists_gridSubTriple_family_of_placement {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) {ep de α τ : ℝ} {l Pn : ℕ} (hl : 0 < l) {κ : Type} (cl : κ → ZMod 3 → ↥Pp.parts) (sz bs : κ → ZMod 3 → ℕ) (I : κ → ZMod 3 → Finset (Fin Pn)) (Good : Finset κ) (hcard : ∀ (c : κ) (a : ZMod 3), (I c a).card = sz c a) (hfitS : ∀ S ∈ Pp.parts, Pn * l ≤ S.card) (hbs : ∀ (c : κ) (a : ZMod 3), bs c a ≤ sz c a * l) (hdisjI : ∀ c ∈ Good, ∀ c' ∈ Good, c ≠ c' → ∀ (a b a' b' : ZMod 3), a ≠ b → a' ≠ b' → cl c a = cl c' a' → cl c b = cl c' b' → Disjoint (I c a) (I c' a') ∨ Disjoint (I c b) (I c' b')) (hgood : ∀ c ∈ Good, GoodTriple G Pp ep de ↑(cl c 0) ↑(cl c 1) ↑(cl c 2)) (hrel : ∀ c ∈ Good, ∀ (a : ZMod 3), α * ↑(↑(cl c a)).card ≤ ↑(bs c a)) (hshape : ∀ c ∈ Good, ∀ (a : ZMod 3), |↑(bs c a) - τ * ↑(G.edgeDensity ↑(cl c (a + 1)) ↑(cl c (a + 2)))| ≤ 1) : ∃ (k : ℕ) (U : ℕ → Finset V) (W : ℕ → Finset V) (X : ℕ → Finset V) (A : ℕ → Finset V) (B : ℕ → Finset V) (C : ℕ → Finset V), k ≤ Good.card ∧ (∀ i < k, IsGridSubTriple G Pp ep de α τ (U i) (W i) (X i) (A i) (B i) (C i)) ∧ (∀ i < k, ∀ j < k, i ≠ j → Disjoint (tripleRect (A i) (B i) (C i)) (tripleRect (A j) (B j) (C j))) ∧ ∑ i ∈ Finset.range k, τ ^ 2 * (↑(G.edgeDensity (U i) (W i)) * ↑(G.edgeDensity (U i) (X i)) * ↑(G.edgeDensity (W i) (X i))) = ∑ c ∈ Good, τ ^ 2 * (↑(G.edgeDensity ↑(cl c 0) ↑(cl c 1)) * ↑(G.edgeDensity ↑(cl c 0) ↑(cl c 2)) * ↑(G.edgeDensity ↑(cl c 1) ↑(cl c 2)))

The block family of a coarse-cell placement. Every copy of Good becomes a member of the family: its block at the position a is the prescribed number bs c a of vertices inside the union of the coarse cells I c a of its cluster cl c a.

GridTripleDesign

def Nibble.AX1.triShift {q : ℕ} (s v : ZMod q) : ZMod q

The quadratic shift of the cluster v in the cluster triple of vertex sum s.

Equations

• Nibble.AX1.triShift s v = v ^ 2 - v * s

def Nibble.AX1.triBlock {q : ℕ} (s v j : ZMod q) : ZMod q

The block used in cluster v by the j-th sub-triple of the cluster triple of vertex sum s.

Equations

• Nibble.AX1.triBlock s v j = j + Nibble.AX1.triShift s v

theorem Nibble.AX1.triShift_diff {q : ℕ} (s a b : ZMod q) : triShift s b - triShift s a = (b - a) * (a + b - s)

The diagonal offset: in the cluster pair {a, b}, the triple of vertex sum s occupies the diagonal {(k, k + (b - a) * (a + b - s))}. For a ≠ b this offset is an injective function of s, which is the whole point of the design.

theorem Nibble.AX1.triShift_diff_third {q : ℕ} (u w x : ZMod q) : triShift (u + w + x) w - triShift (u + w + x) u = -((w - u) * x)

For the triple {u, w, x} the offset of the pair {u, w} is -(w - u) * x: it depends on the pair and on the third vertex only.

@[simp]

theorem Nibble.AX1.triBlock_zero_shift {q : ℕ} (s v : ZMod q) : triBlock s v 0 = triShift s v

theorem Nibble.AX1.triBlock_bijective {q : ℕ} (s v : ZMod q) : Function.Bijective (triBlock s v)

Inside one cluster triple, the q sub-triples cover every block of every one of the three clusters exactly once.

theorem Nibble.AX1.triBlock_eq_lineTriple {q : ℕ} (s u w x j : ZMod q) : (triBlock s u j, triBlock s w j, triBlock s x j) = lineTriple (triShift s w - triShift s u) (triShift s x - triShift s u) (triBlock s u j)

The sub-triples of a fixed cluster triple form a line in the sense of Nibble.AX1.lineTriple, re-based at the first cluster: all single-triple facts proved for the line design apply.

def Nibble.AX1.triPairSet {q : ℕ} [NeZero q] (s a b : ZMod q) : Finset (ZMod q × ZMod q)

The block pairs a cluster triple uses in one of its cluster pairs: the diagonal of offset (b - a) * (a + b - s).

Equations

• Nibble.AX1.triPairSet s a b = Finset.image (fun (j : ZMod q) => (Nibble.AX1.triBlock s a j, Nibble.AX1.triBlock s b j)) Finset.univ

theorem Nibble.AX1.mem_triPairSet {q : ℕ} [NeZero q] {s a b : ZMod q} {p : ZMod q × ZMod q} : p ∈ triPairSet s a b ↔ ∃ (j : ZMod q), (triBlock s a j, triBlock s b j) = p

theorem Nibble.AX1.triPairSet_snd_eq {q : ℕ} [NeZero q] {s a b : ZMod q} {p : ZMod q × ZMod q} (hp : p ∈ triPairSet s a b) : p.2 = p.1 + (triShift s b - triShift s a)

A block pair of the diagonal is determined by its first coordinate.

theorem Nibble.AX1.card_triPairSet {q : ℕ} [NeZero q] (s a b : ZMod q) : (triPairSet s a b).card = q

Each cluster triple uses exactly q block pairs in each of its three cluster pairs.

theorem Nibble.AX1.triPairSet_disjoint {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] {s s' a b : ZMod q} (hab : a ≠ b) (hs : s ≠ s') : Disjoint (triPairSet s a b) (triPairSet s' a b)

The allocation is consistent: two cluster triples with different vertex sums use disjoint sets of block pairs in every cluster pair {a, b} they share. Since the vertex sum is symmetric, this holds simultaneously for all three pairs of each triple.

theorem Nibble.AX1.triPairSet_disjoint_of_third {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] {a b x x' : ZMod q} (hab : a ≠ b) (hx : x ≠ x') : Disjoint (triPairSet (a + b + x) a b) (triPairSet (a + b + x') a b)

The form used in the assembly: two cluster triples through the same cluster pair {a, b}, with different third clusters, never share a block pair.

theorem Nibble.AX1.card_triPairSet_biUnion {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] {a b : ZMod q} (hab : a ≠ b) (S : Finset (ZMod q)) : (S.biUnion fun (x : ZMod q) => triPairSet (a + b + x) a b).card = q * S.card

Feasibility of the allocation: if S is a set of third clusters, the triples {a, b, x}, x ∈ S, together use q * #S distinct block pairs of the cluster pair {a, b}, out of the q ^ 2 block pairs available. So the design fits as long as the number of cluster triples through a pair is at most the number q of blocks per cluster.

theorem Nibble.AX1.card_triPairSet_biUnion_le {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] {a b : ZMod q} (hab : a ≠ b) (S : Finset (ZMod q)) : (S.biUnion fun (x : ZMod q) => triPairSet (a + b + x) a b).card ≤ q ^ 2

The block pairs used in a cluster pair are of course among all q ^ 2 of them, so the count above is a genuine packing bound: the design never overflows a cluster pair.

GridTripleDesignRect

theorem Nibble.AX1.exists_third_of_card_three {α : Type} [DecidableEq α] {T : Finset α} (hT : T.card = 3) {a b : α} (ha : a ∈ T) (hb : b ∈ T) (hab : a ≠ b) : ∃ (x : α), T = {a, b, x} ∧ x ≠ a ∧ x ≠ b

A 3-element set containing two distinct elements a, b is {a, b, x} for a unique third element x.

def Nibble.AX1.triCells {q : ℕ} (T : Finset (ZMod q)) (j : ZMod q) : Finset (ZMod q × ZMod q)

The cells used by one sub-triple of the design: the cluster triple T (a set of cluster indices) with offset j occupies, in the cluster v ∈ T, the block triBlock (∑ T) v j.

Equations

• Nibble.AX1.triCells T j = Finset.image (fun (c : ZMod q) => (c, Nibble.AX1.triBlock (∑ v ∈ T, v) c j)) T

theorem Nibble.AX1.mem_triCells {q : ℕ} {T : Finset (ZMod q)} {j v : ZMod q} (hv : v ∈ T) : (v, triBlock (∑ u ∈ T, u) v j) ∈ triCells T j

theorem Nibble.AX1.sum_triple {q : ℕ} {a b x : ZMod q} (hab : a ≠ b) (hxa : x ≠ a) (hxb : x ≠ b) : ∑ v ∈ {a, b, x}, v = a + b + x

theorem Nibble.AX1.triCells_inter_subsingleton {q : ℕ} [Fact (Nat.Prime q)] {T T' : Finset (ZMod q)} {j j' : ZMod q} (hT : T.card = 3) (hT' : T'.card = 3) (hne : ¬(T = T' ∧ j = j')) {c d : ZMod q × ZMod q} (hc : c ∈ triCells T j) (hc' : c ∈ triCells T' j') (hd : d ∈ triCells T j) (hd' : d ∈ triCells T' j') : c = d

Two distinct sub-triples of the design share at most one cell.

If the cluster triples differ, or if they agree but the offsets differ, then no two cells can be common: two common cells lie in two distinct clusters a ≠ b, and the identity triShift s b - triShift s a = (b - a) * (a + b - s) then forces the two vertex sums to be equal, hence the offsets to be equal and (both triples being {a, b, ·} with the same sum) the triples to be equal.

theorem Nibble.AX1.tripleRect_cells {V : Type} [DecidableEq V] {ι : Type} (blk : ι → Finset V) (S : Finset ι) {A B C : Finset V} {cA cB cC : ι} (hA : A ⊆ blk cA) (hB : B ⊆ blk cB) (hC : C ⊆ blk cC) (hcA : cA ∈ S) (hcB : cB ∈ S) (hcC : cC ∈ S) (hAB : cA ≠ cB) (hAC : cA ≠ cC) (hBC : cB ≠ cC) {p : V × V} (hp : p ∈ tripleRect A B C) : ∃ (c : ι) (d : ι), c ∈ S ∧ d ∈ S ∧ c ≠ d ∧ p.1 ∈ blk c ∧ p.2 ∈ blk d

A vertex pair of the rectangle of a sub-triple whose three parts sit in the blocks of three distinct cells joins the blocks of two distinct cells.

theorem Nibble.AX1.tripleRect_disjoint_of_design {q : ℕ} [Fact (Nat.Prime q)] {V : Type} [DecidableEq V] (blk : ZMod q × ZMod q → Finset V) (hblk : ∀ (c d : ZMod q × ZMod q), c ≠ d → Disjoint (blk c) (blk d)) {T T' : Finset (ZMod q)} {j j' : ZMod q} (hT : T.card = 3) (hT' : T'.card = 3) (hne : ¬(T = T' ∧ j = j')) {u w x u' w' x' : ZMod q} (huT : u ∈ T) (hwT : w ∈ T) (hxT : x ∈ T) (huw : u ≠ w) (hux : u ≠ x) (hwx : w ≠ x) (huT' : u' ∈ T') (hwT' : w' ∈ T') (hxT' : x' ∈ T') (huw' : u' ≠ w') (hux' : u' ≠ x') (hwx' : w' ≠ x') {A B C A' B' C' : Finset V} (hA : A ⊆ blk (u, triBlock (∑ v ∈ T, v) u j)) (hB : B ⊆ blk (w, triBlock (∑ v ∈ T, v) w j)) (hC : C ⊆ blk (x, triBlock (∑ v ∈ T, v) x j)) (hA' : A' ⊆ blk (u', triBlock (∑ v ∈ T', v) u' j')) (hB' : B' ⊆ blk (w', triBlock (∑ v ∈ T', v) w' j')) (hC' : C' ⊆ blk (x', triBlock (∑ v ∈ T', v) x' j')) : Disjoint (tripleRect A B C) (tripleRect A' B' C')

The rectangles of the design are pairwise disjoint.

blk assigns to each cell — a pair (cluster index, block index) — a block of vertices, distinct cells getting disjoint blocks. Two distinct sub-triples of the design (different cluster triples, or the same cluster triple with different offsets) have disjoint vertex-pair rectangles, whatever subsets of the three blocks are used as the parts A, B, C.

Combined with Nibble.AX1.tripleGraph_edgeDisjoint_of_rect_disjoint and Nibble.AX1.sum_area_le_of_rect_disjoint this is the edge-disjointness requirement of Nibble.AX1.BlockCoverResidual for the whole family of cluster triples at once.

BlockCoverUniformAux

Naming the three elements of a triangle

noncomputable def Nibble.AX1.pick3 {ι : Type} [Nonempty ι] [DecidableEq ι] (t : Finset ι) : ι × ι × ι

An ordered triple listing the three elements of t, when t has exactly three of them.

Equations

• One or more equations did not get rendered due to their size.

theorem Nibble.AX1.pick3_spec {ι : Type} [Nonempty ι] [DecidableEq ι] {t : Finset ι} (h3 : t.card = 3) : (pick3 t).1 ≠ (pick3 t).2.1 ∧ (pick3 t).1 ≠ (pick3 t).2.2 ∧ (pick3 t).2.1 ≠ (pick3 t).2.2 ∧ t = {(pick3 t).1, (pick3 t).2.1, (pick3 t).2.2}

theorem Nibble.AX1.pick3_mem {ι : Type} [Nonempty ι] [DecidableEq ι] {t : Finset ι} (h3 : t.card = 3) : (pick3 t).1 ∈ t ∧ (pick3 t).2.1 ∈ t ∧ (pick3 t).2.2 ∈ t

Cell disjointness gives rectangle disjointness

theorem Nibble.AX1.tripleRect_disjoint_of_cells_inter {V : Type} [DecidableEq V] {ι : Type} [DecidableEq ι] (blk : ι → Finset V) (hblk : ∀ (c d : ι), c ≠ d → Disjoint (blk c) (blk d)) {t t' : Finset ι} (hint : (t ∩ t').card ≤ 1) {cA cB cC cA' cB' cC' : ι} (hcA : cA ∈ t) (hcB : cB ∈ t) (hcC : cC ∈ t) (hAB : cA ≠ cB) (hAC : cA ≠ cC) (hBC : cB ≠ cC) (hcA' : cA' ∈ t') (hcB' : cB' ∈ t') (hcC' : cC' ∈ t') (hAB' : cA' ≠ cB') (hAC' : cA' ≠ cC') (hBC' : cB' ≠ cC') {A B C A' B' C' : Finset V} (hA : A ⊆ blk cA) (hB : B ⊆ blk cB) (hC : C ⊆ blk cC) (hA' : A' ⊆ blk cA') (hB' : B' ⊆ blk cB') (hC' : C' ⊆ blk cC') : Disjoint (tripleRect A B C) (tripleRect A' B' C')

The rectangles of two members that share at most one cell are disjoint. blk assigns a block of vertices to each cell, distinct cells getting disjoint blocks; a member is given by three distinct cells, and its three parts are subsets of the corresponding blocks.

A crude bound for the fractional triangle packing number

theorem Nibble.AX1.nu3star_le_card_sq {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] : YusterE.nu3star H ≤ ↑(Fintype.card W) ^ 2

CoarseCellCoupled

The three positions of a cluster triple

theorem Nibble.AX1.zmod3_cases (a : ZMod 3) : a = 0 ∨ a = 1 ∨ a = 2

Every element of ZMod 3 is 0, 1 or 2.

Copies

def Nibble.AX1.copySet {ι : Type} [DecidableEq ι] (Gd : Finset ι) (n : ι → ℕ) : Finset (ι × ℕ)

The copies of the elements of Gd: n th copies of th.

Equations

• Nibble.AX1.copySet Gd n = Gd.biUnion fun (th : ι) => Finset.image (fun (j : ℕ) => (th, j)) (Finset.range (n th))

theorem Nibble.AX1.mem_copySet {ι : Type} [DecidableEq ι] {Gd : Finset ι} {n : ι → ℕ} {p : ι × ℕ} : p ∈ copySet Gd n ↔ p.1 ∈ Gd ∧ p.2 < n p.1

theorem Nibble.AX1.sum_copySet {ι : Type} [DecidableEq ι] {M : Type} [AddCommMonoid M] (Gd : Finset ι) (n : ι → ℕ) (f : ι → M) : ∑ p ∈ copySet Gd n, f p.1 = ∑ th ∈ Gd, n th • f th

theorem Nibble.AX1.card_copySet {ι : Type} [DecidableEq ι] (Gd : Finset ι) (n : ι → ℕ) : (copySet Gd n).card = ∑ th ∈ Gd, n th

noncomputable def Nibble.AX1.triPos {V : Type} [Fintype V] [DecidableEq V] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) (a : ZMod 3) : ↥Pp.parts

The three positions of a cluster triple, indexed by ZMod 3.

Equations

• Nibble.AX1.triPos Pp th a = if a = 0 then (Nibble.AX1.pick3 th).1 else if a = 1 then (Nibble.AX1.pick3 th).2.1 else (Nibble.AX1.pick3 th).2.2

theorem Nibble.AX1.triPos_mem {V : Type} [Fintype V] [DecidableEq V] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] {th : Finset ↥Pp.parts} (h3 : th.card = 3) (a : ZMod 3) : triPos Pp th a ∈ th

theorem Nibble.AX1.triPos_injective {V : Type} [Fintype V] [DecidableEq V] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] {th : Finset ↥Pp.parts} (h3 : th.card = 3) : Function.Injective (triPos Pp th)

noncomputable def Nibble.AX1.dOpp {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) (a : ZMod 3) : ℝ

The density of the cluster pair opposite to the position a.

Equations

• Nibble.AX1.dOpp G Pp th a = ↑(G.edgeDensity ↑(Nibble.AX1.triPos Pp th (a + 1)) ↑(Nibble.AX1.triPos Pp th (a + 2)))

noncomputable def Nibble.AX1.dProd {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) : ℝ

The density product of a cluster triple.

Equations

• Nibble.AX1.dProd G Pp th = Nibble.AX1.dOpp G Pp th 0 * Nibble.AX1.dOpp G Pp th 1 * Nibble.AX1.dOpp G Pp th 2

theorem Nibble.AX1.dOpp_nonneg {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) (a : ZMod 3) : 0 ≤ dOpp G Pp th a

theorem Nibble.AX1.dOpp_le_one {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) (a : ZMod 3) : dOpp G Pp th a ≤ 1

theorem Nibble.AX1.dOpp_zero {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) : dOpp G Pp th 0 = ↑(G.edgeDensity ↑(triPos Pp th 1) ↑(triPos Pp th 2))

theorem Nibble.AX1.dOpp_one {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) : dOpp G Pp th 1 = ↑(G.edgeDensity ↑(triPos Pp th 2) ↑(triPos Pp th 0))

theorem Nibble.AX1.dOpp_two {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) : dOpp G Pp th 2 = ↑(G.edgeDensity ↑(triPos Pp th 0) ↑(triPos Pp th 1))

theorem Nibble.AX1.dProd_eq {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) : dProd G Pp th = ↑(G.edgeDensity ↑(triPos Pp th 0) ↑(triPos Pp th 1)) * ↑(G.edgeDensity ↑(triPos Pp th 0) ↑(triPos Pp th 2)) * ↑(G.edgeDensity ↑(triPos Pp th 1) ↑(triPos Pp th 2))

The density product read off the three positions in their natural order.

theorem Nibble.AX1.dOpp_mul_dOpp_mul_dens {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Pp : Finpartition Finset.univ) [Nonempty ↥Pp.parts] (th : Finset ↥Pp.parts) {a b : ZMod 3} (hab : a ≠ b) : dOpp G Pp th a * dOpp G Pp th b * ↑(G.edgeDensity ↑(triPos Pp th a) ↑(triPos Pp th b)) = dProd G Pp th

The three opposite densities of a triple, seen from two of its positions. For two distinct positions a, b the density of the pair (a, b) is the density opposite to the third position, so the three factors multiply out to the density product.

Arithmetic of the parameters

The reduction

theorem Nibble.AX1.blockCoverResidualCoupled_of_boxAllocation (hbox : BoxAllocationResidual) : BlockCoverResidualCoupled

The coarse-cell reduction: the small-box allocation residual implies the coupled block-allocation residual.

theorem Nibble.AX1.ax1_of_boxAllocation (hbox : BoxAllocationResidual) : AX1Statement

AX1 from the small-box allocation residual. Composing the reduction of this file with Nibble.AX1.ax1_of_blockCoverCoupled.