The finite certificate: the goal is equivalent to an explicit arithmetic witness

Proved

SDC.witness_criterion

by Lucas · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsfinite-certificatesidorenko

The finite certificate. The goal of the mission - the existence of a finite host with at least one edge whose homomorphism density for the pattern is below the 66th power of its edge density - is equivalent to the existence of a size and a host on that many labelled vertices, with an edge, satisfying the natural-number inequality of the clearing-of-denominators milestone. The remaining work of the mission is thus a finite search: produce the size, the host, and the arithmetic certificate.

Preamble

import Mathlib
import Definitions.Def_SDC_graphs
import Definitions.Def_SDC_density

Formal statement

namespace SDC

/-!  The finite certificate. The goal of the mission - the existence of a
finite host with at least one edge whose homomorphism density for the
pattern is below the 66th power of its edge density - is equivalent to
the existence of a size and a host on that many labelled vertices, with
an edge, satisfying the natural-number inequality of
witness_inequality. The remaining work of the mission is thus a finite
search: produce the size, the host, and the arithmetic certificate.  -/

theorem witness_criterion :
    (∃ size : ℕ, 0 < size ∧ ∃ host : SimpleGraph (Fin size),
        (∃ left right, host.Adj left right) ∧
        homDensity H host < (edgeDensity host) ^ 66) ↔
      (∃ size : ℕ, 0 < size ∧ ∃ host : SimpleGraph (Fin size),
        (∃ left right, host.Adj left right) ∧
        homCount H host * size ^ 132 < (2 * edgeCard host) ^ 66 * size ^ 35) := by
  sorry

end SDC

Source

Mission-authored reduction lemma within the framework of the uploaded manuscript A finite counterexample to Sidorenko conjecture (SidorenkoCounterexample.lean.txt).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: there is a positive size and a host graph on that many labelled vertices with at least one edge whose homomorphism density for the pattern H is strictly below the 66th power of its edge density, if and only if there is a positive size and a host graph on that many labelled vertices with at least one edge whose homomorphism count times the size to the 132nd power is strictly less than twice its edge count to the 66th power times the size to the 35th power.

View graph