Energy gain from resolved polyad witnesses

Suppose a lower skeleton T refines S, and for each polyad in a finite family we have a large set of triples on which a color density differs substantially from its density on the whole polyad. If membership in every such witness set is constant on the polyads of T, then these witnesses force a quantitative polyad energy gain. Witnesses of relative size at least δ and density deviation at least δ force an energy gain of at least δ³ times the support mass of the family, normalized by the number of injective triples.

Witnesses may be unions of subpolyad supports, so this estimate applies to the tests in top regularity at any rank. Only their supports matter here; the construction of a bounded pair refinement resolving them is separate. The family may select a different top color for each polyad. No equitability, distinct-cell condition, or nonempty-host assumption is needed.

The argument is the conditional-expectation energy increment: on a resolved witness, the average fine density equals the actual density, and Cauchy–Schwarz turns its deviation into a lower bound for the fine variance. Disjoint coarse polyad supports allow these bounds to be summed without loss.

Main results

• TauCeti.Colored3Graph.sum_relativeDensity_ofTriple_on: conditional expectation on a resolved set of triples.
• TauCeti.Colored3Graph.card_mul_sq_relDensityOn_sub_le_sum: a resolved set's density deviation controls the sum of squared fine-density deviations.
• TauCeti.Colored3Graph.polyadEnergy_increment_of_witnesses: the quantitative energy gain for a finite family of resolved witnesses.

References

• V. Rödl and M. Schacht, Regular partitions of hypergraphs: regularity lemmas, Combin. Probab. Comput. 16 (2007), the index-increment argument.

theorem TauCeti.Colored3Graph.sum_relativeDensity_ofTriple_on {κ : Type u_1} {κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) {T : PairSkeleton3 κ₂' V} (c : κ) (U : Finset { x : Fin 3 → V // Function.Injective x }) (hU : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → (x ∈ U ↔ y ∈ U)) : ∑ x ∈ U, ↑(H.relativeDensity c (Polyad3.ofTriple T x)) = ↑U.card * ↑(H.relDensityOn c U)

On a set that is a union of fine polyad supports, the sum of the fine relative densities is the actual color count, expressed as the density times the size of the set.

theorem TauCeti.Colored3Graph.card_mul_sq_relDensityOn_sub_le_sum {κ : Type u_1} {κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) {T : PairSkeleton3 κ₂' V} (c : κ) (U : Finset { x : Fin 3 → V // Function.Injective x }) (hU : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → (x ∈ U ↔ y ∈ U)) (a : ℝ) : ↑U.card * (↑(H.relDensityOn c U) - a) ^ 2 ≤ ∑ x ∈ U, (↑(H.relativeDensity c (Polyad3.ofTriple T x)) - a) ^ 2

Cauchy–Schwarz on a resolved witness. The squared deviation of its density from any real number a, multiplied by its size, is bounded by the sum of the squared deviations of the fine densities from a. The empty witness is allowed.

theorem TauCeti.Colored3Graph.polyadEnergy_increment_of_witnesses {κ : Type u_1} {κ₂ : Type u_2} {κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) {S : PairSkeleton3 κ₂ V} {T : PairSkeleton3 κ₂' V} [Fintype κ] (h : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → Polyad3.ofTriple S x = Polyad3.ofTriple S y) (B : Finset (Polyad3 S)) (c : Polyad3 S → κ) (U : Polyad3 S → Finset { x : Fin 3 → V // Function.Injective x }) {δ : ℝ} (hsub : ∀ P ∈ B, U P ⊆ P.support) (hresolve : ∀ P ∈ B, ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → (x ∈ U P ↔ y ∈ U P)) (hsize : ∀ P ∈ B, δ * ↑P.support.card ≤ ↑(U P).card) (hdev : ∀ P ∈ B, δ ≤ |↑(H.relDensityOn (c P) (U P)) - ↑(H.relativeDensity (c P) P)|) : δ ^ 3 * ((∑ P ∈ B, ↑P.support.card) / ↑((Fintype.card V).descFactorial 3)) ≤ H.polyadEnergy T - H.polyadEnergy S

Resolved irregularity witnesses force an energy gain. For each coarse polyad in B, choose a color and a witness contained in its support. If every witness is a union of fine polyad supports, has at least a δ-fraction of its parent's size, and has density deviation at least δ, then the energy gain is at least δ³ times the normalized support mass of B. The refinement hypothesis concerns all polyads, while resolution is needed only for the chosen witnesses. In particular, they may be unions of rank-r subpolyad tests.