GridShiftUnique

def Nibble.AX1.gridShift (n : ℕ) (j k : Fin n) : ℕ

The shift f(j,k) = (j+k) mod n.

Equations

• Nibble.AX1.gridShift n j k = (↑j + ↑k) % n

theorem Nibble.AX1.gridShift_UW_injective {n : ℕ} : Function.Injective fun (p : Fin n × Fin n) => (gridShift n p.1 p.2, ↑p.1)

The U–W block pair is used at most once: (j,k) ↦ (f(j,k), j) is injective.

theorem Nibble.AX1.gridShift_UX_injective {n : ℕ} : Function.Injective fun (p : Fin n × Fin n) => (gridShift n p.1 p.2, ↑p.2)

The U–X block pair is used at most once: (j,k) ↦ (f(j,k), k) is injective.

theorem Nibble.AX1.gridShift_WX_injective {n : ℕ} : Function.Injective fun (p : Fin n × Fin n) => (↑p.1, ↑p.2)

The W–X block pair is used at most once: (j,k) ↦ (j,k) is injective (trivial).

theorem Nibble.AX1.gridShift_label_injective {n : ℕ} : Function.Injective fun (p : Fin n × Fin n) => (gridShift n p.1 p.2, ↑p.1, ↑p.2)

Consequence: the diagonal grid labelling is injective — distinct (j,k) give distinct sub-triples (f(j,k), j, k). (Immediate from any one of the block-pair injectivities, e.g. WX.)

GridDesign

The index arithmetic of the diagonal design

theorem Nibble.AX1.eq_of_div_mod_eq {n i i' : ℕ} (hdiv : i / n = i' / n) (hmod : i % n = i' % n) : i = i'

Two indices below n² with the same quotient and remainder mod n are equal.

def Nibble.AX1.gridIdxA (n i : ℕ) : ℕ

The U-block index of the i-th member of the diagonal design.

Equations

• Nibble.AX1.gridIdxA n i = (i / n + i % n) % n

def Nibble.AX1.gridIdxB (n i : ℕ) : ℕ

The W-block index of the i-th member of the diagonal design.

Equations

• Nibble.AX1.gridIdxB n i = i / n

def Nibble.AX1.gridIdxC (n i : ℕ) : ℕ

The X-block index of the i-th member of the diagonal design.

Equations

• Nibble.AX1.gridIdxC n i = i % n

theorem Nibble.AX1.gridIdxA_lt {n : ℕ} (hn : 0 < n) (i : ℕ) : gridIdxA n i < n

theorem Nibble.AX1.gridIdxB_lt {n i : ℕ} (hi : i < n * n) : gridIdxB n i < n

theorem Nibble.AX1.gridIdxC_lt {n : ℕ} (hn : 0 < n) (i : ℕ) : gridIdxC n i < n

theorem Nibble.AX1.gridIdx_AB_inj {n i i' : ℕ} (hi : i < n * n) (hi' : i' < n * n) (hA : gridIdxA n i = gridIdxA n i') (hB : gridIdxB n i = gridIdxB n i') : i = i'

The U–W block pair is used at most once.

theorem Nibble.AX1.gridIdx_AC_inj {n i i' : ℕ} (hi : i < n * n) (hi' : i' < n * n) (hA : gridIdxA n i = gridIdxA n i') (hC : gridIdxC n i = gridIdxC n i') : i = i'

The U–X block pair is used at most once.

theorem Nibble.AX1.gridIdx_BC_inj {n i i' : ℕ} (hB : gridIdxB n i = gridIdxB n i') (hC : gridIdxC n i = gridIdxC n i') : i = i'

The W–X block pair is used at most once.

Locating an edge in the block structure

def Nibble.AX1.pairIn {V : Type} (S T : Finset V) (x y : V) : Prop

The two endpoints of an edge lie one in S and one in T.

Equations

• Nibble.AX1.pairIn S T x y = (x ∈ S ∧ y ∈ T ∨ x ∈ T ∧ y ∈ S)

theorem Nibble.AX1.pairIn_symm {V : Type} {S T : Finset V} {x y : V} (h : pairIn S T x y) : pairIn T S x y

theorem Nibble.AX1.crossAdj_iff_pairIn {V : Type} {U W X : Finset V} {x y : V} : crossAdj U W X x y ↔ pairIn U W x y ∨ pairIn U X x y ∨ pairIn W X x y

crossAdj is exactly the disjunction of the three pairIns.

theorem Nibble.AX1.pairIn_absurd {V : Type} {S T S' T' : Finset V} {x y : V} (h : pairIn S T x y) (h' : pairIn S' T' x y) (h1 : Disjoint S S') (h2 : Disjoint S T') : False

Two different pairs of blocks cannot carry the same edge, if one of the two blocks of the first pair is disjoint from both blocks of the second.

theorem Nibble.AX1.pairIn_match {V : Type} {S T S' T' : Finset V} {x y : V} (h : pairIn S T x y) (h' : pairIn S' T' x y) (hST' : Disjoint S T') (hTS' : Disjoint T S') : ¬Disjoint S S' ∧ ¬Disjoint T T'

The same pair of clusters carrying the same edge forces the two blocks to meet.

The design

def Nibble.AX1.gridA {V : Type} (n : ℕ) (Ub : ℕ → Finset V) (i : ℕ) : Finset V

The U-part of the i-th member of the diagonal design.

Equations

• Nibble.AX1.gridA n Ub i = Ub (Nibble.AX1.gridIdxA n i)

def Nibble.AX1.gridB {V : Type} (n : ℕ) (Wb : ℕ → Finset V) (i : ℕ) : Finset V

The W-part of the i-th member of the diagonal design.

Equations

• Nibble.AX1.gridB n Wb i = Wb (Nibble.AX1.gridIdxB n i)

def Nibble.AX1.gridC {V : Type} (n : ℕ) (Xb : ℕ → Finset V) (i : ℕ) : Finset V

The X-part of the i-th member of the diagonal design.

Equations

• Nibble.AX1.gridC n Xb i = Xb (Nibble.AX1.gridIdxC n i)

theorem Nibble.AX1.gridDesign_pairwise_edgeDisjoint {V : Type} (G : SimpleGraph V) {n : ℕ} (Ub Wb Xb : ℕ → Finset V) (hUU : ∀ a < n, ∀ b < n, a ≠ b → Disjoint (Ub a) (Ub b)) (hWW : ∀ a < n, ∀ b < n, a ≠ b → Disjoint (Wb a) (Wb b)) (hXX : ∀ a < n, ∀ b < n, a ≠ b → Disjoint (Xb a) (Xb b)) (hUW : ∀ a < n, ∀ b < n, Disjoint (Ub a) (Wb b)) (hUX : ∀ a < n, ∀ b < n, Disjoint (Ub a) (Xb b)) (hWX : ∀ a < n, ∀ b < n, Disjoint (Wb a) (Xb b)) {i : ℕ} (hi : i < n * n) {i' : ℕ} (hi' : i' < n * n) (hne : i ≠ i') (x y : V) (h : (tripleGraph G (gridA n Ub i) (gridB n Wb i) (gridC n Xb i)).Adj x y) : ¬(tripleGraph G (gridA n Ub i') (gridB n Wb i') (gridC n Xb i')).Adj x y

The diagonal design is edge-disjoint. If the sub-blocks of each cluster are pairwise disjoint and the sub-blocks of different clusters are disjoint, then two distinct members of the diagonal family have no common edge: a common edge determines the pair of blocks that carries it, hence — by Nibble.AX1.gridShift_UW_injective and its companions, in the form Nibble.AX1.gridIdx_AB_inj, Nibble.AX1.gridIdx_AC_inj, Nibble.AX1.gridIdx_BC_inj — the member.