The pattern facts: bipartite, 66 edges, three points per triple, no isolated points
ProvedSDC.pattern_factscombinatoricsincidence-graphsidorenko
The pattern facts. The incidence graph H is bipartite (the 13 points versus the 22 triples); its edge set has cardinality 66 - three incidences for each of the 22 triples; each triple of the table is a 3-element set; and every point lies in at least one triple. The edge count 66 is the exponent in Sidorenko inequality for this pattern, and the absence of isolated vertices is what makes the density comparison meaningful.
Preamble
import Mathlib import Definitions.Def_SDC_graphs import Definitions.Def_SDC_density
Formal statement
namespace SDC
/-! The pattern facts. The incidence graph H is bipartite (the 13
points versus the 22 triples), its edge set has cardinality 66 - three
incidences for each of the 22 triples - each triple is a 3-element set,
and every point lies in at least one triple. The edge count 66 is the
exponent in Sidorenko inequality for this pattern, and the absence of
isolated vertices is what makes the density comparison meaningful. -/
theorem pattern_facts :
H.IsBipartite ∧
H.edgeSet.ncard = 66 ∧
(∀ f : Fin 22, (faces f).card = 3) ∧
∀ p : Fin 13, ∃ f : Fin 22, p ∈ faces f := by
sorry
end SDC
Source
Mission-authored sanity lemma about the pattern of the uploaded manuscript A finite counterexample to Sidorenko conjecture (SidorenkoCounterexample.lean.txt): the facts recorded in Table 1 of the manuscript.
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: the pattern graph is bipartite, its edge set has ncard exactly 66, every one of the 22 face finsets has cardinality exactly 3, and for each of the 13 points there exists one of the 22 faces containing it.