YusterNibbleApply #
Y5 (scaffold) — nibble ⇒ large triangle packing. Assuming NibbleTheorem, there is a
near-regularity tolerance μ > 0 such that, whenever the edge-type triangle hypergraph is
(1±μ)-nearly d-regular with codegree ≤ μd, it has a matching (edge-disjoint triangle
packing) of
size ≥ (1-β)·|E(G)|/3. Direct application of NibbleTheorem to triangleHypergraphSub G, using
card_EdgeV to turn Fintype.card (EdgeV G) into |E(G)| = |cliqueFinset 2|.
Y5 (majority) — nibble ⇒ large triangle packing, tolerating an exceptional edge set. The
NibbleTheoremMost version of nibble_gives_triangleSub_matching: assuming the majority interface,
there are tolerances μ, η > 0 such that whenever the edge-type triangle hypergraph is
NearlyRegularMost d μ η (near-d-regular outside an η-fraction of edges) with codegree ≤ μd, it
has an edge-disjoint triangle packing of size ≥ (1-β)·|E(G)|/3. This is the version the
Szemerédi+counting reconstruction (which yields NearlyRegularMost, not strict) feeds.
YusterSubBridge #
Sub ↦ E bridge. A matching of the edge-vertex-type triangle hypergraph lower-bounds nu3:
mapping each hyperedge T by the subtype embedding EdgeV G ↪ Finset V (T ↦ T.map emb) turns a
matching of triangleHypergraphSub G into a matching of triangleHypergraphE G of the same
cardinality (the embedding is injective — preserves card and disjointness — and recovers the
original
2-subsets of each triangle since they are all 2-cliques). Then nu3_ge.
ν₃ lower bound from the nibble. Assuming NibbleTheorem and the Y3
near-regularity/codegree
interface on triangleHypergraphSub G, the integral triangle-packing number satisfies
(1-β)·|E(G)|/3 ≤ ν₃ G. Combines Y5 (nibble_gives_triangleSub_matching) with the Sub ↦
nu3 bridge.
This is the quantitative half of Y6 (the other half is ν₃* ≤ an upper bound).
Reduction to duality and rounding #
PaperIII edgesIn: edges of G contained in a vertex set t.
Equations
- Nibble.AX1.edgesIn G t = {e ∈ G.edgeFinset | ∀ v ∈ e, v ∈ t}
Instances For
PaperIII IsFracCover: nonneg edge weights, total ≥ 1 inside each triangle.
Equations
- Nibble.AX1.IsFracCover G y = ((∀ (e : Sym2 V), 0 ≤ y e) ∧ ∀ t ∈ G.cliqueFinset 3, 1 ≤ ∑ e ∈ Nibble.AX1.edgesIn G t, y e)
Instances For
PaperIII τ₃*: the fractional triangle-cover optimum (LP value).
Equations
- Nibble.AX1.tau3Star G = sInf {x : ℝ | ∃ (y : Sym2 V → ℝ), Nibble.AX1.IsFracCover G y ∧ x = ∑ e ∈ G.edgeFinset, y e}
Instances For
AX1 statement (PaperIII Layer X, verbatim): the fractional–integral triangle-packing gap is
o(n²), uniformly over graphs, read cover-side (τ₃* − ν₃).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The strong-duality obligation (Aristotle core b3ee717f): τ₃* ≤ ν₃* for every graph
(the reverse of the proven weak duality; together they give τ₃* = ν₃*).
Equations
- Nibble.AX1.StrongDualityHyp = ∀ {V : Type} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], Nibble.AX1.tau3Star G ≤ Nibble.YusterE.nu3star G
Instances For
The unconditional nibble-gap obligation (NibbleTheoremMost + second-stage
near-regularity
discharged
for all large graphs): ν₃* − ν₃ ≤ ε n² uniformly.
Equations
- One or more equations did not get rendered due to their size.
Instances For
AX1 REDUCTION. AX1 follows from the two remaining obligations: cover-side strong duality
(τ₃* ≤ ν₃*) and the unconditional nibble packing gap (ν₃* − ν₃ ≤ ε n²). The definitional bridges
Nibble.{nu3,nu3star} ↔ PaperIII.{nu3,nu3Star} (already proven) make these the SAME ν₃, ν₃*
as AX1's.
Finite packing-cover LP duality #
A fractional PACKING: nonneg object weights, total ≤ 1 across each constraint.
Equations
Instances For
Packing optimum (LP value).
Equations
Instances For
THE ATOM — finite LP strong duality (packing = cover). Machinery-free: pure finite LP. This is the only genuinely hard step; everything downstream is instantiation.
Strong duality for triangle packing and covering #
Object type: the triangles of G.
Equations
- Nibble.AX1.Tri G = ↥(G.cliqueFinset 3)
Instances For
Constraint type: the edges of G.
Equations
- Nibble.AX1.Edg G = ↥G.edgeFinset
Instances For
Incidence: the edges contained in a triangle.
Equations
- Nibble.AX1.triInc G t = {e : Nibble.AX1.Edg G | ↑e ∈ Nibble.AX1.edgesIn G ↑t}
Instances For
Every triangle has an incident graph edge.
Bridge 1 (cover side). The abstract cover optimum over the triangle–edge incidence equals
τ₃*.
Bridge 2 (packing side). The abstract packing optimum over the triangle–edge
incidence equals
ν₃*.
StrongDualityHyp — the instantiation. τ₃* ≤ ν₃* follows from the abstract
finite LP strong
duality applied to the triangle–edge incidence, via the two value bridges.
StrongDualityHyp DISCHARGED — the cover-side strong-duality obligation of
the AX1 chain is now a theorem (via the abstract finite LP duality + the
triangle–edge encoding bridges). One of the three AX1
obligations is closed, independently of the nibble.
Weak duality in the reverse direction for the triangle–edge incidence.
The cover-side AX1 statement yields the unconditional packing-gap formulation.
The remaining AX1 obligation is precisely the unconditional packing gap.
YusterGap #
Y6 capstone — integrality gap bound. Assuming NibbleTheorem and the Y3 near-regularity /
codegree interface on triangleHypergraphSub G, the gap between the fractional and integral
triangle
packing numbers is at most β·|E(G)|/3. Combining nu3_ge_nibble and nu3star_le. As β → 0 this
is o(n²) — AX1.
YusterAX1 #
Edge count bound |E(G)| ≤ |V(G)|². Each edge is a 2-subset of the vertex set, so
|E| ≤ C(|V|,2) ≤ |V|².
AX1-form gap. Assuming NibbleTheorem and the edge-based Y3 interface, the
integrality gap is
≤ ε·|V(G)|² — the shape AX1 states. Takes β = 3ε in nu3star_sub_nu3_le (so β·|E|/3 = ε·|E|) and
bounds |E| ≤ |V|².
YusterMost #
Majority ν₃ lower bound. NibbleTheoremMost + the Y3-majority interface ⇒ ν₃ ≥ (1-β)|E|/3.
Majority integrality-gap bound ν₃* − ν₃ ≤ β|E|/3.
Majority AX1-form gap ν₃* − ν₃ ≤ ε|V|².
NibbleGapReduction #
Uniform nibble gap: tolerances μ, η depending only on ε (NOT on G) such that
every graph that is near-d-regular (outside η-fraction) with bounded codegree has
ν₃* − ν₃ ≤ ε n². This is the
G-uniform form of the proven per-graph nu3star_sub_nu3_le_eps_most.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Near-regularity obligation (the second-stage core): for tolerances μ, η, every
sufficiently large graph admits a near-regularity witness d with the free codegree bound.
This is exactly what a Szemerédi/Haxell–Rödl regularization must supply.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sized near-regularity obligation. The corrected Freedman route also needs the triangle
hypergraph vertex count (|E(G)|) to be polynomially bounded by the regular degree scale d.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dense-regime sized obligation in the natural graph-scale form: the base vertex count is linearly controlled by the regular degree scale.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triangle-hypergraph vertex count is quadratically controlled by any linear base-size bound
|V(G)| ≤ L d.
A linear base-size second-stage obligation implies the polynomial hypergraph-size obligation consumed by the sized nibble interface.
Linear size control for every positive constant implies the exact sized obligation for every
positive K, by taking L = sqrt K.
NibbleGapHyp reduction. The unconditional packing gap follows from the
G-uniform nibble gap plus the near-regularity obligation for its tolerances.
Bottoms the AX1 chain out at NibbleTheoremMost
(via UniformNibbleGap) and the second-stage regularization (via NearRegObligation).
NibbleGapHyp directly from NibbleTheoremMost. Extracts the uniform tolerances
μ, η from the nibble interface once (at r = 3, β = 3ε), consumes the
near-regularity obligation, and inlines the
packing-gap arithmetic (ν₃* ≤ |E|/3 and matching ≥ (1-3ε)|E|/3 ≤ ν₃, so ν₃*−ν₃ ≤ ε|E| ≤ ε n²).
This bottoms the AX1 dependency chain out at exactly NibbleTheoremMost plus
the second-stage regularization.
NibbleGapHyp from the corrected ceiling-aware nibble theorem. This is the same accounting as
nibbleGap_of_nibbleTheorem, but it keeps the second-stage global-degree ceiling supplied by
NearRegObligation and passes it into the nibble interface.
NibbleGapHyp from the sized corrected nibble theorem. This is the target shape for the Freedman parameter route: all probabilistic plumbing is abstract, while the triangle-specific regularization supplies both the global ceiling and the size-vs-degree bound.
Version of nibbleGap_of_nibbleTheoremCeilSized consuming the dense-regime linear size
obligation.
The full AX1 reduction. AX1 sorry-free follows from the three irreducible obligations.
The full AX1 reduction, ceiling-aware form. This is the corrected target for the Freedman
route: the second-stage regularization supplies the global degree ceiling consumed by
NibbleTheoremMostCeil.
The full AX1 reduction, sized ceiling-aware form. This is the version aligned with the Freedman parameter atom after exposing the necessary size control.
Sized Freedman AX1 reduction consuming the linear dense-regime regularity condition.
TightNibble #
The one-round covering oracle from the sharp round. Running the tight-band schedule
Nibble.TightParams r β gives, for every majority near-regular input with a global degree ceiling
and low codegree, a HasRoundOracle H (γ/(16r)) β.
NibbleTheoremMostCeil, unconditionally.
NibbleTheoremMostCeilSized, unconditionally. The size hypothesis
|V| ≤ K d² is not needed by the tight-band route, so it is simply discarded.
NibbleTheorem, unconditionally.
The nibble gap hypothesis, via Nibble.NibbleGapReduction.
AX1, from strong duality and the sized near-regularity obligation.
Legacy interfaces #
The schedule now supplies the sharp round itself (Nibble.sharpRoundHyp_of_two_gamma_le_eps, whose
regime 2γ ≤ ε is exactly the schedule's own ε = 4((r−1)/r)γ), so Nibble.SharpRoundHyp is no
longer an input. The following wrappers keep the earlier _of_sharpRound interfaces available.
The one-round covering oracle from the sharp round.
NibbleTheoremMostCeil from the sharp round.
NibbleTheoremMostCeilSized from the sharp round.
NibbleTheorem from the sharp round.
The nibble gap hypothesis from the sharp round, via Nibble.NibbleGapReduction.
AX1 from the sharp round, together with strong duality and the sized near-regularity obligation.
YusterSubDegree #
|triangleHypergraphSub| = #triangles. The powerset-subtype map is injective on 3-cliques
(distinct triangles have distinct edge-sets), so the image has the same cardinality.
Degree-sum (handshake) for the edge-based triangle hypergraph. As triangleHypergraphSub G
is 3-uniform, ∑_{E} deg_E = 3·|triangleHypergraphSub| = 3·#triangles. The average edge
triangle-degree is 3·#triangles / |E(G)|.
YusterSubDegreeChar #
The number of triangles containing edge E equals the number of common neighbours c of E's
endpoints (those c ∉ E.val with insert c E.val a triangle).
Second-stage bridge, graph form. The hypergraph-degree of edge E in
triangleHypergraphSub G equals the number of common neighbours of its endpoints.
Second-stage mean codegree. Summing the per-edge codegree (common-neighbour count)
over all edges gives
3·#triangles, so the average edge codegree is 3·#triangles / |E(G)| — the target d for the
second-stage near-regularity window.
YusterSubRegular #
Codegree side (trivial). The edge-based triangle hypergraph has hypergraph-codegree ≤ 1, so it
is CodegreeBounded C for any C ≥ 1 — in particular C = μd once μd ≥ 1.
Majority near-regularity (packaging). Given a per-edge degree window on all but an
exceptional
set Exc of size ≤ η|E(G)|, the edge-based triangle hypergraph is NearlyRegularMost d μ η. The
per-edge bounds and the exceptional count are supplied by the edge counting (edge-counting
substep).
DenseNearRegular #
The triangle-hypergraph degree of an edge {u,v} is the number of common neighbours.
second-stage ceiling (global upper bound). Every edge lies in at most |V| triangles.
Second-stage floor (from a global min-degree bound). If every vertex of G has degree
≥ D, then every edge lies in at least 2D − |V| triangles by inclusion–exclusion.
Second-stage global near-regularity window (packaged). With a global min-degree D
satisfying |V| ≤ 2D
(dense regime), every edge's triangle-degree lies in the window [(1−μ)d, (1+μ)d] provided
the window
covers [2D−|V|, |V|]. This is the global (no exceptional set) near-regularity the corrected nibble
consumes; at δ ≥ (9/10+ε)|V|, taking D = (9/10+ε)|V|, d = (9/10)|V|, μ = 1/9 satisfies the
hypotheses.
Dense-regime package for the corrected nibble input. A global degree window on every graph edge,
the trivial edge-hypergraph codegree bound, and a linear base-size estimate assemble the exact local
data required by NearRegObligationLinearSized.
Dense-regime package specialized to a minimum-degree floor D: the inclusion-exclusion window
triangleSub_degree_window feeds the local linear-sized corrected nibble data.
Tight.DenseRegDischarge #
Dense near-regularity, concrete window. For a graph whose minimum degree D satisfies
9n ≤ 10D (i.e. δ(G) ≥ (9/10)n) and n ≥ 5, the triangle hypergraph is nearly d-regular with
d = n, μ = 1/5, EMPTY exceptional set, codegree ≤ μd, global ceiling ≤ (1+μ)d, and the
linear
size bound n ≤ 1·d. This is exactly the local data of NearRegObligationLinearSized with
μ = 1/5, η = 0, L = 1, d = n.
DenseGapAX1 #
Packing-gap accounting. A matching of the triangle hypergraph of size at least
(1 − 3ε)|E(G)|/3 forces ν₃* − ν₃ ≤ ε|V|², using ν₃* ≤ |E|/3 and |E| ≤ |V|².
The dense branch, unconditionally. For every ε > 0 there is a density threshold θ < 1
and a size threshold n₀ such that every graph on at least n₀ vertices with minimum degree at
least θ|V| satisfies ν₃* − ν₃ ≤ ε|V|².
At minimum degree θ|V| = (1 − μ/2)|V| the common neighbourhood of every edge has size in
[(1−μ)|V|, |V|], so the triangle hypergraph is near-|V|-regular with an empty exceptional set,
bounded codegree and the global degree ceiling — precisely the hypotheses of the unconditional
nibble theorem Nibble.nibbleTheoremMostCeil_holds.
Every fractional triangle packing has total weight at most the number of triangles: each single
weight is at most 1 by its own edge constraint.
ν₃* is at most the number of triangles.
The triangle-poor branch, unconditionally. If G has at most ε|V|² triangles then the
packing gap is at most ε|V|², because ν₃* ≤ #triangles and ν₃ ≥ 0.
The residual. The packing gap for the graphs that neither branch above covers: those that
fail the density threshold (some vertex has degree below θ|V|) and are triangle-rich (more than
ε|V|² triangles). Stated for every threshold θ ∈ (0,1) because the dense branch's threshold
depends on ε.
This is a true statement (a special case of the Haxell–Rödl theorem), unlike the previous blocker
NearRegObligationSized, which asserts near-regularity of the triangle hypergraph of an arbitrary
graph and is false.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The reduction. NibbleGapHyp follows from the residual alone: the dense case is discharged
unconditionally by nibbleGap_dense and the triangle-poor case by nibbleGap_fewTriangles.
AX1 from the residual. Combines the reduction with the proved strong-duality input
Nibble.AX1.strongDualityHyp_holds.
CoreGapAX1 #
Monotonicity of the packing numbers under edge deletion #
The triangle hypergraph is monotone in the graph.
ν₃ is monotone. Every edge-disjoint triangle packing of a spanning subgraph is one of the
graph itself.
A triangle of G that is not a triangle of the spanning subgraph G' has one of its three
edges among the deleted ones.
ν₃* is stable under edge deletion. Deleting a set D of edges decreases the fractional
triangle packing number by at most |D|: the weight carried by the triangles that are destroyed is
at most the total edge load of D, which is at most |D|.
The packing gap is stable under edge deletion.
The low-degree core #
G with every edge at a vertex of K deleted.
Equations
Instances For
Isolating one more vertex destroys at most deg v edges.
The support of G: its non-isolated vertices.
Equations
- Nibble.AX1.posDeg G = {x : V | 0 < G.degree x}
Instances For
The core. Iteratively isolating the vertices of positive degree below t produces a
spanning subgraph in which every vertex is isolated or has degree at least t, at a cost of at
most t·m deleted edges, where m bounds the number of non-isolated vertices.
The core, unpacked. Every graph has a spanning subgraph in which every vertex is isolated
or of degree at least t, obtained by deleting at most t·|V| edges.
The dense branch in the presence of isolated vertices #
Support ceiling. Every edge lies in at most |support| triangles.
Support floor. If every non-isolated vertex has degree at least D, then every edge lies
in at least 2D − |support| triangles: the two neighbourhoods live inside the support.
A graph with no edges has zero packing gap.
The dense branch, tolerating isolated vertices. For every ε > 0 there is a density
threshold θ < 1 and a size threshold n₀ such that every graph on at least n₀ vertices all of
whose vertices are isolated or of degree at least θ|V| satisfies ν₃* − ν₃ ≤ ε|V|².
The triangle hypergraph lives on the edges, so the isolated vertices are invisible to it: run the
nibble at the scale d = |support|, at which the hypergraph is near-d-regular with an empty
exceptional set.
A new unconditional branch: graphs with a dense core. For every ε > 0 there are θ < 1
and n₀ such that every large graph which becomes (isolated-or-)θ|V|-dense after deleting at most
(ε/4)|V|² edges has packing gap at most ε|V|².
This strictly extends Nibble.AX1.nibbleGap_dense (take G' = G, no deletion): the graph
itself may
have arbitrarily many vertices of arbitrarily small positive degree, as long as the edges at
them are
few.
The residual #
The core packing-gap statement at parameters (ε, δ). The gap ν₃* − ν₃ ≤ ε|V|² for large
graphs in which every vertex is isolated or has degree at least δ|V|, and whose fractional packing
number exceeds ε|V|² (otherwise the conclusion is immediate from ν₃ ≥ 0).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residual. The core packing gap at every pair of parameters.
Equations
- Nibble.AX1.CoreGapResidual = ∀ (ε : ℝ), 0 < ε → ∀ (δ : ℝ), 0 < δ → Nibble.AX1.CoreGapAt ε δ
Instances For
CoreGapAt is unconditionally true near the top of the density range. For every ε > 0
there is θ < 1 with CoreGapAt ε θ — hence, by CoreGapAt.mono_delta, CoreGapAt ε δ for every
δ ≥ θ. This is the satisfiability witness for the residual: it is a nonempty, non-circular family
of true statements, proved from the nibble, not from the target.
The reduction #
The reduction. NibbleGapResidual follows from the core residual: delete the edges at all
vertices of positive degree below (ε/4)|V| — this costs at most (ε/4)|V|² edges, hence at most
that much of the packing gap — and apply the core residual to the resulting graph.
NibbleGapHyp from the core residual.
AX1 from the core residual, combining with the proved strongDualityHyp_holds.
The Haxell–Rödl packing gap for triangle hypergraphs: ν₃*(G) − ν₃(G) = o(|V|²) for every
graph. This is the published theorem the whole AX1 chain is an instance of; it is recorded here
only to certify that the residual below it is genuinely true, never used as an input to anything
proved.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residual is a special case of Haxell–Rödl, hence true and not refutable.
The converse reduction. NibbleGapResidual implies the core residual as well (the dense
instances being supplied by nibbleGap_denseCore), so the reformulation is lossless: nothing has
been strengthened, and the two residuals are equivalent.