Directed and asymmetric Sidorenko are equivalent (Theorem 5)
ProvedDirS.sidorenko_equivTheorem 5 of the paper, the main equivalence: if B is an oriented graph with a homomorphism to K_2, then the underlying undirected bipartite graph of B has the asymmetric Sidorenko property if and only if B has the directed Sidorenko property. The statement here is taken with B the orientation of a bipartite graph H, so the homomorphism-to-edge hypothesis is discharged by the presentation. The proof composes the graphon characterizations: by Proposition 22, asymmetric Sidorenko for the underlying graph is the graphon inequality t_bip >= |E W|^{e}; by Observation 16 the bipartite density of the graph is the directed density of its orientation; and by Proposition 21 the directed Sidorenko property is the very same graphon inequality. The conjectural converse directions of the paper - Conjecture 4 and Conjecture 7 - remain open and are deliberately not formalized.
Formalization Note The equivalence of the two Sidorenko properties is the goal of the mission; the equivalence of the two forcing properties (the preceding milestone) is its forcing counterpart. The quantifier shapes match on the two sides because the orientation presentation fixes the parts.
import Mathlib import Definitions.Def_DirS_gr import Definitions.Def_DirS_gw
namespace DirS
/-! The goal (Theorem 5): directed and asymmetric Sidorenko are
equivalent. For every bipartite graph H, the asymmetric Sidorenko property
of H and the directed Sidorenko property of the orientation of H are
equivalent. The proof runs through the graphon characterizations of
Propositions 21 and 22 (milestones 2 and 3) and the density agreement of
Observation 16 (milestone 1): the bipartite density of H in a graphon is
the directed density of its orientation in the same graphon, and the
exponents agree, so the two graphon inequalities coincide. The
conjectural converse directions of the paper - Conjecture 4, that every
bipartite oriented graph with a homomorphism to the edge has the directed
Sidorenko property, and Conjecture 7, its forcing counterpart - remain
open and are deliberately not formalized. -/
theorem sidorenko_equiv (m n : ℕ) (H : BipGraph m n) :
AsymSidorenko H ↔ DirSidorenko (orientOf H) := by sorry
end DirS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every bipartite graph H with two finite parts, the asymmetric Sidorenko property of H and the directed Sidorenko property of the orientation of H are equivalent. No hypotheses appear.