Documentation

LeanPool.AsymptoticTrianglePacking.Internal.AX1.GridLineDesign

GridLineDesign #

source
def Nibble.AX1.lineTriple {q : ℕ} (a b j : ZMod q) :
ZMod q × ZMod q × ZMod q

One block sub-triple of the line (a, b): the blocks j of U, j + a of W and j + b of X.

Equations
Instances For
    source
    @[simp]
    theorem Nibble.AX1.lineTriple_fst {q : ℕ} (a b j : ZMod q) :
    (lineTriple a b j).1 = j
    source
    @[simp]
    theorem Nibble.AX1.lineTriple_snd {q : ℕ} (a b j : ZMod q) :
    (lineTriple a b j).2.1 = j + a
    source
    @[simp]
    theorem Nibble.AX1.lineTriple_thd {q : ℕ} (a b j : ZMod q) :
    (lineTriple a b j).2.2 = j + b
    source
    theorem Nibble.AX1.diagIndex_bijective {q : ℕ} :
    Function.Bijective fun (x : ZMod q × ZMod q) => (x.2, x.2 + x.1)

    The q diagonals of a cluster pair partition its q² block pairs: the map sending a diagonal label a and a position j to the block pair (j, j + a) is a bijection. This is the allocation form of Nibble.AX1.gridUW_bijective: a cluster pair shared by several cluster triples is exactly covered as soon as the diagonals are distributed among them.

    source
    theorem Nibble.AX1.lineTriple_UW_unique {q : ℕ} {a b a' b' j j' : ZMod q} (hfst : (lineTriple a b j).1 = (lineTriple a' b' j').1) (hsnd : (lineTriple a b j).2.1 = (lineTriple a' b' j').2.1) :
    a = a' ∧ j = j'

    Two block sub-triples of a family of lines with distinct first labels never use the same block pair of the cluster pair (U, W).

    source
    theorem Nibble.AX1.lineTriple_UX_unique {q : ℕ} {a b a' b' j j' : ZMod q} (hfst : (lineTriple a b j).1 = (lineTriple a' b' j').1) (hthd : (lineTriple a b j).2.2 = (lineTriple a' b' j').2.2) :
    b = b' ∧ j = j'

    Two block sub-triples of a family of lines with distinct second labels never use the same block pair of the cluster pair (U, X).

    source
    theorem Nibble.AX1.lineTriple_WX_unique {q : ℕ} {a b a' b' j j' : ZMod q} (hsnd : (lineTriple a b j).2.1 = (lineTriple a' b' j').2.1) (hthd : (lineTriple a b j).2.2 = (lineTriple a' b' j').2.2) :
    b - a = b' - a' ∧ j + a = j' + a'

    Two block sub-triples of a family of lines with distinct differences never use the same block pair of the cluster pair (W, X).

    source
    theorem Nibble.AX1.lineTriple_pair_disjoint {q : ℕ} {S T : Finset (ZMod q)} (hST : Disjoint S T) {a b a' b' : ZMod q} (ha : a ∈ S) (ha' : a' ∈ T) (j j' : ZMod q) (hfst : (lineTriple a b j).1 = (lineTriple a' b' j').1) :
    (lineTriple a b j).2.1 ≠ (lineTriple a' b' j').2.1

    The allocation criterion. Two cluster triples through the cluster pair (U, W) that are allocated disjoint sets of diagonals never use a common block pair of that cluster pair: the rectangles of the two triples inside U × W are disjoint.

    source
    theorem Nibble.AX1.card_diag_fiber {q : ℕ} [NeZero q] (a : ZMod q) :
    (Finset.image (fun (j : ZMod q) => (j, j + a)) Finset.univ).card = q

    The diagonals of one cluster pair are exactly q, and each has exactly q block pairs. Together with Nibble.AX1.diagIndex_bijective this is the counting behind the allocation: the diagonals allocated to the cluster triples through a pair tile that pair as soon as they partition ZMod q.