Clearing denominators: the violation as a natural-number inequality
ProvedSDC.witness_inequalityClearing denominators. For a finite nonempty host G with m vertices and e edges, the homomorphism density of the pattern is below the 66th power of the edge density exactly when the natural-number inequality homCount H G * m^132 < (2e)^66 * m^35 holds. The violation is therefore a decidable arithmetic statement about finite data, with no real division left.
import Mathlib import Definitions.Def_SDC_graphs import Definitions.Def_SDC_density
namespace SDC
/-! Clearing denominators. For a finite nonempty host G with m vertices
and e edges, the homomorphism density of the pattern is below the 66th
power of the edge density exactly when the natural-number inequality
homCount H G * m ^ 132 < (2 * e) ^ 66 * m ^ 35 holds. The violation is
therefore a decidable arithmetic statement about finite data, with no
real division left. -/
theorem witness_inequality {W : Type*} [Fintype W] [Nonempty W] (G : SimpleGraph W) :
homDensity H G < (edgeDensity G) ^ 66 ↔
homCount H G * (Fintype.card W) ^ 132 <
(2 * edgeCard G) ^ 66 * (Fintype.card W) ^ 35 := by
sorry
end SDC
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, the homomorphism density of the pattern H in G is strictly below the 66th power of the edge density of G if and only if the homomorphism count of H in G times the cardinality of W to the 132nd power is strictly less than twice the edge count of G to the 66th power times the cardinality of W to the 35th power.