CoreGapBlockCover

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.BlockCoverResidual : Prop

The deterministic block-allocation residual. At every choice of accuracy ε, density threshold δ, relative block size α ≤ δ/2, scale floor T₀ and regularity scale ε₁, all large regularity-reduced graphs carry a family of block sub-triples with pairwise disjoint vertex-pair rectangles whose edges recover the fractional triangle-packing optimum up to ε|V|².

The bound α ≤ δ/2 on the relative size of the blocks is not cosmetic, it is forced: the sizes #A ≈ τ·d(W,X), #B ≈ τ·d(U,X), #C ≈ τ·d(U,W) of Nibble.AX1.IsGridSubTriple are proportional to the three cluster densities, and A ⊆ U etc., so all three of #A/#U, #B/#W, #C/#X can be at least α only when the three densities are within a factor 1/α of each other. Demanding a constant α would therefore make the statement false: a graph all of whose good cluster triples have density profile (1, 1/10, 1/10) — three groups of clusters, dense across the first two, sparse to the third — admits no sub-triple at all at α = 1/4, while its reduced graph has ν₃* of order |V|². Since the densities are at least δ, α = δ/2 is the natural scale, and that is the value at which Nibble.AX1.subTripleDesignLocalResidual_of_blockCover uses the residual.

Equations

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

theorem Nibble.AX1.subTripleDesignLocalResidual_of_blockCover (h : BlockCoverResidual) : SubTripleDesignLocalResidual

The reduction: the deterministic block-allocation residual gives the local design residual.

All the analytic content of the design is discharged here: uniformity of the blocks (Nibble.AX1.isUniform_subblock), their densities (Nibble.AX1.edgeDensity_sub_lt_of_isUniform), the transfer to the reduced graph (Nibble.AX1.isUniform_regularityReduced), the six scale windows (Nibble.AX1.scale_window), the edge counts (Nibble.AX1.three_edgeDensity_mul_le_tripleGraph_edges), the pruning budget and the ν₃* bookkeeping (Nibble.AX1.sum_area_le_of_rect_disjoint).

theorem Nibble.AX1.ax1_of_blockCover (h : BlockCoverResidual) : AX1Statement

AX1 from the deterministic block-allocation residual.

The residual at a fine relative block size

Nibble.AX1.BlockCoverResidual above is stated at every relative block size α ≤ δ / 2, but the reduction only ever uses it at the one value α = δ / 2 with a density threshold δ that the reduction itself chooses, and which is free to be small compared with the accuracy ε. Recording that coupling is not a cosmetic change: at α comparable with δ and δ comparable with 1 the statement is false — the blocks are then forced to occupy a constant fraction of their cluster, so only boundedly many rectangles fit into a cluster pair, and the resulting quantisation error is a fixed positive multiple of |V| ^ 2. This is proved in Nibble.CoreGapBlockCoverRefute (Nibble.AX1.not_blockCoverResidual), with the explicit witness δ = 1, α = 1/2, ε₁ = 1, ε = 1/1000 and the complete graph split into five equal clusters.

Nibble.AX1.BlockCoverResidualFine is the same statement carrying the two side conditions the reduction actually supplies, δ ≤ ε and α ≤ ε ^ 2; it is implied by BlockCoverResidual (Nibble.AX1.blockCoverResidualFine_of_blockCover) and it still yields AX1 (Nibble.AX1.ax1_of_blockCoverFine). Both conditions are exactly what a construction needs: δ ≤ ε lets the cluster triples of density below the threshold be discarded at a cost of at most ε|V| ^ 2, and α ≤ ε ^ 2 makes the blocks small compared with their clusters, which is what turns the rounding of a fractional cluster packing to the quantised block sizes into an O(ε|V|^2) error.

def Nibble.AX1.BlockCoverResidualFine : Prop

The deterministic block-allocation residual at a fine relative block size. Same as Nibble.AX1.BlockCoverResidual, but only for the parameter range the reduction uses: the density threshold δ is below the accuracy ε, and the relative block size α is below ε ^ 2.

Equations

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

theorem Nibble.AX1.blockCoverResidualFine_of_blockCover (h : BlockCoverResidual) : BlockCoverResidualFine

The fine residual is a special case of the full one: it is the same statement under two extra hypotheses.

theorem Nibble.AX1.subTripleDesignLocalResidual_of_blockCoverFine (h : BlockCoverResidualFine) : SubTripleDesignLocalResidual

The reduction at the fine parameter range. Identical to Nibble.AX1.subTripleDesignLocalResidual_of_blockCover except that the density threshold is chosen as δ = (min 1 ε) ^ 2 / 8, which makes the two extra hypotheses of Nibble.AX1.BlockCoverResidualFine available at the point of use.

theorem Nibble.AX1.ax1_of_blockCoverFine (h : BlockCoverResidualFine) : AX1Statement

AX1 from the deterministic block-allocation residual at fine relative block size.

What is left in Nibble.AX1.BlockCoverResidual, and what it is not

The residual is now purely a statement about placing rectangles, and the accounting inside it is exact. Writing p = d(U,W), q = d(U,X), r = d(W,X) for the three cluster densities of the triple carrying the i-th sub-triple, the scale-equalisation sizes #A ≈ τr, #B ≈ τq, #C ≈ τp of Nibble.AX1.IsGridSubTriple make the three terms of the covering clause equal:

p·#A·#B = q·#A·#C = r·#B·#C = τ²·p·q·r,

so each sub-triple contributes exactly τ²pqr to (∑ᵢ covᵢ)/3, while the rectangles it occupies in the three cluster pairs have areas τ²qr, τ²pr, τ²pq. Summing the disjointness constraint over the cluster triples through one pair (U, W) therefore reads

∑_X (number of sub-triples on (U,W,X)) · τ²·d(U,X)·d(W,X) ≤ #U·#W,

i.e. exactly the capacity constraint ∑_X z_{UWX} ≤ e(U,W) of the fractional triangle packing LP of the weighted cluster graph, with z_{UWX} the value contributed by that cluster triple. And on the LP side a fractional triangle packing of the reduced graph respects exactly those capacities: Nibble.AX1.sum_fracPacking_cluster_pair_le (Nibble.CoreGapClusterCapacity) bounds the weight it puts on the triangles using a U–W edge by e(U, W). (That the aggregated weights are an optimal LP solution, and hence that the LP optimum bounds ν₃*, is the informal reading of that constraint; only the per-pair constraint itself is formalised.) In other words, Nibble.AX1.BlockCoverResidual is precisely the statement that an (almost) optimal solution of that cluster LP can be realised by an edge-disjoint family of block rectangles: the fractional-to-integral step in a blow-up.

Three things about the shape of that residual are settled, and none of them can be traded away.

• The ν₃* clause cannot be replaced by "cover all but ε|V|² of the triangle-carrying edges". That stronger covering criterion is available (Nibble.AX1.hasNearRegularFamily_of_cover) but is in general unsatisfiable: as explained at the end of Nibble.CoreGapRegularCover, a cluster triple with densities 1, 1/10, 1/10 can have only about 3/10 of its edges covered by near-regular classes, while every one of its edges lies in a triangle.
• The global exceptional-edge rate of Nibble.AX1.SubTripleDesignResidual cannot be met by any construction whose sub-triples live inside clusters — see the head of Nibble.CoreGapGridLocalResidual — which is why the route here goes through Nibble.AX1.SubTripleDesignLocalResidual.
• Allocating to each cluster triple a private piece of each cluster (so that rectangles of different triples are disjoint because their blocks already are) is far too lossy. With m clusters of size N and all densities 1, the LP value is ≈ m²N²/6, whereas maximising ∑_T g_T²τ² under the per-cluster constraints ∑_{T ∋ U} g_T τ ≤ N — there are ≈ m²/2 triples through each cluster — gives only ≈ 2N²/(3m), short by a factor ≈ m³. Blocks must therefore be reused by many cluster triples, disjointness coming from the other coordinate of the rectangle.

That is what the line design of Nibble.GridLineDesign is for. Indexing the blocks of each cluster by ZMod q, the line L(a,b) = {(j, j+a, j+b) : j} is a family of q sub-triples whose three projections are the diagonal a of (U,W), the diagonal b of (U,X) and the diagonal b-a of (W,X) (Nibble.AX1.lineTriple_UW_unique, Nibble.AX1.lineTriple_UX_unique, Nibble.AX1.lineTriple_WX_unique); the q diagonals of a pair partition its q² block pairs (Nibble.AX1.diagIndex_bijective, the partial form of Nibble.AX1.gridUW_bijective); and two cluster triples through the same pair that receive disjoint sets of diagonals never collide (Nibble.AX1.lineTriple_pair_disjoint), which is where Nibble.AX1.balanced_bucket_le allocates.

The simultaneous consistency of those allocations — the diagonals handed to a cluster triple in its three pairs have to be the three projections of one family of lines, at the same time for every pair of the cluster graph — is now settled, in closed form and deterministically, by Nibble.GridTripleDesign and Nibble.GridTripleDesignRect. Indexing both the clusters and the blocks of each cluster by a prime field ZMod q, give the cluster triple of vertex sum s the quadratic shift triShift s v = v ^ 2 - v * s, so that its j-th sub-triple occupies the block j + triShift s v of the cluster v. In the pair {a, b} this is the diagonal of offset (b - a) * (a + b - s) (Nibble.AX1.triShift_diff), an injective function of s for a ≠ b; two distinct cluster triples through a common pair have different sums, so they never share a block pair, in all three of their pairs at once (Nibble.AX1.triPairSet_disjoint, Nibble.AX1.triCells_inter_subsingleton), and the resulting vertex-pair rectangles are pairwise disjoint (Nibble.AX1.tripleRect_disjoint_of_design). A cluster pair is filled by exactly q · (number of cluster triples through it) of its q ^ 2 block pairs (Nibble.AX1.card_triPairSet_biUnion), so the allocation is feasible whenever q is at least the number of clusters.

What is still missing is therefore not the consistency of the allocation but the quantitative realisation of the LP optimum under the two side conditions the residual carries.

• Sizes. Nibble.AX1.IsGridSubTriple prescribes the three part sizes #A ≈ τ·r, #B ≈ τ·q, #C ≈ τ·p from a single global scale τ, so the rectangles of the family are not free: their side lengths are dictated by the cluster densities, and the fractional solution has to be rounded to those quantised sizes.
• Relative size. The same predicate asks each part to be at least an α fraction of its cluster (this is what makes the parts inherit ε₁/(8α)-uniformity), while α has to stay large compared with ε₁, and the number of clusters is at least 4/ε₁. Hence at most 1/α² rectangles fit in a cluster pair, far fewer than the ≈ m cluster triples through it: the family must be sparse, using few and large sub-triples rather than a fine grid. In that regime the design above is used with a small number q of blocks per cluster, and choosing which cluster triples carry the LP mass becomes an approximate weighted triangle decomposition of the cluster graph — for the all-densities-1 reduced graph it is exactly an approximate Steiner triple system on the clusters, each cluster pair being used once at full size.

That decomposition step, and the rounding of the LP solution to the quantised sizes, is what Nibble.AX1.BlockCoverResidual still asserts.