Directed Sidorenko forces a homomorphism to the edge (Observation 20)
ProvedDirS.dir_sid_needs_edgeObservation 20 of the paper: if the oriented graph B has the directed Sidorenko property, then B has a homomorphism to the directed edge K_2. The proof evaluates the Sidorenko inequality on the complete balanced bipartite orientation on n + n vertices, all edges directed from the first part to the second: its directed edge density is one half, while a graph without a homomorphism to the directed edge has no homomorphisms into it at all, so the inequality fails for large n. The colouring supplied by the homomorphism is exactly the two-colouring recorded by homToEdge.
Formalization Note The complete balanced bipartite orientation is the concrete graph knn of the graph layer; the quantitative content is the growth of the homomorphism count against n^{2 e(B)}.
import Mathlib import Definitions.Def_DirS_gr import Definitions.Def_DirS_gw
namespace DirS
/-! Milestone 4 (Observation 20): directed Sidorenko forces a homomorphism
to the edge. If the oriented graph B has the directed Sidorenko property,
then B has a homomorphism to the directed edge K_2. The proof evaluates
the Sidorenko inequality on the complete balanced bipartite orientation
on n + n vertices: a graph without a homomorphism to the edge has no
homomorphism into it at all, while its directed edge density is one half,
and the inequality fails for large n. -/
theorem dir_sid_needs_edge {m : ℕ} (B : OriGraph m) (h : DirSidorenko B) :
homToEdge B := by sorry
end DirS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: every oriented graph B with the directed Sidorenko property admits a Boolean colouring of its vertices such that every edge goes from a false-coloured vertex to a true-coloured vertex - a homomorphism from B to the directed edge. No other hypotheses appear.