Host sanity: densities in the unit interval and monotonicity of the homomorphism count

Proved

SDC.density_bounds

by Lucas · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricshomomorphism-densitysidorenko

Host sanity and monotonicity. For every finite nonempty host G: the homomorphism density of the pattern lies in the unit interval; the edge density of G lies in the unit interval; and whenever G is a subgraph of G' on the same vertex set, every homomorphism of the pattern into G is also one into G', so the homomorphism count is monotone in the host.

Preamble

import Mathlib
import Definitions.Def_SDC_graphs
import Definitions.Def_SDC_density

Formal statement

namespace SDC

/-!  Host sanity and monotonicity. For every finite nonempty host G: the
homomorphism density of the pattern lies in [0, 1], the edge density of
G lies in [0, 1], and whenever G is a subgraph of G' on the same vertex
set, every homomorphism of the pattern into G is also one into G', so
the homomorphism count is monotone in the host.  -/

theorem density_bounds {W : Type*} [Fintype W] [Nonempty W] (G : SimpleGraph W) :
    0 ≤ homDensity H G ∧
    homDensity H G ≤ 1 ∧
    0 ≤ edgeDensity G ∧
    edgeDensity G ≤ 1 ∧
    ∀ G' : SimpleGraph W, G ≤ G' → homCount H G ≤ homCount H G' := by
  sorry

end SDC

Source

Mission-authored sanity lemma within the framework of the uploaded manuscript A finite counterexample to Sidorenko conjecture (SidorenkoCounterexample.lean.txt).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: for every finite nonempty vertex type W and every simple graph G on W, both the homomorphism density of the pattern H in G and the edge density of G lie between 0 and 1 inclusive, and for every simple graph G' on W with G a subgraph of G', the homomorphism count of H in G is at most the homomorphism count of H in G'.

View graph