The sum-product formula: the pattern's homomorphism count as a sum of products of common-neighborhood sizes
ProvedSDC.hom_sum_productThe computational core. Because the pattern is the incidence graph of the triple system, a homomorphism from H to a host G is a map of points together with a map of triples, constrained only by the incidences: the image of a triple must be a common neighbor of the images of its three points. Summing over the point maps and multiplying the numbers of admissible images of the triples expresses the homomorphism count of the pattern as a sum over point maps of products of common-neighborhood sizes. This is the formula through which the inequality of the goal is evaluated on an explicit host.
import Mathlib import Definitions.Def_SDC_graphs import Definitions.Def_SDC_density
namespace SDC
open BigOperators
/-! The computational core. Because the pattern is the incidence graph of
the triple system, a homomorphism from H to a host G is a map of points
together with a map of triples, constrained only by the incidences: the
image of a triple must be a common neighbor of the images of its three
points. Summing over the point maps and multiplying the numbers of
admissible images of the triples expresses the homomorphism count of the
pattern as a sum over point maps of products of common-neighborhood
sizes. This is the formula through which the inequality of the goal is
evaluated on an explicit host. -/
theorem hom_sum_product {W : Type*} [Fintype W] (G : SimpleGraph W) :
homCount H G =
∑ φ : (Fin 13 → W), ∏ f : Fin 22,
(⋂ p ∈ faces f, G.neighborSet (φ p)).ncard := by
sorry
end SDC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every finite vertex type W and every simple graph G on W, the homomorphism count of the pattern H in G equals the sum over all functions from the 13 points to W of the product over the 22 triples of the ncard of the intersection of the neighbor sets of the images of the three points of the triple.