YusterFracUpper

theorem Nibble.YusterE.isFracPacking_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : IsFracPacking G fun (x : Finset (Finset V)) => 0

The all-zero weighting is a fractional packing.

theorem Nibble.YusterE.triangleHypergraphE_subset_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {T : Finset (Finset V)} (hT : T ∈ triangleHypergraphE G) : T ⊆ G.cliqueFinset 2

Each hyperedge of triangleHypergraphE G is a set of 2-cliques (edges).

theorem Nibble.YusterE.fracPacking_sum_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {w : Finset (Finset V) → ℝ} (hw : IsFracPacking G w) : ∑ T ∈ triangleHypergraphE G, w T ≤ ↑(G.cliqueFinset 2).card / 3

Per-packing bound. For any fractional packing w, the total weight is ≤ |E(G)|/3. Double counting: 3·∑_T w_T = ∑_T ∑_{e∈T} w_T = ∑_e ∑_{T∋e} w_T ≤ ∑_e 1 = |E(G)|.

theorem Nibble.YusterE.nu3star_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : nu3star G ≤ ↑(G.cliqueFinset 2).card / 3

Y6 (upper) — ν₃* ≤ |E(G)|/3. The fractional triangle-packing number is bounded by |E(G)|/3. Together with nu3_ge_nibble this bounds the integrality gap ν₃* − ν₃.