The square of the Moebius ladder dominates the (5,3)-incidence graph (Theorem 2.1)
ProvedSidB.ms_squareTheorem 2.1 of the paper: for every graphon W, the homomorphism density of the (5,3)-incidence graph F_{5,3} is at most the homomorphism density of the square M^2 of the Moebius ladder M = K_{5,5} minus its ten-cycle, t_{F_{5,3}}(W) <= t_{M^2}(W). The proof writes t_{M^2}(W) as the expectation of the product over the five triples Z_i of rho(x_{Z_i})^2 and t_{F_{5,3}}(W) as the expectation of the product over all ten triples of rho once; symmetrizing over the 5! permutations of the left part and applying Hoelder's inequality (1) in the form E prod_I f~I <= prod_phi (E prod_I f{phi(I)})^(1/5!) closes the comparison, since the Z_i constitute half the triples. In the mission the inequality is the statement that the density of incGraph53 is at most the density of mobiusSquare for every graphon.
Formalization Note The symmetrization uses the transport axiom of the graphon interface over the permutations of the five-element left part, and the Hoelder (AM-GM) axiom is exactly the inequality (1) of the paper; the rho-power functionals are the weighted products the axiom consumes.
import Mathlib import Definitions.Def_SidB_graph import Definitions.Def_SidB_hyper
namespace SidB
/-! Milestone 1 (Theorem 2.1): the square of the Moebius ladder dominates
the (5,3)-incidence graph. For every graphon, the homomorphism density of
the (5,3)-incidence graph F_{5,3} is at most the homomorphism density of
the square M^2 of the Moebius ladder M = K_{5,5} minus its ten-cycle. The
proof of Section 2 symmetrizes over the permutations of the five-element
left part and applies the Hoelder axiom (the AM-GM inequality for the
expectation functional); the weak-norming property of the incidence graph,
recorded in the mission's milestone 4, then lifts this to Sidorenko for
M^2. -/
theorem ms_square (g : Graphon) :
g.dens incGraph53 ≤ g.dens mobiusSquare := by sorry
end SidB
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every graphon, the homomorphism density of the (5,3)-incidence graph - the membership bigraph between a five-element left part and its ten three-element subsets - is at most the homomorphism density of the square of the Moebius ladder, that is, of the blow-up with two copies per right vertex of the bigraph whose right vertex i is adjacent to the left vertices i-1, i, and i+1 cyclically. No hypotheses appear.