BoxPlacementCount

def Nibble.AX1.BoxCount.subs (P u : ℕ) : Finset (Finset (Fin P))

The cell sets of a prescribed size in one cluster.

Equations

• Nibble.AX1.BoxCount.subs P u = Finset.powersetCard u Finset.univ

def Nibble.AX1.BoxCount.plc (P : ℕ) (u : ZMod 3 → ℕ) : Finset (ZMod 3 → Finset (Fin P))

The placements of a copy with prescribed sizes u: one cell set per cluster.

Equations

• Nibble.AX1.BoxCount.plc P u = Fintype.piFinset fun (a : ZMod 3) => Nibble.AX1.BoxCount.subs P (u a)

theorem Nibble.AX1.BoxCount.mem_subs {P u : ℕ} {A : Finset (Fin P)} : A ∈ subs P u ↔ A.card = u

theorem Nibble.AX1.BoxCount.card_subs (P u : ℕ) : (subs P u).card = P.choose u

theorem Nibble.AX1.BoxCount.mem_plc {P : ℕ} {u : ZMod 3 → ℕ} {A : ZMod 3 → Finset (Fin P)} : A ∈ plc P u ↔ ∀ (a : ZMod 3), (A a).card = u a

Counting the cell sets of one cluster

theorem Nibble.AX1.BoxCount.card_subs_req {P u : ℕ} (B : Finset (Fin P)) (hB : B.card ≤ u) : {A ∈ subs P u | B ⊆ A}.card = (P - B.card).choose (u - B.card)

The subsets of prescribed size containing a prescribed set.

theorem Nibble.AX1.BoxCount.choose_mul_step {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) : n * (n - 1).choose (k - 1) = k * n.choose k

The absorption identity for binomial coefficients, in cleared form.

theorem Nibble.AX1.BoxCount.subs_one_mul {P u : ℕ} (huP : u ≤ P) (i : Fin P) : {A ∈ subs P u | {i} ⊆ A}.card * P = u * (subs P u).card

One prescribed cell in one cluster.

theorem Nibble.AX1.BoxCount.subs_two_mul {P u : ℕ} (huP : u ≤ P) {i i' : Fin P} (hii : i ≠ i') : {A ∈ subs P u | {i, i'} ⊆ A}.card * (P * (P - 1)) = u * (u - 1) * (subs P u).card

Two prescribed cells in one cluster.

Counting the placements

theorem Nibble.AX1.BoxCount.succ_ne_self (p : ZMod 3) : p ≠ p + 1

theorem Nibble.AX1.BoxCount.exists_third {p q : ZMod 3} (hpq : p ≠ q) : ∃ (t : ZMod 3), p ≠ t ∧ q ≠ t

Two distinct positions of a copy have a unique third.

theorem Nibble.AX1.BoxCount.univ_eq_three {p q t : ZMod 3} (hpq : p ≠ q) (hpt : p ≠ t) (hqt : q ≠ t) : Finset.univ = {p, q, t}

Three distinct positions exhaust ZMod 3.

theorem Nibble.AX1.BoxCount.mem_three {p q t : ZMod 3} (hpq : p ≠ q) (hpt : p ≠ t) (hqt : q ≠ t) (a : ZMod 3) : a = p ∨ a = q ∨ a = t

theorem Nibble.AX1.BoxCount.prod_three {M : Type u_1} [CommMonoid M] (f : ZMod 3 → M) {p q t : ZMod 3} (hpq : p ≠ q) (hpt : p ≠ t) (hqt : q ≠ t) : ∏ a : ZMod 3, f a = f p * f q * f t

A product over the three positions of a copy.

theorem Nibble.AX1.BoxCount.card_plc_req {P : ℕ} {u : ZMod 3 → ℕ} (req : ZMod 3 → Finset (Fin P)) : {A ∈ plc P u | ∀ (a : ZMod 3), req a ⊆ A a}.card = ∏ a : ZMod 3, {A ∈ subs P (u a) | req a ⊆ A}.card

The placements are the products of the cell sets: a coordinatewise condition splits.

theorem Nibble.AX1.BoxCount.card_plc_three {P : ℕ} {u : ZMod 3 → ℕ} {p q t : ZMod 3} (hpq : p ≠ q) (hpt : p ≠ t) (hqt : q ≠ t) (Bp Bq Bt : Finset (Fin P)) : {A ∈ plc P u | Bp ⊆ A p ∧ Bq ⊆ A q ∧ Bt ⊆ A t}.card = {A ∈ subs P (u p) | Bp ⊆ A}.card * {A ∈ subs P (u q) | Bq ⊆ A}.card * {A ∈ subs P (u t) | Bt ⊆ A}.card

The master count: a coordinatewise requirement splits into a product over the three clusters.

theorem Nibble.AX1.BoxCount.filter_empty_req {P : ℕ} (v : ℕ) : {A ∈ subs P v | ∅ ⊆ A} = subs P v

The empty requirement is no requirement.

theorem Nibble.AX1.BoxCount.card_plc_prod {P : ℕ} {u : ZMod 3 → ℕ} {p q t : ZMod 3} (hpq : p ≠ q) (hpt : p ≠ t) (hqt : q ≠ t) : (plc P u).card = (subs P (u p)).card * (subs P (u q)).card * (subs P (u t)).card

theorem Nibble.AX1.BoxCount.card_plc_pos {P : ℕ} {u : ZMod 3 → ℕ} (huP : ∀ (a : ZMod 3), u a ≤ P) : 0 < (plc P u).card

theorem Nibble.AX1.BoxCount.card_one {P : ℕ} {u : ZMod 3 → ℕ} (huP : ∀ (a : ZMod 3), u a ≤ P) (p : ZMod 3) (i : Fin P) : {A ∈ plc P u | i ∈ A p}.card * P = u p * (plc P u).card

theorem Nibble.AX1.BoxCount.card_two {P : ℕ} {u : ZMod 3 → ℕ} (huP : ∀ (a : ZMod 3), u a ≤ P) {p q : ZMod 3} (hpq : p ≠ q) (i j : Fin P) : {A ∈ plc P u | i ∈ A p ∧ j ∈ A q}.card * (P * P) = u p * u q * (plc P u).card

theorem Nibble.AX1.BoxCount.card_two_one {P : ℕ} {u : ZMod 3 → ℕ} (huP : ∀ (a : ZMod 3), u a ≤ P) {p q : ZMod 3} (hpq : p ≠ q) {i i' : Fin P} (hii : i ≠ i') (j : Fin P) : {A ∈ plc P u | i ∈ A p ∧ i' ∈ A p ∧ j ∈ A q}.card * (P * (P - 1) * P) = u p * (u p - 1) * u q * (plc P u).card

theorem Nibble.AX1.BoxCount.card_three {P : ℕ} {u : ZMod 3 → ℕ} (huP : ∀ (a : ZMod 3), u a ≤ P) {p q t : ZMod 3} (hpq : p ≠ q) (hpt : p ≠ t) (hqt : q ≠ t) (i j l : Fin P) : {A ∈ plc P u | i ∈ A p ∧ j ∈ A q ∧ l ∈ A t}.card * (P * P * P) = u p * u q * u t * (plc P u).card

BoxPlacementEdge

@[reducible, inline]

abbrev Nibble.AX1.Slot (ι : Type) (P : ℕ) : Type

A cell-pair slot of an ordered cluster pair.

Equations

• Nibble.AX1.Slot ι P = (ι × ι × Fin P × Fin P)

@[reducible, inline]

abbrev Nibble.AX1.PlaceVtx (ι κ : Type) (P : ℕ) : Type

The ground set of the placement hypergraph: the cell-pair slots and the copy tokens.

Equations

• Nibble.AX1.PlaceVtx ι κ P = (Nibble.AX1.Slot ι P ⊕ κ)

def Nibble.AX1.orient {ι : Type} {P : ℕ} (idx : ι → ℕ) (S T : ι) (i j : Fin P) : Slot ι P

The slot of the cell pair (i, j) of the cluster pair (S, T), written in the orientation prescribed by idx.

Equations

• Nibble.AX1.orient idx S T i j = if idx S < idx T then (S, T, i, j) else (T, S, j, i)

def Nibble.AX1.rect {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} (idx : ι → ℕ) (cl : κ → ZMod 3 → ι) (c : κ) (A : ZMod 3 → Finset (Fin P)) (a : ZMod 3) : Finset (PlaceVtx ι κ P)

The rectangle that the placement A of the copy c occupies in the cluster pair (cl c a, cl c (a+1)).

Equations

• Nibble.AX1.rect idx cl c A a = Finset.image (fun (p : Fin P × Fin P) => Sum.inl (Nibble.AX1.orient idx (cl c a) (cl c (a + 1)) p.1 p.2)) (A a ×ˢ A (a + 1))

def Nibble.AX1.placeEdge {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} (idx : ι → ℕ) (cl : κ → ZMod 3 → ι) (c : κ) (A : ZMod 3 → Finset (Fin P)) : Finset (PlaceVtx ι κ P)

The edge of the placement A of the copy c: its token and its three rectangles.

Equations

• Nibble.AX1.placeEdge idx cl c A = insert (Sum.inr c) (Finset.univ.biUnion (Nibble.AX1.rect idx cl c A))

theorem Nibble.AX1.zmod3_consec {p q : ZMod 3} (hpq : p ≠ q) : q = p + 1 ∨ p = q + 1

In ZMod 3 two distinct positions are consecutive one way or the other.

theorem Nibble.AX1.zmod3_pair_ne {a b : ZMod 3} (hab : a ≠ b) : ¬(a = b ∧ a + 1 = b + 1 ∨ a = b + 1 ∧ a + 1 = b)

Two distinct positions of a copy give two distinct cluster pairs.

theorem Nibble.AX1.orient_symm {ι : Type} {P : ℕ} {idx : ι → ℕ} {S T : ι} (h : idx S ≠ idx T) (i j : Fin P) : orient idx T S j i = orient idx S T i j

The orientation is symmetric on distinct clusters.

theorem Nibble.AX1.orient_inj {ι : Type} {P : ℕ} {idx : ι → ℕ} (S T : ι) : Function.Injective fun (p : Fin P × Fin P) => orient idx S T p.1 p.2

theorem Nibble.AX1.mem_rect {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} {a : ZMod 3} {x : Slot ι P} : Sum.inl x ∈ rect idx cl c A a ↔ ∃ i ∈ A a, ∃ j ∈ A (a + 1), orient idx (cl c a) (cl c (a + 1)) i j = x

theorem Nibble.AX1.inr_notMem_rect {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} {a : ZMod 3} {c' : κ} : Sum.inr c' ∉ rect idx cl c A a

theorem Nibble.AX1.mem_placeEdge_inr {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (c' : κ) : Sum.inr c' ∈ placeEdge idx cl c A ↔ c' = c

An edge contains exactly one token, that of its copy.

theorem Nibble.AX1.placeEdge_toRight {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} : (placeEdge idx cl c A).toRight = {c}

The tokens of an edge: exactly the token of its copy.

theorem Nibble.AX1.mem_placeEdge_orient {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) {p q : ZMod 3} (hpq : p ≠ q) {i j : Fin P} (hi : i ∈ A p) (hj : j ∈ A q) : Sum.inl (orient idx (cl c p) (cl c q) i j) ∈ placeEdge idx cl c A

Occupying a slot. The placement A of c occupies the slot of the cell pair (i, j) in the cluster pair (cl c p, cl c q) whenever i ∈ A p and j ∈ A q.

theorem Nibble.AX1.mem_placeEdge_inl {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) (S T : ι) (i j : Fin P) : Sum.inl (S, T, i, j) ∈ placeEdge idx cl c A ↔ ∃ (p : ZMod 3) (q : ZMod 3), p ≠ q ∧ cl c p = S ∧ cl c q = T ∧ idx S < idx T ∧ i ∈ A p ∧ j ∈ A q

The slots of an edge. The placement A of c occupies the slot (S, T, i, j) exactly when S and T are two clusters of c, in the orientation prescribed by idx, and i, j are cells of the corresponding two sets of A.

theorem Nibble.AX1.mem_placeEdge_iff {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) {p q : ZMod 3} (hpq : p ≠ q) (i j : Fin P) : Sum.inl (orient idx (cl c p) (cl c q) i j) ∈ placeEdge idx cl c A ↔ i ∈ A p ∧ j ∈ A q

A cell pair of an edge.

theorem Nibble.AX1.card_rect {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (a : ZMod 3) : (rect idx cl c A a).card = (A a).card * (A (a + 1)).card

theorem Nibble.AX1.rect_disjoint {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (hcl : Function.Injective (cl c)) {a b : ZMod 3} (hab : a ≠ b) : Disjoint (rect idx cl c A a) (rect idx cl c A b)

theorem Nibble.AX1.placeEdge_card {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (hcl : Function.Injective (cl c)) : (placeEdge idx cl c A).card = 1 + ∑ a : ZMod 3, (A a).card * (A (a + 1)).card

The size of an edge: the token plus the three rectangles.

theorem Nibble.AX1.placeEdge_inj {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {c : κ} {A : ZMod 3 → Finset (Fin P)} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) {c' : κ} {A' : ZMod 3 → Finset (Fin P)} (hcl' : Function.Injective (cl c')) (hA : ∀ (a : ZMod 3), (A a).Nonempty) (hA' : ∀ (a : ZMod 3), (A' a).Nonempty) (h : placeEdge idx cl c A = placeEdge idx cl c' A') : c = c' ∧ A = A'

A placement is recoverable from its edge.

Box placement hypergraph

def Nibble.AX1.BoxPlace.placeCard {κ : Type} (P : ℕ) (sz : κ → ZMod 3 → ℕ) (c : κ) : ℕ

The number of placements of the copy c.

Equations

• Nibble.AX1.BoxPlace.placeCard P sz c = (Nibble.AX1.BoxCount.plc P (sz c)).card

def Nibble.AX1.BoxPlace.placeFam {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] (P : ℕ) (idx : ι → ℕ) (cl : κ → ZMod 3 → ι) (sz : κ → ZMod 3 → ℕ) : Finset (Finset (PlaceVtx ι κ P))

The placement hypergraph: all placements of all copies.

Equations

• Nibble.AX1.BoxPlace.placeFam P idx cl sz = Finset.univ.biUnion fun (c : κ) => Finset.image (Nibble.AX1.placeEdge idx cl c) (Nibble.AX1.BoxCount.plc P (sz c))

noncomputable def Nibble.AX1.BoxPlace.placeWt {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] (P : ℕ) (sz : κ → ZMod 3 → ℕ) : Finset (PlaceVtx ι κ P) → ℝ

The weight of a placement: the reciprocal of the number of placements of its copy, so that the placements of a copy carry total weight 1.

Equations

• Nibble.AX1.BoxPlace.placeWt P sz U = ∑ c : κ, if Sum.inr c ∈ U then (↑(Nibble.AX1.BoxPlace.placeCard P sz c))⁻¹ else 0

theorem Nibble.AX1.BoxPlace.mem_placeFam {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {U : Finset (PlaceVtx ι κ P)} (hU : U ∈ placeFam P idx cl sz) : ∃ (c : κ), ∃ A ∈ BoxCount.plc P (sz c), U = placeEdge idx cl c A

The edges of the placement hypergraph are the placements.

def Nibble.AX1.BoxPlace.boxDemandC {ι κ : Type} [DecidableEq ι] (cl : κ → ZMod 3 → ι) (sz : κ → ZMod 3 → ℕ) (c : κ) (S T : ι) : ℝ

The contribution of one copy to the demand of the cluster pair (S, T).

Equations

• Nibble.AX1.BoxPlace.boxDemandC cl sz c S T = ∑ a : ZMod 3, ∑ b : ZMod 3, if cl c a = S ∧ cl c b = T then ↑(sz c a) * ↑(sz c b) else 0

theorem Nibble.AX1.BoxPlace.boxDemand_eq_sum {ι κ : Type} [DecidableEq ι] [Fintype κ] {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (S T : ι) : boxDemand cl sz S T = ∑ c : κ, boxDemandC cl sz c S T

theorem Nibble.AX1.BoxPlace.boxDemandC_nonneg {ι κ : Type} [DecidableEq ι] {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (c : κ) (S T : ι) : 0 ≤ boxDemandC cl sz c S T

theorem Nibble.AX1.BoxPlace.sz_mul_le_boxDemandC {ι κ : Type} [DecidableEq ι] {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {c : κ} {p q : ZMod 3} {S T : ι} (hp : cl c p = S) (hq : cl c q = T) : ↑(sz c p) * ↑(sz c q) ≤ boxDemandC cl sz c S T

Sums over the placement hypergraph

theorem Nibble.AX1.BoxPlace.plc_nonempty {κ : Type} {P : ℕ} {sz : κ → ZMod 3 → ℕ} (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) {c : κ} {A : ZMod 3 → Finset (Fin P)} (hA : A ∈ BoxCount.plc P (sz c)) (a : ZMod 3) : (A a).Nonempty

theorem Nibble.AX1.BoxPlace.sum_placeFam {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (f : Finset (PlaceVtx ι κ P) → ℝ) : ∑ U ∈ placeFam P idx cl sz, f U = ∑ c : κ, ∑ A ∈ BoxCount.plc P (sz c), f (placeEdge idx cl c A)

A sum over the placement hypergraph is a sum over copies and placements.

theorem Nibble.AX1.BoxPlace.sum_placeFam_filter {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (p : Finset (PlaceVtx ι κ P) → Prop) [DecidablePred p] (f : Finset (PlaceVtx ι κ P) → ℝ) : ∑ U ∈ placeFam P idx cl sz with p U, f U = ∑ c : κ, ∑ A ∈ BoxCount.plc P (sz c) with p (placeEdge idx cl c A), f (placeEdge idx cl c A)

A filtered sum over the placement hypergraph.

theorem Nibble.AX1.BoxPlace.placeWt_edge {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (c : κ) (A : ZMod 3 → Finset (Fin P)) : placeWt P sz (placeEdge idx cl c A) = (↑(placeCard P sz c))⁻¹

The weight of a placement of c is the reciprocal of the number of placements of c.

theorem Nibble.AX1.BoxPlace.placeWt_nonneg {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {sz : κ → ZMod 3 → ℕ} (U : Finset (PlaceVtx ι κ P)) : 0 ≤ placeWt P sz U

theorem Nibble.AX1.BoxPlace.placeCard_pos {κ : Type} {P : ℕ} {sz : κ → ZMod 3 → ℕ} (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (c : κ) : 0 < placeCard P sz c

theorem Nibble.AX1.BoxPlace.sum_placeWt {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) : ∑ U ∈ placeFam P idx cl sz, placeWt P sz U = ↑(Fintype.card κ)

The total weight is the number of copies.

theorem Nibble.AX1.BoxPlace.placeFam_edge_size {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hcl : ∀ (c : κ), Function.Injective (cl c)) {s₀ : ℕ} (hs : ∀ (c : κ) (a : ZMod 3), sz c a ≤ s₀) (U : Finset (PlaceVtx ι κ P)) (hU : U ∈ placeFam P idx cl sz) : U.Nonempty ∧ U.card ≤ 1 + 3 * s₀ ^ 2

Every edge is nonempty and has at most 1 + 3s₀² vertices.

The count of the placements of one copy through a prescribed slot

theorem Nibble.AX1.BoxPlace.sum_inv_const {κ : Type} {P : ℕ} {sz : κ → ZMod 3 → ℕ} {c : κ} (F : Finset (ZMod 3 → Finset (Fin P))) : ∑ _A ∈ F, (↑(placeCard P sz c))⁻¹ = ↑F.card * (↑(placeCard P sz c))⁻¹

theorem Nibble.AX1.BoxPlace.slot_count_core {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {c : κ} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) (hszP : ∀ (a : ZMod 3), sz c a ≤ P) (hP : 0 < P) (S T : ι) (i j : Fin P) {F : Finset (ZMod 3 → Finset (Fin P))} (hFsub : F ⊆ BoxCount.plc P (sz c)) (hF : ∀ A ∈ F, Sum.inl (S, T, i, j) ∈ placeEdge idx cl c A) : F = ∅ ∨ ∃ (p : ZMod 3) (q : ZMod 3), p ≠ q ∧ cl c p = S ∧ cl c q = T ∧ ↑F.card * (↑(placeCard P sz c))⁻¹ ≤ ↑(sz c p) * ↑(sz c q) / ↑P ^ 2

The placements of c occupying a prescribed slot: either there are none, or the slot is the cell pair (i, j) of two clusters cl c p, cl c q of c, and then they are at most a sz(c,p)·sz(c,q)/P² fraction of all placements.

theorem Nibble.AX1.BoxPlace.slot_count_le_demand {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {c : κ} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) (hszP : ∀ (a : ZMod 3), sz c a ≤ P) (hP : 0 < P) (S T : ι) (i j : Fin P) {F : Finset (ZMod 3 → Finset (Fin P))} (hFsub : F ⊆ BoxCount.plc P (sz c)) (hF : ∀ A ∈ F, Sum.inl (S, T, i, j) ∈ placeEdge idx cl c A) : ∑ _A ∈ F, (↑(placeCard P sz c))⁻¹ ≤ boxDemandC cl sz c S T / ↑P ^ 2

The placements of c through a slot of (S,T) are a demand/P² fraction.

theorem Nibble.AX1.BoxPlace.slot_count_le_sz {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {c : κ} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) (hszP : ∀ (a : ZMod 3), sz c a ≤ P) (hP : 0 < P) {s₀ : ℕ} (hs : ∀ (a : ZMod 3), sz c a ≤ s₀) (S T : ι) (i j : Fin P) {F : Finset (ZMod 3 → Finset (Fin P))} (hFsub : F ⊆ BoxCount.plc P (sz c)) (hF : ∀ A ∈ F, Sum.inl (S, T, i, j) ∈ placeEdge idx cl c A) : ∑ _A ∈ F, (↑(placeCard P sz c))⁻¹ ≤ ↑s₀ ^ 2 / ↑P ^ 2

The same count is at most s₀²/P².

theorem Nibble.AX1.BoxPlace.two_slot_count_le {ι κ : Type} [DecidableEq ι] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {c : κ} (hidx : Function.Injective idx) (hcl : Function.Injective (cl c)) (hszP : ∀ (a : ZMod 3), sz c a ≤ P) (hP : 2 ≤ P) {s₀ : ℕ} (hs : ∀ (a : ZMod 3), sz c a ≤ s₀) {S T S' T' : ι} {i j i' j' : Fin P} (hne : (S, T, i, j) ≠ (S', T', i', j')) {F : Finset (ZMod 3 → Finset (Fin P))} (hFsub : F ⊆ BoxCount.plc P (sz c)) (hF1 : ∀ A ∈ F, Sum.inl (S, T, i, j) ∈ placeEdge idx cl c A) (hF2 : ∀ A ∈ F, Sum.inl (S', T', i', j') ∈ placeEdge idx cl c A) : ∑ _A ∈ F, (↑(placeCard P sz c))⁻¹ ≤ 18 * ↑s₀ / ↑P * (boxDemandC cl sz c S T / ↑P ^ 2)

Two slots pin a copy down in a third coordinate. This is the estimate that makes the codegrees of the placement hypergraph small, and it is where the small-box restriction enters.

The loads and the codegrees

theorem Nibble.AX1.BoxPlace.wLoad_inr {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (c : κ) : Slack.wLoad (placeFam P idx cl sz) (placeWt P sz) (Sum.inr c) = 1

The load of a token is exactly 1.

theorem Nibble.AX1.BoxPlace.wLoad_inl_of_not_lt {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) {S T : ι} (h : ¬idx S < idx T) (i j : Fin P) : Slack.wLoad (placeFam P idx cl sz) (placeWt P sz) (Sum.inl (S, T, i, j)) = 0

Only the slots oriented by idx are occupied.

theorem Nibble.AX1.BoxPlace.wLoad_inl_le {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (hP : 0 < P) (S T : ι) (i j : Fin P) : Slack.wLoad (placeFam P idx cl sz) (placeWt P sz) (Sum.inl (S, T, i, j)) ≤ boxDemand cl sz S T / ↑P ^ 2

The load of a slot is at most the normalised demand of its cluster pair.

theorem Nibble.AX1.BoxPlace.codeg_inr_inr {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {c c' : κ} (h : c ≠ c') : ∑ U ∈ {U ∈ placeFam P idx cl sz | Sum.inr c ∈ U} with Sum.inr c' ∈ U, placeWt P sz U = 0

Two tokens are never together in an edge.

theorem Nibble.AX1.BoxPlace.codeg_inl_inr_le {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (hP : 0 < P) {s₀ : ℕ} (hs : ∀ (c : κ) (a : ZMod 3), sz c a ≤ s₀) (c : κ) (S T : ι) (i j : Fin P) : ∑ U ∈ {U ∈ placeFam P idx cl sz | Sum.inl (S, T, i, j) ∈ U} with Sum.inr c ∈ U, placeWt P sz U ≤ 9 * ↑s₀ ^ 2 / ↑P ^ 2

The codegree of a slot and a token is at most 9 s₀²/P².

theorem Nibble.AX1.BoxPlace.codeg_inl_inl_le {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (hP : 2 ≤ P) {s₀ : ℕ} (hs : ∀ (c : κ) (a : ZMod 3), sz c a ≤ s₀) {S T S' T' : ι} {i j i' j' : Fin P} (hne : (S, T, i, j) ≠ (S', T', i', j')) : ∑ U ∈ {U ∈ placeFam P idx cl sz | Sum.inl (S, T, i, j) ∈ U} with Sum.inl (S', T', i', j') ∈ U, placeWt P sz U ≤ 18 * ↑s₀ / ↑P * (boxDemand cl sz S T / ↑P ^ 2)

The codegree of two slots is O(s₀/P) times the normalised demand: two placements sharing two slots are pinned down in one further coordinate. This is where the small-box restriction is used.

theorem Nibble.AX1.BoxPlace.codeg_le {ι κ : Type} [DecidableEq ι] [Fintype κ] [DecidableEq κ] {P : ℕ} {idx : ι → ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} (hidx : Function.Injective idx) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (hP : 2 ≤ P) {s₀ : ℕ} (hs : ∀ (c : κ) (a : ZMod 3), sz c a ≤ s₀) (hsP : s₀ ≤ P) (hdem : ∀ (S T : ι), S ≠ T → boxDemand cl sz S T ≤ ↑P ^ 2) (x z : PlaceVtx ι κ P) (hxz : x ≠ z) : ∑ U ∈ {U ∈ placeFam P idx cl sz | x ∈ U} with z ∈ U, placeWt P sz U ≤ 18 * ↑s₀ / ↑P

All weighted codegrees are O(s₀/P).

Weighted nibble for box placement

theorem Nibble.AX1.BoxPlace.card_copies_le {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] {P : ℕ} {cl : κ → ZMod 3 → ι} {sz : κ → ZMod 3 → ℕ} {ε : ℝ} (hε0 : 0 ≤ ε) (hcl : ∀ (c : κ), Function.Injective (cl c)) (hsz1 : ∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) (hdem : ∀ (S T : ι), S ≠ T → boxDemand cl sz S T ≤ (1 - ε) * ↑P ^ 2) : ↑(Fintype.card κ) ≤ ↑(Fintype.card ι) ^ 2 * ↑P ^ 2

There are not too many copies. Every copy demands at least one cell pair in the cluster pair of its first two clusters, so the number of copies is at most the total capacity.

def Nibble.AX1.BoxPlace.defaultAlloc {κ : Type} (P : ℕ) (sz : κ → ZMod 3 → ℕ) (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (c : κ) : ZMod 3 → Finset (Fin P)

The default allocation of a copy: an initial segment of the cells of the right size.

Equations

• Nibble.AX1.BoxPlace.defaultAlloc P sz hszP c a = (Finset.range (sz c a)).attachFin ⋯

theorem Nibble.AX1.BoxPlace.defaultAlloc_mem {κ : Type} {P : ℕ} {sz : κ → ZMod 3 → ℕ} (hszP : ∀ (c : κ) (a : ZMod 3), sz c a ≤ P) (c : κ) : defaultAlloc P sz hszP c ∈ BoxCount.plc P (sz c)

theorem Nibble.AX1.boxAllocationResidual_main (ε : ℝ) (hε : 0 < ε) (s₀ : ℕ) : ∃ (θ : ℝ), 0 < θ ∧ θ ≤ 1 ∧ ∀ (P : ℕ), 0 < P → ↑s₀ ≤ θ * ↑P → ∀ (ι κ : Type) [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : Fintype κ] [DecidableEq κ] (cl : κ → ZMod 3 → ι) (sz : κ → ZMod 3 → ℕ), (∀ (c : κ), Function.Injective (cl c)) → (∀ (c : κ) (a : ZMod 3), 1 ≤ sz c a) → (∀ (c : κ) (a : ZMod 3), sz c a ≤ s₀) → (∀ (S T : ι), S ≠ T → boxDemand cl sz S T ≤ (1 - ε) * ↑P ^ 2) → ∃ (bad : Finset κ) (I : κ → ZMod 3 → Finset (Fin P)), (∀ (c : κ) (a : ZMod 3), (I c a).card = sz c a) ∧ (∀ c ∉ bad, ∀ c' ∉ bad, 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')) ∧ ∑ c ∈ bad, ∑ a : ZMod 3, ↑(sz c a) * ↑(sz c (a + 1)) ≤ ε * ↑(Fintype.card ι) ^ 2 * ↑P ^ 2

The small-box allocation residual, for a fixed accuracy and a fixed box bound.

theorem Nibble.AX1.boxAllocationResidual_holds : BoxAllocationResidual

The small-box allocation residual.

Unconditional AX1

theorem Nibble.AX1.blockCoverResidualCoupled_holds : BlockCoverResidualCoupled

The coupled block-cover residual follows from the closed box-allocation theorem.

theorem Nibble.AX1.ax1Statement_holds : AX1Statement

The cover-side AX1 statement holds for every graph.

theorem Nibble.AX1.nibbleGapHyp_holds : NibbleGapHyp

The fractional–integral triangle-packing gap is uniformly o(n²).

Finite near-regular hypergraph rounding: basic statement

The public statement records the finite near-regular hypergraph rounding interface used by the nibble method. The underlying finite definitions are kept in the internal library.

@[reducible, inline]

abbrev LeanPool.AsymptoticTrianglePacking.NearRegularNibbleTheorem : Prop

The finite ceiling-carrying nibble interface for near-regular hypergraphs.

Equations

• LeanPool.AsymptoticTrianglePacking.NearRegularNibbleTheorem = LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheoremMostCeil

Nibble rounding infrastructure

This module makes the ceiling-carrying finite nibble interface available to the final assembly. The full development remains internal so that the public API is limited to stable theorem-level statements.

theorem LeanPool.AsymptoticTrianglePacking.nearRegularNibbleTheorem : NearRegularNibbleTheorem

The finite nibble-rounding theorem in the public interface.

Finite near-regular hypergraph rounding

Public entry point for the finite, ceiling-carrying near-regular hypergraph nibble theorem.

theorem LeanPool.AsymptoticTrianglePacking.trianglePackingGap (ε : ℝ) (hε : 0 < ε) : ∃ (n₀ : ℕ), ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → Nibble.YusterE.nu3star G - ↑(Nibble.YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The fractional and integral triangle-packing optima differ by o(n²), uniformly over finite graphs.

theorem LeanPool.AsymptoticTrianglePacking.triangleCoverPackingGap (ε : ℝ) (hε : 0 < ε) : ∃ (n₀ : ℕ), ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → Nibble.AX1.tau3Star G - ↑(Nibble.YusterE.nu3 G) ≤ ε * ↑(Fintype.card V) ^ 2

The fractional triangle-cover optimum exceeds the integral triangle-packing optimum by at most o(n²), uniformly over finite graphs.