CellBoxAllocation

def Nibble.AX1.BoxCompat {P : ℕ} (I I' J J' : Finset (Fin P)) : Prop

Compatibility of two boxes in the grid of one cluster pair: the two rectangles I ×ˢ J and I' ×ˢ J' are disjoint exactly when the boxes are disjoint in one of the two clusters.

Equations

• Nibble.AX1.BoxCompat I I' J J' = (Disjoint I I' ∨ Disjoint J J')

theorem Nibble.AX1.boxCompat_iff_disjoint_product {P : ℕ} (I I' J J' : Finset (Fin P)) (_hI : I.Nonempty) (_hI' : I'.Nonempty) (_hJ : J.Nonempty) (_hJ' : J'.Nonempty) : BoxCompat I I' J J' ↔ Disjoint (I ×ˢ J) (I' ×ˢ J')

theorem Nibble.AX1.box_allocation_infeasible {P : ℕ} (I I' J J' : Finset (Fin P)) (hI : I.card = P) (hJ : J.card = 1) (hI' : I'.card = 1) (hJ' : J'.card = P) : ¬BoxCompat I I' J J'

The box allocation is infeasible at general densities. A P × 1 box and a 1 × P box in the same cluster-pair grid — the shapes forced by two cluster triples through the pair whose two other densities are opposite extremes — cannot be placed compatibly, although their total area 2·P is a 2/P fraction of the capacity P².

Axiom check

BoxAllocationSpec

def Nibble.AX1.boxDemand {ι : Type u_1} {κ : Type u_2} [Fintype κ] [DecidableEq ι] (cl : κ → ZMod 3 → ι) (sz : κ → ZMod 3 → ℕ) (S T : ι) : ℝ

The area demanded in the ordered cluster pair (S, T): every copy through both clusters contributes the product of its two prescribed sizes there.

Equations

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

def Nibble.AX1.BoxAllocationResidual : Prop

The small-box allocation residual. For every accuracy ε and every box bound s₀ there is a smallness threshold θ such that, whenever the prescribed sizes are at most s₀ ≤ θ·P and the demand of every cluster pair is at most (1 - ε)·P², all copies can be given cell sets of the prescribed sizes, three-way coherent by construction, so that any two copies sharing a cluster pair occupy disjoint rectangles of the cell grid of that pair — apart from a set bad of copies of total area at most ε·(#clusters)²·P².

The threshold θ is allowed to depend on the box bound s₀ as well as on ε. This is what the reduction of Nibble.CoarseCellCoupled supplies (there s₀ = ⌈K/δ⌉ is fixed by the accuracy of the block-cover residual, while the number P of cells per cluster is driven to infinity afterwards), and it is what a nibble proof needs: the placement hypergraph has uniformity of order s₀², and the codegree threshold of Nibble.fracNibbleWeighted_nearPerfect degrades with the uniformity, so θ cannot be chosen before s₀ is known.

Equations

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