Paper deep dive

Formalizing Flag Algebras in Lean

Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 213

Intelligence

Status: not_run | Model: - | Prompt: - | Confidence: 0%

Entities (0)

No extracted entities yet.

Relation Signals (0)

No relation signals yet.

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Turán-type upper bounds, including Mantel's theorem and the Erdős pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Turán densities of Mantel's theorem and the Erdős pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

212,092 characters extracted from source content.

Expand or collapse full text

Formalizing Flag Algebras in Lean Gyeongwon Jeong ∗1,4 , Seonghun Park ∗1,4 , Jihoon Hyun 1 , Sang-il Oum 2,3 , and Hongseok Yang 4 1 School of Computing, KAIST, Daejeon, Korea 2 Discrete Mathematics Group, Institute for Basic Science (IBS), Daejeon, Korea 3 Department of Mathematical Sciences, KAIST, Daejeon, Korea 4 School of Computational Sciences, Korea Institute for Advanced Study (KIAS), Seoul, Korea E-mail addresses: jgyw0910@kaist.ac.kr, hun57@kaist.ac.kr, qawbecrdtey@kaist.ac.kr, sagil@ibs.re.kr, hongseokyang@kias.re.kr July 28, 2026 Abstract Razborov’s flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. The method is particularly well suited to constrained problems, where one seeks bounds for graphs that avoid specified finite patterns, such as triangles. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the mathematical foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. Our compiler treats the output of the external semidefinite programming search as candidate certificate data rather than as trusted input: lists of flags, target-density data, and rational positive-semidefinite matrices. It then directs Lean to compute the required density and multiplication facts independently and check those computations against the mathematical definitions, verify positive semidefiniteness exactly overQ, and carry out the algebraic normalization steps that occur in flag-algebra proofs. In our case studies, the compiler yields machine-checked proofs of seven Tur ́an-type upper bounds. These include the upper bounds in Mantel’s theorem and the Erd ̋os pentagon theorem; no proof of the latter that avoids flag algebras is known. They also include aC 4 -density bound for triangle-free graphs and edge-density bounds forK 4 -free,K 5 -free, andC 5 -free graphs. We use the underlying formalization directly as well, without the compiler, to give a separate proof of Mantel’s upper bound, formalize the matching constructions that complete both exact Tur ́an-density results, and prove two inequalities of Goodman. The design of our constrained semantics also prompted a separate meta-theoretic investigation comparing two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We briefly state the resulting root-plantability criterion that characterizes when these approaches agree; a forthcoming paper will present the complete mathematical and formal account. 1 Introduction Why flag algebras matter. Many central questions in extremal combinatorics ask how often one finite pattern can occur when another pattern is forbidden. LetFbe a finite simple graph andHa finite collection ∗ These authors are joint first authors of this work. 1 arXiv:2607.23500v1 [cs.LO] 26 Jul 2026 of finite simple graphs. We write ex(n, F ; H) := max number of induced copies of F in G||V (G)| = n, G is H-free , where an induced copy ofFinGis a vertex subsetS ⊆ V(G) with|S|=|V(F)|andG[S] ∼ = F, andH-free means thatGcontains no copy of any member ofHas a (not necessarily induced) subgraph. We obtain the corresponding asymptotic quantity by normalizingex(n, F;H) by the total number n |V (F)| of|V(F)|-vertex subsets and taking the limit; we call the result the Tur ́an density of F with respect to H: π(F ; H) := lim n→∞ ex(n, F ; H) n |V (F)| . For example, Mantel’s theorem [11] states that a triangle-free graph onnvertices has at most⌊n 2 /4⌋edges. Equivalently,ex(n, K 2 ;K 3 ) =⌊n 2 /4⌋, and the bound is achieved by the complete bipartite graphK ⌊n/2⌋,⌈n/2⌉ . The asymptotic value π(K 2 ; K 3 ) = lim n→∞ ⌊n 2 /4⌋ n 2 = 1 2 records that in any sufficiently large triangle-free graph, at most half of all vertex pairs are edges. (Whenever H =H is a singleton, we write H in place of H; so K 3 above abbreviates K 3 .) Determiningπ(F;H) is hard because it requires controlling all sufficiently largeH-free graphs: a valid upper bound must guarantee that, asymptotically, the proportion of induced copies ofFnever exceeds the claimed value, regardless of the size of the host graph. No finite collection of examples suffices, and the extremal graphs achieving the maximum may change unpredictably as n grows. Razborov’s flag algebra method [1] provides a proof technique for exactly this setting: it reduces the task of proving an asymptotic bound for an infinite class of graphs to checking finitely many algebraic conditions. A semidefinite programming (SDP) solver proposes a finite package of data intended to satisfy these conditions; we call this package a candidate certificate. The flag algebra framework explains why a candidate certificate that passes the checks establishes the desired bound for the whole class. This combination of mathematical abstraction and computer search has been unusually effective. It proved the Erd ̋os pentagon theorem [4,3], concerning the maximum asymptotic density of pentagons in triangle-free graphs, and determined the minimum triangle density for a given edge density [5]. It determined the maximum inducedC 5 density [8] and settled the rainbow-triangle density problem [9]. It has also produced the best known upper bound on Tur ́an’s tetrahedron problem [6] and several exact Tur ́an-density results for 3-uniform hypergraphs [7]. Formalizing the method. We first formalize in Lean the mathematical foundations of Razborov’s flag algebra method for finite simple graphs. This development includes partially labeled graphs and their densities in large graphs, an algebra of density expressions modulo the identities that relate different graph sizes, positive homomorphisms representing graph limits, and the downward operator that turns a labeled density expression into an unlabeled one. We call this part of the development the specification layer (Section 3). Its definitions follow the standard mathematics closely: flags are isomorphism classes of labeled graphs, densities are sampling probabilities, and algebraic expressions are identified when expansion identities give them the same asymptotic meaning. This layer provides the mathematical interface needed to express flag-algebra proofs in Lean much as they appear on paper. From certificates to formal proofs. Stating the method is not the same as checking a concrete application. Each application is supported by a candidate certificate that is compact to state but potentially costly to audit: the Erd ̋os pentagon certificate relies on thousands of exact density values and on rational matrices whose positive semidefiniteness must be established exactly. Such data are impractical to verify by hand, yet a formal proof should neither trust them nor require thousands of individually written proofs. We close this gap with two further layers. The reflection layer (Section 4) supplies executable graph representations, together 2 with adequacy theorems proving that the computations they support agree with the specification. Generation commands then specialize these theorems at elaboration time to produce the verified density, downward, and multiplication identities required by a certificate. The automation layer (Section 5) contains the certificate- to-proof compiler. It checks exact rationalLDL ⊤ factorizations to prove positive semidefiniteness overR, expands the target when necessary, and uses the reflected identities and custom tactics to normalize the certificate calculation under the forbidden-graph assumption and assemble the final bound. Constrained semantics. Our formalization also makes a choice about how to impose a forbidden-graph condition. In the usual built-in approach, one constructs the flag algebra using onlyH-free graphs. Our implementation instead retains the ambient algebra of all finite graphs and imposesH-freeness when an inequality is interpreted. For a typed inequality,forbidLEconsidersH-free empty-type positive homomor- phisms, chooses an occurrence of the flag type uniformly at random, uses its vertices as labels, and requires the inequality to hold with probability one. Section 8 calls this ensemble semantics and compares it with the built-in (or quotient) semantics. Every quotient-valid inequality is ensemble-valid. The two orders agree at the empty flag type, but they can differ at a nonempty flag type; they agree for all inequalities at a fixed flag type exactly when the constrained class is root-plantable at that flag type. We prove that blow-up closure guarantees this agreement and give a C 4 -free counterexample showing that heredity alone does not. Contributions. The paper makes four main contributions. First, it formalizes in Lean the core mathematical theory of flag algebras for finite simple graphs: flags and their densities, the quotient algebra, positive homomorphisms and semantic order, and the downward operator and random-extension machinery. Second, it develops an executable reflection layer, proves that its computations agree with the mathematical specification, and uses it to build a certificate-to-proof compiler that translates externally generated rational certificate data into algebraic proofs checked by Lean. Third, it evaluates the compiler on seven upper-bound certificates, including the bounds needed for Mantel’s theorem and the Erd ̋os pentagon theorem, as well as a bound on theC 4 -density of triangle-free graphs. A separate direct proof of Mantel’s theorem shows how to work with the flag-algebra formalization without the compiler. Matching lower bounds for Mantel’s theorem and the Erd ̋os pentagon theorem complete both Tur ́an-density results, while two inequalities of Goodman further illustrate uses of the same infrastructure outside the certificate pipeline. Fourth, it compares the semantics obtained by building a hereditary constraint into the flag algebra with the ensemble semantics used by our implementation. This comparison yields the root-plantability criterion, a sufficient condition based on blow-up closure, and aC 4 -free counterexample. The meta-theory is formalized in a separate, automatically generated Lean development that extends the manually written flag-algebra library. The complete Lean development, including the certificate-to-proof compiler and this autoformalized meta-theory, is publicly available at https://github.com/taeyool/lean-flag-algebras-release. Organization. Section 2 reviews the mathematical background of flag algebras and establishes the notation used throughout the paper. Section 3 presents the specification layer, including its semantic treatment of forbidden-graph assumptions. Section 4 introduces executable graph representations, proves that their computations agree with the specification, and explains how elaboration-time commands generate flags and their theorems. Section 5 describes the certificate-to-proof compiler, its exact checks of positive semidefiniteness and proof automation, and its evaluation on seven certificates. Section 6 illustrates direct uses of the underlying formalization beyond certificate compilation: a direct proof of Mantel’s theorem, matching lower-bound constructions for Mantel’s theorem and the Erd ̋os pentagon theorem, and two inequalities of Goodman. Section 7 discusses the main engineering obstacles and a recurring bijective proof pattern for finite counting identities. Section 8 presents the core results of our meta-theory of constrained semantics and describes its separate autoformalization, while Section 9 records the remaining design questions. Finally, Section 10 discusses related work, Section 11 presents our conclusions, and Section A reports compilation times for the seven compiler examples. 3 K 2 K 3 P 3 P 3 K 3 C 5 K • 2 K 2 • P 3 • P • 3 P ′ 3 • C • 5 Figure 1: Examples of flags when no graphs are forbidden (H=∅). Top row :∅-flags, equivalently ordinary graphs, of sizes 2, 3, and 5. Bottom row :σ-flags of the unique one-vertex flag typeσ. The filled vertex carries label 1, and the open vertices are unlabeled. Theσ-flagsP • 3 andP ′ 3 • have the same underlying path;P • 3 labels an endpoint, whereas P ′ 3 • labels the middle vertex. 2 Background: Flag Algebras This section recalls the mathematical definitions underlying flag algebras, following Razborov [1], and establishes the notation used later in the paper. No background in flag algebras or extremal combinatorics is assumed. For a non-negative integern, we write [n] for the set of positive integers at mostn. We consider only undirected, finite, and simple graphs; for a graphG, its vertex and edge sets are denoted byV(G) and E(G), respectively. We use the standard graph names:K n is the complete graph onnvertices,P n the path andC n the cycle onnvertices,Gthe complement ofG, andK a,b the complete bipartite graph with parts of sizes a and b. We fix a (possibly empty) finite setHof forbidden graphs. In this paper, an unqualified subgraph is an ordinary, not necessarily induced, subgraph. A graph isH-free if it contains no subgraph isomorphic to any member of H. All flag types, flags, and flag algebras defined below are relative to this fixed H. 2.1 Flag Types and Flags Flag Types. A flag type specifies the labeled part shared by all flags of that flag type. Formally, a flag type of sizekis anH-free graphσwith vertex set [k]. The empty flag type∅, of size zero, is the unique graph on the empty vertex set. We use the term flag type rather than Razborov’s original type to avoid confusion with Lean’s type system in later sections. Flags. For a graphGand a setS ⊆ V(G), letG[S] denote the induced subgraph ofGonS: its vertex set isS, and its edges are exactly the edges ofGwith both endpoints inS. Fix a flag typeσof sizek. A σ-flag is a pairF= (M,θ F ) consisting of anH-free finite graphMand an injective mapθ F : [k],→ V(M) that induces a graph isomorphism fromσtoM[Im(θ F )]. The size ofFis|V(M)|, and we writeV(F) for V(M). For eachi∈[k], the vertexθ F (i) carries labeli. The vertices inIm(θ F ) are therefore called the labeled vertices ofF; they are also often called its roots. All remaining vertices are unlabeled. For a setS ⊆ V(F) withIm(θ F )⊆ S, we writeF[S] for theσ-flag (M[S],θ F ) and call it theσ-flag induced byFonS. Flags over the empty flag type∅are simply ordinaryH-free graphs with no labeled vertices. Figure 1 illustrates several flags of different flag types. Twoσ-flags (M 1 ,θ 1 ) and (M 2 ,θ 2 ) are isomorphic, denoted by (M 1 ,θ 1 ) ∼ = σ (M 2 ,θ 2 ), if there is a graph isomorphismα:V(M 1 )→ V(M 2 ) withα◦ θ 1 =θ 2 ; this equation says thatαpreserves every label. The set of isomorphism classes ofσ-flags of sizenis writtenF σ n , andF σ = S n≥k F σ n . EachF σ n is finite, although F σ itself is infinite. When a flag typeσis fixed, we consistently call an individual flag of that flag type a σ-flag. We reserve the unqualified term flag for statements in which the flag type is unspecified, varies, or is irrelevant. 4 2.2 Subflag Densities In a density calculation, flags play two roles. The pattern flag is the small local configuration whose occurrence is being measured, while the host flag is the larger flag in which we sample vertices. These are roles in the calculation, not different kinds of flags. We useF, orF i , for pattern flags,Gfor host flags, andG ′ for an intermediate host flag when a third flag variable is needed. Let σ be a flag type of size k. Single-flag density. For aσ-flagFof sizem(the patternσ-flag) and aσ-flagG= (M,θ G ) of size n≥ m(the hostσ-flag), the density ofFinG, writtenp(F;G), is the probability that a uniformly random (m− k)-element subset ofV(G)\ Im(θ G ), together with theklabeled vertices ofG, induces aσ-flagF ′ with F ′ ∼ = σ F . Explicitly: p(F ; G) := 1 n−k m−k · n S ⊆ V (G)\ Im(θ G ) |S| = m− k, G[S∪ Im(θ G )] ∼ = σ F o . This value lies in [0,1] and is invariant under isomorphism of bothFandG. Whenn < m, we setp(F;G) := 0 by convention. Example 2.1 (Subflag densities inC • 5 ). Among the four unlabeled vertices of, exactly two are adjacent to the labeled one. Hence p(;) = 2 4 = 1 2 , p(;) = 2 4 = 1 2 . Chain rule. The densityp(F;G) can be computed in two equivalent ways: by samplingm− kunlabeled vertices directly fromG, or by first sampling an intermediateσ-flagG ′ of some sizen ′ withm ≤ n ′ ≤ n insideGand then samplingFinsideG ′ . These two procedures describe the same sampling experiment. The resulting identity is the single-flag case of Razborov’s chain rule [1, Lemma 2.2]. Lemma 2.2 (Chain rule). For F ∈F σ m , G∈F σ n , and n ′ with m≤ n ′ ≤ n, p(F ; G) = X G ′ ∈F σ n ′ p(F ; G ′ )p(G ′ ; G). Multi-flag density. For patternσ-flagsF 1 ,...,F t of sizesm 1 ,...,m t and a hostσ-flagG= (M,θ G ) of size n, we say F 1 ,...,F t fit in G if n− k ≥ (m 1 − k) +· + (m t − k). WhenF 1 ,...,F t fit inG, let (S 1 ,...,S t ) be a uniformly random tuple of pairwise-disjoint subsetsS i ⊆ V (G)\ Im(θ G ) with|S i |=m i −k. The density ofF 1 ,...,F t inG, writtenp(F 1 ,...,F t ;G), is the probability thatG[S i ∪ Im(θ G )] ∼ = σ F i for everyi∈[t]. WhenF 1 ,...,F t do not fit inG, we setp(F 1 ,...,F t ;G) := 0 by convention. 2.3 The Flag Algebra Fix a flag typeσof sizek. Informally, the flag algebraA σ is an algebra 1 of density expressions generated byσ-flags. Eachσ-flag is a symbolic building block: it stands for the density of that local labeled pattern in a large host graph. The quotient below records the identity of Lemma 2.2 among these building blocks. Formally, letR[F σ ] be the free real vector space onF σ , that is, the vector space of finite formal real linear 1 Here “algebra” means a vector space whose elements can also be multiplied. In this paper, the scalar coefficients are real numbers, multiplication is bilinear and associative, there is a multiplicative unit, and the order of multiplication does not matter: fg = gf . 5 combinations ofσ-flags. For aσ-flagF, write e F for its corresponding basis vector. Define the zero spaceZ σ as the subspace generated by all elements of the form e F − X G∈F σ n p(F ; G)· e G ,for F ∈F σ m and n≥ m.(1) The flag algebra is the quotient vector space A σ := R[F σ ]/Z σ . We write [F] for the class of e F inA σ . Throughout the paper, capital lettersF,Gdenote finite flags, while lowercase lettersf,g,hdenote arbitrary flag-algebra elements. For familiar named or pictorial flags, such asK 2 or, we retain the standard shorthand of omitting the brackets in algebraic formulas; there the surrounding algebraic context makes the canonical image unambiguous. We call P G∈F σ n p(F;G)·e G the expansion ofFat sizen. By Lemma 2.2, aσ-flagF ∈ F σ m and its expansion at any sizen ≥ mhave the same density in every hostσ-flag of size≥ n. The quotient byZ σ records this expansion identity as the equality [F ] = X G∈F σ n p(F ; G) [G]in A σ .(2) We may therefore freely replace [F ] by its expansion at any size n≥ m. Example 2.3 (K 2 expanded at size 3 in the triangle-free algebra). Working in the triangle-free flag algebra (i.e.,H=K 3 ), the∅-flags of size 3 are the three triangle-free graphs on three vertices:,, and. The density of an edge in each of them is p(K 2 ;) = 0, p(K 2 ;) = 1 3 , p(K 2 ;) = 2 3 , so the zero-space quotient identifies K 2 = 1 3 + 2 3 in A ∅ .(3) Multiplication. Forσ-flagsF 1 ∈F σ m 1 andF 2 ∈F σ m 2 , choose an auxiliary sizeℓ≥ m 1 +m 2 − kand define [F 1 ]· [F 2 ] := X G∈F σ ℓ p(F 1 ,F 2 ; G)· [G]in A σ .(4) At first glance, this definition appears to depend on both the choice ofℓand the choice of representatives for [F 1 ] and [F 2 ]. The zero-space quotient ensures neither matters: the product is independent ofℓand respects isomorphism classes of the inputσ-flags. Extending bilinearly to all ofA σ gives an algebra over the real numbers. Its multiplication is commutative, meaning thatfg=gffor allf,g ∈A σ . The unit of this algebra is the basis element represented by theσ-flag (σ, id [k] ) of sizek, in which the underlying graph isσ itself and every vertex is labeled; we write it as 1 σ , and simply as 1 when σ =∅. Example 2.4 (Multiplication ofK • 2 andK 2 • ). Letσbe the one-vertex flag type. Takingℓ= 3, the density p(,; G) equals 1 2 for each size-3 σ-flag G whose labeled vertex has degree exactly 1: p(,;) = p(,;) = 1 2 , and vanishes on all other size-3 σ-flags: p(,; G) = 0for all G∈F σ 3 \,. Hence ·= 1 2 + 1 2 in A σ . 6 2.4 Positive Homomorphisms and Semantic Order Fix a flag typeσ. The flag algebraA σ provides algebraic syntax for expressing densities of patternσ-flags. Flag algebra proofs, however, target asymptotic statements: rather than a single finite hostσ-flag, we consider increasing sequencesG n n∈N of hostσ-flags with|V(G n )|→∞and ask what happens toσ-flag densities in the limit. Positive homomorphisms can be thought of as the limiting density profiles of convergent sequences of hostσ-flags. The semantic non-negativity coneC σ then consists of the flag-algebra elements whose value under every positive homomorphism is non-negative, and establishing membership inC σ is precisely what flag algebra proofs aim to do. Convergent sequences. Call a sequenceG n n∈N of hostσ-flags increasing if|V(G 1 )| <|V(G 2 )| <·. Each hostσ-flagGdefines a pointp G ∈[0,1] F σ byp G (F) :=p(F;G). An increasing sequence is convergent if the sequence of pointsp G n converges in [0,1] F σ endowed with the product topology; equivalently, if lim n→∞ p(F ; G n ) exists for every σ-flag F . Positive homomorphisms. A positive homomorphism onA σ is a mapφ:A σ → Rthat preserves addition, multiplication, multiplication by real scalars, and the unit. It must also satisfyφ([F])≥0 for everyσ-flagF. Following standard flag-algebra terminology, we call such a homomorphism positive, although its defining inequalities are non-strict. We write Hom + (A σ ,R) for the set of all positive homomorphisms on A σ . In A σ , the following identity holds for every ℓ≥|V (σ)|: X F∈F σ ℓ [F ] = 1 σ .(5) Applying anyφ∈ Hom + (A σ ,R) to both sides gives P F∈F σ ℓ φ ([F]) = 1; non-negativity then forcesφ([F])∈ [0,1] for everyσ-flagF. Thus, eachφ ∈ Hom + (A σ ,R) determines a point in [0,1] F σ via the assignment F 7→ φ([F ]), so Hom + (A σ ,R) can be identified with a subset of [0, 1] F σ . The following theorem makes precise the sense in which positive homomorphisms are exactly the limiting density profiles of convergent sequences of σ-flags [1]. Theorem 2.5 (Razborov).(a) If G n n∈N is a convergent sequence of σ-flags, then lim n→∞ p G n ∈ Hom + (A σ ,R). (b) Conversely, everyφ∈ Hom + (A σ ,R) satisfiesφ=lim n→∞ p G n for some convergent sequenceG n n∈N of σ-flags. Semantic non-negativity cone and order. For a fixed flag typeσ, define the semantic non-negativity cone C σ :=f ∈A σ | φ(f )≥ 0 for every φ∈ Hom + (A σ ,R). We write f ≤ H,σ gwhen g− f ∈C σ , where the subscriptHrecords that the comparison is made in theH-free world: bothA σ andC σ are built fromH-free graphs. Equivalently,f ≤ H,σ gmeans thatφ(f)≤ φ(g) for everyφ ∈ Hom + (A σ ,R). When σ=∅, we writef ≤ H gin place off ≤ H,∅ g, andCin place ofC ∅ . Note thatf ∈C σ is the same as saying 0≤ H,σ f . Two immediate examples of elements ofC σ are flag basis elements and squares. Everyσ-flagFgives an element [F]∈C σ , because positive homomorphisms send every flag basis element to a non-negative real by definition. For anyf ∈A σ , the squaref 2 satisfies 0≤ H,σ f 2 , becauseφ(f 2 ) =φ(f) 2 ≥ 0 for everyφ∈ Hom + (A σ ,R). Moreover, if 0≤ H,σ fand 0≤ H,σ g, then 0≤ H,σ f+g, sinceφ(f+g) =φ(f) +φ(g)≥0 for every φ∈ Hom + (A σ ,R). Similarly, if 0≤ H,σ f and c is a non-negative real number, then 0≤ H,σ c· f . 7 From semantic non-negativity to Tur ́an density. The problem of bounding the Tur ́an densityπ(F;H) from above reduces to establishing membership in C ∅ , as the following lemma shows. Lemma 2.6. If [F ]≤ H c· 1 for some c∈ R, then π(F ; H)≤ c. Proof. Suppose for contradiction thatπ(F;H)> c. Then there existε >0 and an increasing sequence of H-free graphsG k k∈N such thatp(F;G k )> c+εfor allk. Since eachp G k is a point in [0,1] F ∅ andF ∅ is countable, this product space is compact and metrizable. Hence the sequencep G k has a convergent subsequencep G k j ; by Theorem 2.5(a) its limit is someφ ∈ Hom + (A ∅ ,R). Sinceφis the pointwise limit ofp G k j , we haveφ([F]) =lim j p(F;G k j )≥ c+ε > c. But [F]≤ H c·1 meansφ([F])≤ cfor every φ∈ Hom + (A ∅ ,R), a contradiction. A matching lower bound typically comes from an explicitH-free construction whoseF-density approachesc, pinning down π(F ; H) exactly. Two classical results illustrate how this looks in flag algebra language. Example 2.7 (Mantel’s theorem [11]). Mantel’s theorem statesπ(K 2 ;K 3 ) = 1 2 , meaning asymptotically at most half of all vertex pairs in a triangle-free graph are edges. The upper bound translates into the flag algebra inequality [K 2 ]≤ K 3 1 2 ·1; the balanced complete bipartite graphsK ⌊n/2⌋,⌈n/2⌉ witness the lower bound. Example 2.8 (Erd ̋os Pentagon Theorem [3,4]). The Erd ̋os pentagon problem asks for the maximum density ofC 5 in triangle-free graphs; the asymptotic answer isπ(C 5 ;K 3 ) = 24 625 . The upper bound corresponds to the flag algebra inequality [C 5 ]≤ K 3 24 625 ·1; an explicitK 3 -free construction (the balanced blow-up ofC 5 ) witnesses the lower bound. 2.5 The Downward Operator Labeled flag algebras (i.e.,A σ withσ ̸=∅) are often richer than the unlabeled algebraA ∅ : establishing membership inC σ can be easier than working directly inC. The final extremal statement, however, is always about unlabeled graphs. The downward operator bridges this gap by mappingA σ toA ∅ in a way that preserves semantic non-negativity (Theorem 2.9), so valid inequalities proved in a labeled algebra can be transferred to the unlabeled one. For aσ-flagF= (M,θ F ), letF| ∅ denote the∅-flag obtained fromFby forgetting the embeddingθ F , i.e., viewing M as a ∅-flag. For a σ-flag F of size m with |V (σ)| = k, let q σ (F ) := θ ′ : [k] ,→ V (M )| θ ′ embeds σ into M and (M,θ ′ ) ∼ = σ F m(m− 1)· (m− k + 1) be the probability that a uniformly random injection [k],→ V(M) recovers the sameσ-flag asF. The downward operator J·K σ :A σ →A ∅ is then defined on flag basis elements by J[F ]K σ := q σ (F )· [F| ∅ ], extended linearly to all of A σ . For f ∈A σ , we callJfK σ the downward image of f . We write⟨σ⟩ 0 ∈A ∅ for the empty-type flag-algebra basis element represented by the underlying graph of the flag typeσ, with its vertex labels forgotten. Applying the downward operator to the typed unit therefore gives J1 σ K σ = q σ (1 σ )⟨σ⟩ 0 . Random homomorphisms. A positive homomorphismφ 0 ∈ Hom + (A ∅ ,R) records the limiting densities of unlabeled graphs along a convergent sequence of finite graphs. For a nonempty flag typeσ, its random extension can be understood through any such sequence realizingφ 0 : in each finite graph, choose uniformly at random an embedding ofσand use the embedded vertices as labels. Razborov’s random-extension theorem describes the limiting distribution of the resultingσ-flag densities. Wheneverφ 0 (⟨σ⟩ 0 )>0, meaning that the underlying unlabeled graph ofσhas positive limiting density, the following holds [1]: there exists a unique 8 probability measure onHom + (A σ ,R), which we denoteExt σ (φ 0 ), such that for everyf ∈A σ , the random positive homomorphismφ σ ∼ Ext σ (φ 0 ) satisfies E φ σ (f ) = φ 0 JfK σ φ 0 J1 σ K σ .(6) Note that the denominator is positive by the assumptionφ 0 (⟨σ⟩ 0 )>0, sinceφ 0 J 1 σ K σ =q σ (1 σ )· φ 0 (⟨σ⟩ 0 ) and q σ (1 σ ) > 0 always. Equation (6) implies that the downward operatorJ·K σ maps C σ to C: Theorem 2.9 (Razborov [1]). For any flag type σ and any f ∈A σ with 0≤ H,σ f , 0 ≤ H JfK σ . Proof sketch.Letφ 0 ∈ Hom + (A ∅ ,R); we showφ 0 (JfK σ )≥0. Ifφ 0 (⟨σ⟩ 0 ) = 0, thenφ 0 assigns density zero to the underlying unlabeled graph ofσ. The underlying graph of everyσ-flag contains an induced copy ofσ, so the downward image of everyσ-flag basis element also evaluates to zero underφ 0 . By linearity, φ 0 (JfK σ ) = 0. Otherwise, letφ σ ∼ Ext σ (φ 0 ). Since 0≤ H,σ f, every positive homomorphism onA σ evaluates f non-negatively, so E[φ σ (f )]≥ 0. Rearranging Equation (6): φ 0 JfK σ = φ 0 J1 σ K σ · E φ σ (f ) ≥ 0. Since φ 0 was arbitrary, we have 0≤ H JfK σ . A flag algebra proof of [F]≤ H c·1 typically proceeds as follows: first, one exhibitsf ∈A σ with 0≤ H,σ f for some nonempty flag typeσ(e.g., a squaref=g 2 ) and applies Theorem 2.9 to obtain 0≤ H JfK σ ; then, one addsJfK σ to [F] or an expansion of [F] at an appropriate size, and uses non-negativity of flag basis elements and Equation (5) to conclude [F ]≤ H c· 1. The following example illustrates this pattern. Example 2.10 (Mantel’s theorem via flag algebras). We proveK 2 ≤ K 3 1 2 ·1 in the triangle-free flag algebra. Let σ be the one-vertex flag type. Step 1: A key inequality. Since 0≤ H,σ (()−()) 2 , Theorem 2.9 gives 0≤ K 3 J(()−()) 2 K σ . Expanding the square, computing each product at size 3, and then applying the downward operator gives the following inequality in A ∅ : 0≤ K 3 J(()− ()) 2 K σ =J()· ()− 2· ()· () + ()· ()K σ = r +−+ z σ = − 1 3 − 1 3 .(7) Step 2: Algebraic derivation. Starting from Equation(3), we add two non-negative terms and simplify using Equation (5): K 2 = 1 3 + 2 3 by Equation (3) ≤ K 3 1 3 + 2 3 + 1 2 − 1 3 − 1 3 + 1 3 by Equation (7) and 0≤ K 3 = 1 2 · ++ = 1 2 · 1.by Equation (5) 9 3 Formalizing Flag Algebras in Lean 4 Informal flag algebra proofs are compact partly because their notation is deliberately overloaded. The same symbol may denote a concrete labeled graph, its isomorphism class, a basis vector in a free vector space, an element of the quotient algebra, or the real number obtained by applying a positive homomorphism to that element. On paper, these changes of viewpoint are usually harmless and are left implicit. In Lean, however, they create an immediate formalization challenge: each role must be represented by a separate type, and each passage between roles must be justified. In particular, constructions on concrete graphs must be invariant under isomorphism, expansion identities must hold in the quotient, multiplication must be well defined on the quotient algebra, and positive homomorphisms must preserve the algebraic operations. Our first design choice is therefore to make the Lean definitions follow the mathematics of Section 2 as closely as possible, even when the resulting definitions cannot be executed directly. Accordingly, flags are isomorphism classes of labeled graphs, densities are finite sampling probabilities, the flag algebra is a quotient by expansion identities, and positive homomorphisms provide semantic interpretations of algebra elements. The following subsections present these definitions in turn. Together with the maps between these representations and the theorems establishing their correctness, they form the specification layer. Several of these quotient-based definitions involve nonconstructive choices and are therefore markednoncomputable. For the finite calculations needed in later proofs, such as testing flag isomorphism and computing densities and products, the reflection layer of Section 4 provides executable procedures corresponding to the abstract definitions in the specification layer. Its adequacy theorems prove that the results returned by these procedures agree with those abstract definitions. Our second design choice concerns how forbidden-subgraph assumptions are represented in the Lean development. In the mathematical presentation of Section 2, we first fixHand construct flags and flag algebras within the class ofH-free graphs. Our Lean formalization instead constructs the ambient flag algebras without a forbidden-family parameter and imposesH-freeness later by restricting the positive homomorphisms considered by the semantic order. Thus, the core formalization implements the unconstrained theory. If an arbitrary forbidden family were carried through the definitions from the outset, even the elementary constructions of flags, densities, expansion identities, and multiplication would require an additional parameter and corresponding side conditions. By postponing the constraint, we formalize theH-independent algebraic definitions and results only once. The same Lean infrastructure can then be reused for different forbidden graphs, with the appropriate constraint introduced only in the semantic comparisons required by each extremal application. This design is sound for the Tur ́an-density applications formalized here: Section 3.6 defines the ensemble semantic order and states the transfer theorem that converts an empty-type ensemble inequality into the corresponding extremal-density bound. Section 8 places this design in a broader mathematical setting by comparing the ensemble semantic order with the order obtained by building the constraint into the flag algebra from the outset. It gives a criterion for the two orders to agree, broad sufficient conditions for agreement, and an example in which they differ. A forthcoming paper will develop this meta-theory and its applications in full. For Lean-facing notation, we write the empty flag type as∅ t , rather than the∅used in Section 2, to distinguish it from ordinary empty sets. The Lean snippets below are lightly adapted for exposition. We make otherwise inferred parameters explicit and occasionally replace implementation-oriented names with clearer paper-facing names, so that the relevant types and dependencies are visible without requiring the surrounding source context. 3.1 Flag Types and Flags Our formalization builds on Mathlib, particularly its graph library. Before giving the Lean definitions of flags, we recall the small amount of Mathlib notation used below. In Section 2, we described a finite graph as having a vertex setV(G). In Lean, the vertex set is represented by a type: a term of typeSimpleGraph Vis a simple graph whose vertices are the elements of the typeV. Finiteness is supplied separately by assumptions such asFintype V. For example,SimpleGraph (Fin n)is a graph on the typeFin n, whose elements are the natural numbers 0,...,n− 1. 10 Mathlib providesG ,→ g Hfor the type of graph embeddings fromGtoH. Such an embedding is an injective vertex map that preserves and reflects adjacency, so its image is an induced copy ofGinH. Mathlib also providesG≃ g Hfor graph isomorphisms. With this notation in place, the concrete pairF= (M,θ F ) from Section 2 is represented by LabeledGraph, while its isomorphism class is represented by Flag. abbrev FlagType (T : Type) := SimpleGraph T structure LabeledGraph T : Type [Fintype T] (σ : FlagType T) (V : Type) where graph : SimpleGraph V type_embed : σ ,→g graph HereFlagType Tis simply a name forSimpleGraph T: a flag type is represented by a simple graph on the label typeT. The structureLabeledGraphpackages the two pieces of a concreteσ-flag: the fieldgraphstores the underlying graphM, and the fieldtypeembedstores the embeddingθ F :σ ,→ g M. In the signature, braces mark implicit parameters that Lean normally infers from context, whereas square brackets mark typeclass assumptions. Thus,[Fintype T]tells Lean that the label typeTis finite; later definitions use assumptions such as [DecidableEq V] when equality on a vertex type must be decidable. We defineLabeledGraphIsoas a structure representing isomorphisms between twoLabeledGraphterms, and define Flag by quotienting LabeledGraph by this isomorphism relation: structure LabeledGraphIso T V V’ : Type [Fintype T] σ : FlagType T (G : LabeledGraph σ V) (G’ : LabeledGraph σ V’) where graph_iso : G.graph ≃g G’.graph type_preserve : graph_iso ◦ G.type_embed = G’.type_embed infixl:50 " ≃f " => LabeledGraphIso instance labeledGraphSetoid T : Type [Fintype T] (σ : FlagType T) (V : Type) : Setoid (LabeledGraph σ V) where -- r : LabeledGraph σ V → LabeledGraph σ V → Prop r := fun G G’ => Nonempty (G ≃f G’) iseqv := ... -- proof that r defines an equivalence relation def Flag T : Type [Fintype T] (σ : FlagType T) (V : Type) : Type := Quotient (labeledGraphSetoid σ V) The structureLabeledGraphIsorepresents an isomorphism of concreteσ-flags. It consists of a graph isomorphismgraphisobetween the underlying graphs, together with a compatibility prooftypepreserve saying that this isomorphism sends the labeled copy ofσinGto the labeled copy ofσinG ′ . This is the Lean form of the conditionα◦ θ G =θ G ′ . The notationG≃ f G ′ denotes this type of isomorphism data, with σ inferred from the two labeled graphs. Lean’s quotient type does not accept an arbitrary relation directly; it requires a setoid, which packages a relation with proofs that it is an equivalence relation. The instancelabeledGraphSetoidprovides this package forLabeledGraph σ V. Its fieldridentifies two termsG,G ′ when a labeled-graph isomorphism G≃ f G ′ exists, and its fieldiseqvcontains the proofs that this relation is reflexive, symmetric, and transitive. Finally,Flag σ Vis defined as the quotient ofLabeledGraph σ Vby that setoid, so its elements are precisely isomorphism classes of concrete σ-flags on the vertex type V. Lean’sQuotienttype comes with double-bracket notation for equivalence classes. In Lean code, the unsubscripted notationJxKmeans “the quotient class of the representativex,” with the relevant quotient inferred from the expected type. Thus, in this subsection, when the expected type isFlag σ V,JGKis the σ-flag represented by the concrete labeled graphG. Throughout the paper, unsubscripted double brackets denote quotient classes, whereas the subscripted bracketsJ−K σ andJ−K 0 denote the downward operator. We return to this quotient-class notation in Section 3.3. We can now representF σ n in Lean byFlag σ (Fin n). The typeFinFlag σcollectsσ-flags of all finite sizes and representsF σ = S n F σ n . It is defined as a dependent sum type: each element is a dependent pair 11 ˆ F=⟨n,F⟩, wherenrecords the size andFis theσ-flag of that size. In Lean, the two components are accessed as ˆ F.1 and ˆ F.2. def FinFlag k : N (σ : FlagType (Fin k)) : Type := Σ (n : N), Flag σ (Fin n) Unlike the definitions in Section 2, none of the definitions above carries theH-free condition: the underlying graphs are arbitrary. This is a deliberate interface choice. The core quotient and density machinery is developed once for all finite graphs, whileH-freeness is imposed later by restricting the positive homomorphisms used in the ensemble semantic order (Section 3.6). 3.2 Subflag Densities Formalizing the density function is not straightforward. The densityp(F 1 ,...,F t ;G) from Section 2 should be a function takingtpatternσ-flags and a hostσ-flag to a value in [0,1], butFlagis a quotient type of LabeledGraph. The standard way to define a function from a quotient type in Lean is to first define it on the underlying type, prove that it respects the equivalence relation, and lift it viaQuotient.lift. That is, one must first define the density withLabeledGraphinputs, and then prove that replacing any input by an isomorphic LabeledGraph gives the same result. We first introduceLabeledGraphListas an abbreviation for a (Fin t)-indexed tuple ofLabeledGraphs. Given such a tuple of patternLabeledGraphs and a hostLabeledGraph,labeledGraphListDensitycomputes the density as the number of tuples (S 1 ,...,S t ) satisfying the conditions in the definition ofp(F 1 ,...,F t ;G), divided by the total number of candidate tuples. Rather than adopting the probabilistic sampling formulation of Section 2, this direct ratio is easier to work with in Lean. abbrev LabeledGraphList T : Type [Fintype T] (σ : FlagType T) (t : N) (Vl : Fin t → Type) : Type := (i : Fin t) → LabeledGraph σ (Vl i) noncomputable def labeledGraphListDensity T W : Type [Fintype T] [Fintype W] [DecidableEq W] t : N Vl : Fin t → Type [FintypeList Vl] [DecidableEqList Vl] σ : FlagType T (Hl : LabeledGraphList σ t Vl) (G : LabeledGraph σ W) : Q := let r_list (i : Fin t) := (Hl i).size - σ.size labeledGraphListCount Hl G / multinomialCoefficient r_list (G.size - σ.size) The first line definesLabeledGraphListby spelling out what a finite list means in this dependent setting: it is a function that assigns to each indexi : Fin ta concreteσ-flagLabeledGraph σ (Vl i). The family Vl : Fin t → Typerecords the vertex type of each entry, so thetpatternσ-flags are not forced to share one ambient vertex type. The second definition gives the finite ratio corresponding top(F 1 ,...,F t ;G). HereHlis the tuple of pattern labeled graphs andGis the concrete labeled graph in which they are counted. The local function rlist records, for each pattern, how many unlabeled vertices it contributes: r i =|V (F i )|−|σ|. The helper labeledGraphListCount, whose Lean definition is omitted from the displayed excerpt, supplies the numerator. It counts tuples of induced labeled subgraphs ofGsuch that the entry at each indexiis isomorphic, as aσ-flag, to the patternHl i, and different entries use pairwise-disjoint sets of unlabeled vertices. The denominator appliesmultinomialCoefficienttorlistand|V(G)|−|σ|; it counts all ways to choose disjoint vertex sets of the required sizes from the unlabeled vertices ofG. Their ratio is the multi-flag density p(F 1 ,...,F t ; G), represented as a rational number. The square-bracketed parameters tell Lean what finite data and decision procedures are available. For a typeX,[Fintype X]supplies an enumeration of all elements ofX, while[DecidableEq X]supplies a 12 procedure for deciding whether two elements are equal. The pattern tuple may use a different vertex typeVl iat each index. Accordingly,[FintypeList Vl]and[DecidableEqList Vl]package the same information for every typeVl i. In Lean, such square-bracketed parameters are called typeclass parameters, and Lean normally supplies them automatically through its typeclass inference mechanism. Thenoncomputablekeyword signals that Lean cannot synthesize an algorithm to evaluate this definition directly. This poses no obstacle to formalizing flag algebra itself, but becomes relevant when applying the algebra to concrete extremal problems, a point we return to in Section 4. The concrete functionlabeledGraphListDensityhas two inputs: the tupleHlof pattern labeled graphs and the host labeled graphG. To make this a function ofσ-flags, we lift these two inputs separately. The host input is lifted fromLabeledGraphtoFlag; for the pattern tuple, the intermediate quotient is the quotient of concrete tuples by entrywise isomorphism. We first lift the host inputG, then lift the pattern tuples, and finally package the result as a function onFlagList. The congruence proofs, omitted below, show that the density is unchanged when the hostσ-flag or any patternσ-flag is replaced by an isomorphic representative. def labeledGraphListEqv T : Type [Fintype T] σ : FlagType T t : N Vl : Fin t → Type (Gl Gl’ : LabeledGraphList σ t Vl) : Prop := ∀ (i : Fin t), Nonempty (Gl i ≃f Gl’ i) instance labeledGraphListSetoid T : Type [Fintype T] (σ : FlagType T) (t : N) (Vl : Fin t → Type) : Setoid (LabeledGraphList σ t Vl) where r := labeledGraphListEqv iseqv := ... -- proof that the entrywise isomorphism is an equivalence def QuotLabeledGraphList T : Type [Fintype T] (σ : FlagType T) (t : N) (Vl : Fin t → Type) : Type := Quotient (labeledGraphListSetoid σ t Vl) abbrev FlagList T : Type [Fintype T] (σ : FlagType T) (t : N) (Vl : Fin t → Type) : Type := ∀ (i : Fin t), Flag σ (Vl i) noncomputable def labeledGraphListDensityLifted T W : Type [Fintype T] [Fintype W] [DecidableEq W] t : N Vl : Fin t → Type [FintypeList Vl] [DecidableEqList Vl] σ : FlagType T (Hl : LabeledGraphList σ t Vl) : Flag σ W → Q := Quotient.lift (fun G => labeledGraphListDensity Hl G) (...) -- proof that host-graph equivalence preserves density noncomputable def quotLabeledGraphListDensity T W : Type [Fintype T] [Fintype W] [DecidableEq W] t : N Vl : Fin t → Type [FintypeList Vl] [DecidableEqList Vl] σ : FlagType T : QuotLabeledGraphList σ t Vl → Flag σ W → Q := Quotient.lift labeledGraphListDensityLifted (...) -- proof that pattern-list equivalence preserves density noncomputable def FlagList.coe T : Type [Fintype T] σ : FlagType T t : N Vl : Fin t → Type (Fl : FlagList σ t Vl) : QuotLabeledGraphList σ t Vl := 13 Jfun i => (Fl i).outK noncomputable def flagListDensity T W : Type [Fintype T] [Fintype W] [DecidableEq W] t : N Vl : Fin t → Type [FintypeList Vl] [DecidableEqList Vl] σ : FlagType T : FlagList σ t Vl → Flag σ W → Q := fun Fl => quotLabeledGraphListDensity (FlagList.coe Fl) HerelabeledGraphListEqvsays that two concrete tuples are equivalent exactly when their entries are isomorphic as labeled graphs: for each indexi, there must exist an isomorphismGl i≃ f Gl’ i. The instance labeledGraphListSetoidsupplies the setoid required byQuotient. Its quotient isQuotLabeledGraphList. The abbreviation FlagList is the more convenient tuple of already-quotiented σ-flags. The three density definitions then lift the original concrete density one argument at a time. For a fixed concrete pattern tupleHl,labeledGraphListDensityLifted Hlis a functionFlag σ W → Q, obtained by quotienting the host argument. The next definition,quotLabeledGraphListDensity, lifts the pattern tuple as well, so its first input is aQuotLabeledGraphListand its second input is a hostFlag. In the final definition, the inputFlhas typeFlagList σ t Vl, that is,Fl iis already aσ-flag for eachi : Fin t. The termFlagList.coe Flhas typeQuotLabeledGraphList σ t Vl; concretely, it chooses a representative (Fl i).outfor eachσ-flag in the tuple and forms the quotient class of the concrete tuplefun i => (Fl i).out. Thus,flagListDensitycan callquotLabeledGraphListDensityafter converting the input tuple of σ-flags into the quotient-of-tuples input expected by the preceding definition. The followingflagDensity 1 andflagDensity 2 are specializations offlagListDensityto singleton and pair lists: noncomputable def flagDensity 1 T U W : Type [Fintype T] [Fintype U] [DecidableEq U] [Fintype W] [DecidableEq W] σ : FlagType T (F : Flag σ U) (G : Flag σ W) : Q := flagListDensity [F] f G noncomputable def flagDensity 2 T U 1 U 2 W : Type [Fintype T] [Fintype U 1 ] [DecidableEq U 1 ] [Fintype U 2 ] [DecidableEq U 2 ] [Fintype W] [DecidableEq W] σ : FlagType T (F 1 : Flag σ U 1 ) (F 2 : Flag σ U 2 ) (G : Flag σ W) : Q := flagListDensity [F 1 , F 2 ] f G Here the superscripted bracket notation is a tuple constructor forFlagList. Thus,[F] f is the one-entry FlagListwhose unique entry isF, and[F 1 , F 2 ] f is the two-entryFlagListsending the first index ofFin 2 toF 1 and the second toF 2 . The superscriptfdistinguishes this notation from ordinary list notation and from quotient brackets; it does not add another quotienting operation. Building on the definitions above, we prove the following chain rule (Lemma 2.2) and several of its variants. Although the statement is the elementary counting identity of Section 2, its formal proof must account for the quotient representation: the counts are defined on concrete labeled graphs, and the identity between them comes from an explicit bijection between the choices the two sampling procedures make (Section 7.5). theorem flagDensity_eq_sum_density_prods ℓ 0 ℓ 1 ℓ ℓ ′ : N σ : FlagType (Fin ℓ 0 ) (F 1 : Flag σ (Fin ℓ 1 )) (G : Flag σ (Fin ℓ)) (hℓ 1 : ℓ 0 ≤ ℓ 1 ) (hℓ ′ : ℓ 1 ≤ ℓ ′ ) (hℓ : ℓ ′ ≤ ℓ) : flagDensity 1 F 1 G = P G’ : Flag σ (Fin ℓ ′ ), flagDensity 1 F 1 G’ * flagDensity 1 G’ G := ... 14 3.3 The Flag Algebra To define the flag algebra, we first construct the free real vector space onF σ . Each element of this vector space is represented as a finitely supported function fromF σ toR, using Mathlib’sFinsupptype. We call the resulting type FlagVector σ; the constructor basisVector produces the basis vector for each σ-flag: abbrev FlagVector k : N (σ : FlagType (Fin k)) : Type := FinFlag σ → 0 R def basisVector k : N σ : FlagType (Fin k) (F : FinFlag σ) : FlagVector σ := Finsupp.single F 1 Here→ 0 denotes the type of finitely supported functions, andFinsupp.single F 1constructs the basis vector e F for F ∈F σ : the function taking value 1 at F and 0 elsewhere. Next, we define the zero spaceZ σ . The auxiliary functionflagExpansion F ℓis the Lean version of P G∈F σ ℓ p (F;G)·e G , the expansion ofFat sizeℓ. We encode the generating element of Equation(1)as zeroElement,zeroSet σcollects all elements of this form, andZeroSpace σis the linear subspace they span, represented in Lean by a Submodule: noncomputable def flagExpansion k : N σ : FlagType (Fin k) (F : FinFlag σ) (ℓ : N) : FlagVector σ := P F’ : Flag σ (Fin ℓ), flagDensity 1 F.2 F’ • basisVector ⟨ℓ, F’⟩ noncomputable def zeroElement k : N σ : FlagType (Fin k) (F : FinFlag σ) (ℓ : N) : FlagVector σ := basisVector F - flagExpansion F ℓ noncomputable def zeroSet k : N (σ : FlagType (Fin k)) : Set (FlagVector σ) := z | ∃ (F : FinFlag σ) (ℓ : N), F.1 ≤ ℓ ∧ z = zeroElement F ℓ noncomputable def ZeroSpace k : N (σ : FlagType (Fin k)) : Submodule R (FlagVector σ) := Submodule.span R (zeroSet σ) InflagExpansion, the black dot is Lean’s scalar multiplication operation onFlagVectors: it scales the basis vector indexed by ⟨ℓ,F ′ ⟩ by the density flagDensity 1 F.2 F’. Following the same pattern as the definition ofFlagfromLabeledGraphin Section 3.1, we now define the flag algebraA σ as a quotient ofFlagVector σ. The equivalence relationflagVectorEqvdeclares two elements ofFlagVector σequivalent when their difference lies inZeroSpace σ, andflagVectorSetoid σ packages this relation into a setoid so that Lean’s quotient type can be applied. def flagVectorEqv k : N σ : FlagType (Fin k) (f g : FlagVector σ) : Prop := f - g ∈ ZeroSpace σ instance flagVectorSetoid k : N (σ : FlagType (Fin k)) : Setoid (FlagVector σ) where r := flagVectorEqv iseqv := ... -- proof that flagVectorEqv is an equivalence relation abbrev FlagAlgebra k : N (σ : FlagType (Fin k)) : Type := Quotient (flagVectorSetoid σ) SinceFlagAlgebra σis another quotient type, iffis aFlagVector σ, the unsubscripted notationJfKdenotes its class in this quotient. The quotient therefore imposes a family of expansion identities: for everyσ-flagF : FinFlag σand every sizeℓ≥ F.1, the class ofbasisVector Fis identified with the class offlagExpansion F ℓ, that is, with the linear combination of all size-ℓ σ-flags weighted by their densities over F . 15 Formalizing multiplication inA σ also requires several steps. The termflagMulWithSizedefines the product of twoσ-flags at a chosen output sizeℓas in Equation(4). The termflagMulspecializes this product to the minimal admissible sizeℓ=F.1 +F ′ .1− k. Then,bilinearExtensionextendsflagMullinearly in each argument to give a product onFlagVector σ. This intermediate product is only a bilinear operation on formal sums; the quotient is where the usual algebra laws are established. Finally,Quotient.map 2 lifts the product to FlagAlgebra σ. noncomputable def flagMulWithSize k : N σ : FlagType (Fin k) (F F’ : FinFlag σ) (ℓ : N) : FlagVector σ := P G : Flag σ (Fin ℓ), flagDensity 2 F.2 F’.2 G • basisVector ⟨ℓ, G⟩ noncomputable def flagMul k : N σ : FlagType (Fin k) (F F’ : FinFlag σ) : FlagVector σ := flagMulWithSize F F’ (F.1 + F’.1 - k) noncomputable instance k : N (σ : FlagType (Fin k)) : Mul (FlagVector σ) where mul := bilinearExtension flagMul noncomputable instance k : N (σ : FlagType (Fin k)) : Mul (FlagAlgebra σ) where mul := by apply Quotient.map 2 (· * ·) -- proof omitted: for f f’ g g’ : FlagVector σ, -- flagVectorEqv f f’ and flagVectorEqv g g’ imply flagVectorEqv (f * g) (f’ * g’) HereQuotient.map 2 is a Lean built-in function that lifts a binary operation to a quotient type given a proof that the operation respects the equivalence relation. In the displayed definition, the expression(· * ·)is not a new operation: since its two arguments are flag vectors, Lean resolves*using the immediately preceding Mul (FlagVector σ)instance, whose multiplication isbilinearExtension flagMul. The quotient instance then lifts exactly this vector-level multiplication toFlagAlgebra σ. The proof obligation amounts to showing that this multiplication respectsflagVectorEqv, as noted in the comment above. The load-bearing lemma is that ZeroSpace σ is closed under multiplication by arbitrary flag vectors: theorem flagVector_mul_zeroSpace k : N σ : FlagType (Fin k) (f : FlagVector σ) z : FlagVector σ (hz_zero : z ∈ ZeroSpace σ) : f * z ∈ ZeroSpace σ := ... Together with commutativity, this says thatZeroSpace σis an ideal in the algebraic sense: multiplying a zero-space element by any flag vector still gives a zero-space element. This is exactly the property needed to define multiplication on the quotient. If two representatives differ by a zero-space element, then multiplying both by the same vector still gives representatives that differ by a zero-space element, so the product does not depend on the chosen representatives. This is the compatibility condition that allows the Lean definition to use Quotient.map 2 . A separate theorem handles the choice of output size: theorem flagMulWithSize_indep_on_size k : N σ : FlagType (Fin k) F 1 F 2 : FinFlag σ ℓ 1 ℓ 2 : N (hℓ 1 : F 1 .1 + F 2 .1 ≤ ℓ 1 + k) (hℓ 2 : F 1 .1 + F 2 .1 ≤ ℓ 2 + k) : flagVectorEqv (flagMulWithSize F 1 F 2 ℓ 1 ) (flagMulWithSize F 1 F 2 ℓ 2 ) := ... The hypotheseshℓ 1 andhℓ 2 are the admissibility assumptions on the two output sizes:ℓ 1 andℓ 2 must both be large enough to contain the two inputσ-flags after identifying their common flag typeσ. HereF j .1 is the total number of vertices ofF j , andkis the number of labeled vertices inσ. Equivalently, the intended output size is at leastF 1 .1 +F 2 .1− k: the unlabeled vertices outside the flag type are sampled disjointly in the twoσ-flags, while theklabeled vertices are shared. The theorem then says that any two such admissible output sizes give equivalent flag vectors, justifying the choice of the minimal size in flagMul. With these definitions in place, we prove thatFlagAlgebra σis an algebra over the real numbers and that its multiplication is commutative, completing the formalization of the algebraic structure of A σ . 16 3.4 Positive Homomorphisms and Semantic Order This subsection describes how we encode the semantic side of flag algebras in Lean: sequences of finiteσ-flags, their limiting density functions, positive homomorphisms, and the order induced by testing against all positive homomorphisms. The convergence theorem from Theorem 2.5 is the main mathematical bridge between finiteσ-flag sequences and positive homomorphisms, but the formalization first has to make each of these surrounding notions explicit. A sequence ofσ-flags indexed byNis represented byFlagSeq σ. The predicateConvergesTosays that such a sequence has a prescribed limiting density function. abbrev FlagSeq k : N (σ : FlagType (Fin k)) := N → FinFlag σ def ConvergesTo k : N σ : FlagType (Fin k) (s : FlagSeq σ) (a : FinFlag σ → R) : Prop := Increases s ∧ Tendsto (flagDensitySeq s) atTop (N a) Here the candidate limitais a real-valued function on finiteσ-flags. The first conjunct,Increases s, asserts that the underlying sizes of theσ-flagss(0),s(1),...strictly increase. The second conjunct uses Lean’s filter notation for convergence:atTopis the limitn→∞onN, andNais the neighborhood filter of the functiona. The termflagDensitySeq sis the sequence of density functions associated tos; itsn-th value sends a finite σ-flag F to p(F ; s(n)). Thus, the Tendsto line is the Lean statement that, for every finite σ-flag F , lim n→∞ p(F ; s(n)) = a(F ). Mathematically, a positive homomorphism is a mapφ:A σ → Rthat preserves addition, multiplication, multiplication by real scalars, and the unit, and satisfiesφ([F])≥0 for every finiteσ-flagF. The Lean definition follows this sentence almost literally: abbrev Hom k : N (σ : FlagType (Fin k)) := FlagAlgebra σ → a [R] R def PositiveHom k : N (σ : FlagType (Fin k)) : Type := φ : Hom σ // ∀ F : FinFlag σ, φJbasisVector FK ≥ 0 The arrow→ a [R]in the first definition is Lean’s notation for the type of functions preserving addition, multiplication, multiplication by real scalars, and the unit. Thus,Homabbreviates the type of these structure- preserving maps fromFlagAlgebratoR, with the flag typeσsupplied as its argument. The second definition is Lean’s subtype construction. Mathematically, we read it in the usual set-comprehension form φ∈ Hom(A σ ,R)| φ([F ])≥ 0 for every F ∈F σ . In other words, the only extra condition imposed byPositiveHomis non-negativity on flag basis elements. In Lean syntax, the expression after the subtype separator //, ∀ F : FinFlag σ, φ JbasisVector FK ≥ 0, is the predicate that imposes this condition. HerebasisVector Fis the formal basis vector representing F, and the unsubscripted quotient brackets send that flag vector to its class in the flag algebra beforeφ evaluates it. Using these definitions, we formalize Theorem 2.5 as two separate theorems. 2 2 For readability, the displayed statements give the limit profile the ambient function typeFinFlag σ → R. The Lean implementation instead packages such profiles in the auxiliary subtypeFlagDensitySpace σ, which records that every value lies in [0,1], and packages the profile induced by a positive homomorphism asφ.coe. Accordingly, the implemented conclusions are written more compactly asφ.coe = aandConvergesTo s φ.coe. The formulations are equivalent: every flag density lies in [0, 1], so the pointwise limit of a convergent flag sequence does as well. 17 -- Theorem 2.5 (a) theorem flagSeq_limit_mem_positiveHom k : N σ : FlagType (Fin k) (s : FlagSeq σ) a : FinFlag σ → R (hs_conv : ConvergesTo s a) : ∃ (φ : PositiveHom σ), ∀ (F : FinFlag σ), φJbasisVector FK = a F := ... -- Theorem 2.5 (b) theorem positiveHom_as_flagSeq_limit k : N σ : FlagType (Fin k) (φ : PositiveHom σ) : ∃ (s : FlagSeq σ), ConvergesTo s (fun F => φJbasisVector FK) := ... Hereais the same real-valued function on finiteσ-flags that appears in the definition ofConvergesTo. The first theorem assumes ConvergesTo s a and produces a positive homomorphism φ satisfying φ JbasisVector FK = a(F )for every finite σ-flag F. Thus, the limiting density profile of every convergentσ-flag sequence is induced by a positive homomorphism. Conversely, the second theorem starts with a positive homomorphismφand produces aσ-flag sequences satisfying ConvergesTo s F 7→ φ(JbasisVector FK) . In other words, the density profile induced by every positive homomorphism arises as the limit of aσ-flag sequence. Both directions require nontrivial formalization work. In part (a), one must show that the limitaof aσ-flag sequencessatisfies all algebraic properties of a positive homomorphism, including details that informal proofs leave implicit. Part (b) goes in the opposite direction. Starting from a positive homomorphismφ, the proof uses the valuesφ([G]) to put a probability distribution on the finiteσ-flags of each sufficiently large size: aσ-flagGis sampled with weightφ([G]). These weights are indeed probabilities becauseφis non-negative on flag basis elements and satisfies the normalization identity X G∈F σ ℓ φ([G]) = φ   X G∈F σ ℓ [G]   = φ(1 σ ) = 1. One then samples an entire sequence X = (X 0 ,X 1 ,...), whereX n is chosen from the distribution onσ-flags of sizen 2 +k. The key estimate says that, for each fixed testσ-flagF, the densityp(F;X n ) is very likely to be close toφ([F]) oncenis large. Thus, almost every sampled sequence has the limiting density profile prescribed byφ. Selecting one such realization and calling itG 0 ,G 1 ,...gives the deterministicσ-flag sequence required by Theorem 2.5(b). The Lean proof formalizes this argument by constructing the product measure on flag sequences, proving that the required coordinatewise convergence event has probability one, and selecting a realization from that event. We also define the semantic non-negativity coneC σ and the order it induces onA σ . Here,semanticCone σ is the set of elements inFlagAlgebra σthat every positive homomorphism evaluates non-negatively. The induced order is installed as a Lean LE instance, with f ≤ g defined to mean g− f ∈C σ . def semanticCone k : N (σ : FlagType (Fin k)) : Set (FlagAlgebra σ) := f | ∀ φ : PositiveHom σ, φ f ≥ 0 instance k : N (σ : FlagType (Fin k)) : LE (FlagAlgebra σ) where le := fun f g => g - f ∈ semanticCone σ 18 3.5 The Downward Operator The downward operator from Section 2.5 forgets the labels of a typed flag-algebra expression while keeping the correct averaging factor. On a single σ-flag F , the intended formula is J[F ]K σ = q σ (F )· [F| ∅ ]. The displayed formula specifies the downward operator on flag basis elements. To implement it, we first define the normalizing factor and the operation of forgetting labels on concreteσ-typed labeled graphs, and prove that both are independent of the chosen representative. This gives the downward image of an individual σ-flag. We then extend this operation linearly to flag vectors and prove that two flag vectors representing the same element of A σ have the same image in A ∅ . The result is a well-defined operator A σ −→A ∅ . Fix a flag typeσwithkvertices. We regard these vertices ofσas labels. A concreteσ-typed labeled graphGonnvertices includes an embedding ofσintoG, which places these labels onkvertices ofG. Its normalizing factor is computed by counting such label placements. The numerator,isomorphismCount G, counts the injections of theklabels into the underlying graph that produce a typed labeled graph isomorphic to G. Its denominator n! (n− k)! is the total number of injections of those labels into the n vertices. Their ratio is q σ (G). The other ingredient,F| ∅ , simply forgets the type embedding while retaining the underlying graph. The following listing shows the concrete definitions of the two ingredients, their lifts to isomorphism classes, and the mapdownwardFlagthat combines them. The subsequent listing carries out the linear extension and the passage to the flag algebra described above. noncomputable def downwardNormalizingFactor_labeledGraph k n : N σ : FlagType (Fin k) (G : LabeledGraph σ (Fin n)) : Q := let num_of_all_injections := n.factorial / (n - k).factorial isomorphismCount G / num_of_all_injections noncomputable def downwardNormalizingFactor k n : N σ : FlagType (Fin k) : Flag σ (Fin n) → Q := Quotient.lift (fun G : LabeledGraph σ (Fin n) => downwardNormalizingFactor_labeledGraph G) (...) def unlabel_labeledGraph k : N V : Type σ : FlagType (Fin k) (G : LabeledGraph σ V) : LabeledGraph ∅ t V := ... noncomputable def unlabel k : N V : Type σ : FlagType (Fin k) : Flag σ V → Flag ∅ t V := Quotient.lift (fun G : LabeledGraph σ V =>Junlabel_labeledGraph GK) (...) noncomputable def downwardFlag k n : N σ : FlagType (Fin k) (F : Flag σ (Fin n)) : FlagVector ∅ t := downwardNormalizingFactor F • basisVector ⟨n, unlabel F⟩ The definitions appear in the order of this construction. The counting ratio on concreteσ-typed labeled graphs is implemented bydownwardNormalizingFactorlabeledGraph, and its lift to isomorphism classes is downwardNormalizingFactor. Similarly,unlabellabeledGraphforgets the type embedding at the concrete level, whileunlabellifts this operation to flags. Finally,downwardFlagforms the empty-type basis vector indexed by the pair ⟨n, unlabel F⟩ and scales it by downwardNormalizingFactor F. We next lift the single-flag construction to the algebra. The mapdownwardFlagVectorfirst extends downwardFlaglinearly from basisσ-flags to arbitraryσ-typed flag vectors. Its output is an empty-type flag 19 vector; taking its zero-space quotient givesdownwardFlagVectorQuot, whose values lie inFlagAlgebra ∅ t . At this stage the input is still a flag vector rather than an element of FlagAlgebra σ. To quotient the input as well, we must show that the construction is independent of the chosen represen- tative. The key respect lemma says that if twoσ-typed flag vectors differ by an element of the zero space, then their downward images represent the same element of the empty-type algebra. This is exactly the compatibility condition needed to define downward by a final quotient lift. noncomputable def downwardFlagVector k : N σ : FlagType (Fin k) : FlagVector σ → FlagVector ∅ t := linearExtension (fun F : FinFlag σ => downwardFlag F.2) noncomputable def downwardFlagVectorQuot k : N σ : FlagType (Fin k) : FlagVector σ → FlagAlgebra ∅ t := fun f : FlagVector σ =>JdownwardFlagVector fK lemma downwardFlagVectorQuot_respect_eqv k : N σ : FlagType (Fin k) f f’ : FlagVector σ (h : f - f’ ∈ ZeroSpace σ) : downwardFlagVectorQuot f = downwardFlagVectorQuot f’ := ... noncomputable def downward k : N σ : FlagType (Fin k) : FlagAlgebra σ → FlagAlgebra ∅ t := Quotient.lift (fun f : FlagVector σ => downwardFlagVectorQuot f) (...) notation "J" f "K 0 " => (downward f) The last definition is now a genuine mapFlagAlgebra σ → FlagAlgebra∅ t , independent of all representative choices. The final line introduces the Lean notationJfK 0 fordownward f; the subscript 0 emphasizes that the result lies in the empty-type algebra. In mathematical prose we useJfK σ , following Section 2.5, where the subscript instead records the type being forgotten. Altogether, the implementation consists of a quotient lift from concrete labeled graphs to flags, a linear extension to flag vectors, and a second quotient lift to the flag algebra. Having constructed the algebraic map, we turn to its semantic meaning. The key result is the formal random-extension identity from Equation (6); preservation of semantic non-negativity will follow from it. For the measure-theoretic statement, the implementation represents a random positive homomorphism by its density profile. The sample spacePositiveHomSpace σis the measurable subspace of [0,1] F σ consisting of profiles induced by positive homomorphisms. Each pointφof this space determines a positive homomorphism, andPositiveHomSpace.toPosHom φ fevaluates that homomorphism onf. Thus, a probability measure onPositiveHomSpace σcan be read simply as a distribution of positive homomorphisms. With this representation, the random-extension identity is stated as follows. theorem existsprobMeasureextendemptyTypepositiveHom k : N σ : FlagType (Fin k) φ 0 : PositiveHom ∅ t (hσ : φ 0 (⟨σ⟩ 0 ) > 0) : ∃ P : ProbabilityMeasure (PositiveHomSpace σ), ∀ f : FlagAlgebra σ, R (φ : PositiveHomSpace σ), PositiveHomSpace.toPosHom φ f ∂P = φ 0 JfK 0 / φ 0 J(1 : FlagAlgebra σ)K 0 := ... Mathlib writes R x, g x ∂μfor the integral ofx7→ g(x) with respect toμ; here∂μspecifies the measure and is not a derivative. In the displayed theorem,φranges overPositiveHomSpace σ, the integrand evaluates the corresponding positive homomorphism onf, and the measure isP. BecausePis a probability measure, the left-hand side is the expectation E φ∼P [φ(f )]. 20 The theorem therefore says exactly thatPsatisfies Equation(6), expressed using Lean’s downward notation: E φ∼P [φ(f )] = φ 0 (JfK 0 ) φ 0 (J1 σ K 0 ) . Thus, P realizes the random-extension measure Ext σ (φ 0 ) from Section 2.5. Equivalently, φ 0 (JfK 0 ) = φ 0 (J1 σ K 0 )E φ∼P [φ(f )]. This rearranged form explains the probabilistic construction behind the formal proof. Take a convergent sequence of finite graphs representingφ 0 ; in each graph, choose an embedding ofσuniformly at random, use the embedded vertices as labels, and evaluatef. Averaging and passing to the limit produces the expectation above, while the positive factor φ 0 (J1 σ K 0 ) accounts for the normalization of the random embedding. The random-extension identity now yields the desired transfer property. Iffis non-negative under every positive homomorphism of theσ-typed algebra, then every valueφ(f) in the expectation is non-negative. The rearranged identity therefore shows that the downward image offis non-negative under every empty-type positive homomorphism. This is the Lean counterpart of Theorem 2.9: theorem downward_preserve_semanticCone k : N σ : FlagType (Fin k) (f : FlagAlgebra σ) (hf : f ∈ semanticCone σ) :JfK 0 ∈ semanticCone ∅ t := ... The proof considers an arbitrary empty-type positive homomorphismφ 0 . Whenφ 0 (⟨σ⟩ 0 )>0, it applies the random-extension measure above. Whenφ 0 (⟨σ⟩ 0 ) = 0, a separate lemma shows that every downward image evaluates to zero, so the conclusion is immediate. The density bounds developed later use this theorem to transfer inequalities from a labeled algebra to the unlabeled one. 3.6 Forbidden Graphs and the Ensemble Semantic Order In Section 2, a finite forbidden familyHis fixed first, and the flag types, flags, algebras, and positive homomorphisms are all built inside theH-free world. In that setup, an inequalityf ≤ H,σ gis already an inequality in the constrainedσ-typed algebra: the forbidden configurations have been removed before the semantic order is tested. Our Lean formalization deliberately separates building the algebra from imposing the constraint. The core development constructs the ambient flag algebraA σ of all finite simple graphs, with no forbidden family as a parameter. A forbidden graph enters only when we compare two ambient algebra elementsf,g ∈A σ . We restrict attention to empty-type positive homomorphismsφ 0 that assign density zero to every graph containing the forbidden graph as a (not necessarily induced) subgraph. For each suchφ 0 for whichσhas positive density, take a sequence of finite graphs whose unlabeled density profiles converge toφ 0 . In each graph, choose an embedding ofσuniformly at random and use the embedded vertices as labels. The limiting distribution of the resultingσ-typed density profiles isExt σ (φ 0 ), and we requireφ(f)≤ φ(g) with probability one when φ is sampled from this distribution. Thus, the forbidden-graph condition does not define a separate flag-algebra universe in the implementation. Instead, it restricts the empty-type positive homomorphismsφ 0 from which the random extensions used in the comparison are formed. The elementsfandg, as well as the definitions of flags, densities, products, the downward operator, and positive homomorphisms, remain those of the ambient algebra and can therefore be reused across extremal problems. The order used for this a posteriori condition is the ensemble semantic order. We state it for a single forbidden graph H; a forbidden family would impose the zero-density condition below for every member. 21 Definition 3.1 (Ensemble semantic order). Fix a forbidden graphH, a flag typeσ, and elementsf,g ∈A σ in the ambient flag algebra. We writef ≤ ens H,σ gif, for every empty-type positive homomorphismφ 0 such that, viewing graphs as empty-type flag-algebra elements, φ 0 ([F ]) = 0for every graph F containing H as a subgraphand φ 0 (⟨σ⟩ 0 ) > 0, the random extension φ∼ Ext σ (φ 0 ) satisfies P φ(f )≤ φ(g) = 1. The first condition restrictsφ 0 to theH-free unlabeled limits: it assigns density zero to every graph containingH. The second condition,φ 0 (⟨σ⟩ 0 )>0, says that the underlying unlabeled graph ofσhas positive limiting density along any sequence of finite graphs converging toφ 0 . This is precisely the hypothesis under which the random-extension measureExt σ (φ 0 ) is defined. The final display says that, when aσ-typed positive homomorphism φ is sampled from this measure, the inequality φ(f )≤ φ(g) holds with probability one. Remark 3.2 (Relation to built-inH-free semantics). The background approach builds theH-free condition into the flag algebra from the outset, whereas the ensemble approach retains the ambient algebra and imposes the condition only when comparing its elements. At the empty type, where no labels are chosen, the two approaches agree, so this distinction does not affect the final unlabeled Tur ́an-density bounds. For nonempty types, however, the two approaches can differ: the built-in approach may fix the labels at an exceptional vertex configuration, whereas the ensemble approach obtains its labels by uniform random sampling. An exceptional choice of labels may therefore affect the built-in comparison while remaining invisible to the ensemble comparison. Section 8 gives a precise criterion for when the two approaches agree and an example showing that they need not. The Lean predicate forbidLE is the formalization of Definition 3.1: def forbidLEWith k : N σ : FlagType (Fin k) (C : ForbidCondition) (f g : FlagAlgebra σ) : Prop := ∀ (φ 0 : PositiveHom ∅ t ), φ 0 ⟨σ⟩ 0 > 0 → C φ 0 → P[φ 0 ] φ : PositiveHomSpace σ | φ f ≤ φ g = 1 def forbidLE k m : N σ : FlagType (Fin k) (H : SimpleGraph (Fin m)) (f g : FlagAlgebra σ) : Prop := forbidLEWith (forbiddenCondition H) f g ReadforbidLEfirst. Its explicit argumentHis the forbidden graph, andfandgare the two ambientσ-typed flag-algebra elements being compared. In particular,fandgdo not live in a separately builtH-free algebra. The definition delegates toforbidLEWith, the condition-generic version that takes aForbidConditionas a parameter. AForbidConditionis a predicate on empty-type positive homomorphisms, specifying which empty-type positive homomorphisms are allowed. The particular conditionforbiddenCondition Hselects the H-free ones: it considers only positive homomorphisms φ 0 such that φ 0 ([F ]) = 0for every ∅-flag F whose underlying graph contains H as a subgraph. The body offorbidLEWithranges over empty-type positive homomorphismsφ 0 . The hypothesisC φ 0 imposes the chosen condition onφ 0 ; forforbidLE H, this is theH-free condition described above. Recall thatPositiveHomSpace σis the measurable space ofσ-typed density profiles, each of which determines a positive homomorphism onA σ . The measureP[φ 0 ]is the random-extension measureExt σ (φ 0 ) on this space. In the final line of the definition, the set φ| φ(f )≤ φ(g) 22 is therefore the event that the real number assigned tofis at most the real number assigned tog. The equality to 1 says that this inequality holds with probability one when a density profileφis sampled from Ext σ (φ 0 ). What remains is to connect the semantic predicate above to the corresponding asymptotic bound on induced densities. This is the Lean counterpart of Lemma 2.6, with the hypothesis stated in the ensemble order of Definition 3.1 rather than in the built-in order of Section 2.4. In the theorem below,His the forbidden graph andFis the target graph. The expressionF.toFlagAlgebraconverts the simple graph Finto the corresponding element of the empty-type flag algebraFlagAlgebra ∅ t , whose evaluation is the induced F -density. The formal bridge packages this passage from semantic order to the finite asymptotic statement: theorem generalizedTuranDensity_le_of_forbidLE n m : N H : SimpleGraph (Fin n) F : SimpleGraph (Fin m) c : R (hc : 0 ≤ c) (h : forbidLE H F.toFlagAlgebra (c • (1 : FlagAlgebra ∅ t ))) : generalizedTuranDensity H F ≤ c := ... The hypothesishis an empty-typedforbidLEinequality: the target graphF, viewed as an element of the empty-type flag algebra, is at mostc·1 under the ensemble semantic order for the forbidden graphH. The con- clusion is the corresponding Tur ́an-density bound, written in Lean asgeneralizedTuranDensity H F ≤ c; mathematically, it is the assertion π(F ; H) = lim N→∞ max |V (G)|=N G is H-free p(F ; G)≤ c. Consequently, for each later application, it is enough to prove the empty-type ensemble inequality [F ]≤ ens H,∅ c· 1. The theorem above then yields the corresponding Tur ́an-density boundπ(F;H)≤ c. The same theorem performs this final conversion in every application. The Tur ́an densityπ(F;H) is represented in Lean bygeneralizedTuranDensity H F, whose definition uses Mathlib’slimUnder. This operation returns a real number even before the normalized extremal numbers have been shown to converge; if they did not converge, the returned value would have no asymptotic meaning. We therefore provetendstogeneralizedTuranDensity, which shows that the normalized extremal numbers converge toπ(F;H), namely togeneralizedTuranDensity H F. The proof is standard: oncen≥|V(F)|, the normalized extremal numbers are non-increasing, and they are bounded below by zero, so they converge. 4 The Reflection Layer The finite calculations a formal proof depends on can be discharged in two ways. One is to proceed as a mathematician usually would: when a finite claim is needed, write a proof of that claim directly. In the flag-algebra setting, this would mean proving, one by one, that two particular flags are isomorphic, that a certain density is a given rational number, or that a product of flag-algebra basis elements expands into a specified linear combination. This is possible in principle, but it is the wrong scale: a single nontrivial application contains many such finite checks, and hand-proving each one would bury the mathematical argument under routine case analysis. The second approach is computation-oriented. Instead of proving each finite calculation from scratch, we prove once that an algorithm correctly performs the kind of calculation we need, and then we let Lean run that algorithm inside later proofs. This is the idea of reflection. The reflection layer of our Lean formalization is the computable counterpart of the specification layer described in Section 3. For each finite operation that would otherwise require a hand proof, such as testing whether two labeled graphs represent the same flag, computing a density, or expanding a product, it provides a program that carries out the calculation and a 23 theorem saying that the program’s output agrees with the abstract definition. Later proofs can then run the program and invoke the correctness theorem, rather than reconstructing the finite verification case by case. Flag algebras are especially well suited to this style. In applications, the candidate bounds and their supporting numerical data are often found by computer search or semidefinite programming, and validating the resulting proof already amounts to checking finite data: same-flag tests, subflag densities, multiplication tables, and rational arithmetic. A formal proof should neither trust those external tables nor replay each entry as a hand proof. Reflection gives the middle path. Section 3 gave the specification layer: definitions close to the mathematics, where flags are identified up to isomorphism and quotient classes hide arbitrary choices of representatives. Those definitions are the right ones for stating theorems, but many are markednoncomputablebecause they are specifications rather than efficient programs. This section develops the executable mirror of that layer: concrete graph and flag representations, procedures for isomorphism testing, for computing densities, and for computing downward normalizing factors, and adequacy theorems proving that those procedures agree with the quotient-based definitions. 4.1 Concrete Graph Representations and Finite Search The finite coefficients in a flag-algebra proof come from concrete counting problems. For example, supposeF andGare∅-flags. To compute the densityp(F;G), one can conceptually enumerate all|V(F)|-vertex subsets ofG, regard their induced graphs as∅-flags, test which of them are isomorphic toF, count the successful ones, and divide by |V (G)| |V (F)| . For aσ-flag density, the same experiment keeps the labeled vertices fixed and chooses only the additional unlabeled vertices. The downward normalizing factorq σ (F) is another finite count of the same flavor: it counts label placements rather than subflags. Thus, an executable flag-algebra development needs two basic ingredients. It must be able to enumerate the finite objects being counted, such as candidate induced subflags, and it must be able to decide yes/no questions, such as whether two flags are isomorphic. In Lean, these ingredients are usually provided by typeclass instances. AFintypeinstance gives Lean an explicit finite collection containing every element of a type; aDecidableinstance gives a procedure for deciding a proposition. Once such instances are available, a definition that says “count all objects satisfying this predicate” can be evaluated by iterating over the finite collection and filtering by the decision procedure. The specification layer of Section 3, however, is not designed around producing such executableFintype andDecidableinstances. Its starting point is Mathlib’s graph typeSimpleGraph V, whereVis the type whose elements are the vertices of the graph and the adjacency relationAdjtakes two vertices and returns a proposition: structure SimpleGraph (V : Type*) where Adj : V → V → Prop symm : Symmetric Adj loopless : Irreflexive Adj This works well for the mathematical specification, but it is too general to be the data structure of the evaluator. The vertex typeVneed not come with an algorithm for enumerating its vertices, and the relationAdjneed not come with a Boolean decision procedure. SinceLabeledGraphs andFlags are built on top of this graph type, they inherit the same generality. Even if the specification layer knows that, for each size, there are only finitely many flags up to isomorphism, this does not by itself provide the computational choices needed by the evaluator: a concrete enumeration of representatives and a Boolean procedure for comparing them up to isomorphism. The reflection layer therefore does not useSimpleGraphdirectly as the evaluator’s representation. Instead, it introduces a family of more rigid edge-set representations: ann-vertex graph has vertex typeFin n, and its edge set is stored asFinset (Sym2 (Fin n)), a finite set of unordered pairs of vertices. This representation is packaged as the structureSym2Graph. We then reuse the same graph structure to define a concrete flag type, Sym2FlagType, and a concrete labeled graph, Sym2LabeledGraph. 24 structure Sym2Graph (n : N) where edges : Finset (Sym2 (Fin n)) edges_valid : ∀e in edges, ¬ e.IsDiag abbrev Sym2FlagType (k : N) := Sym2Graph k structure Sym2LabeledGraph k : N (σ : Sym2FlagType k) (n : N) where edges : Finset (Sym2 (Fin n)) edges_valid : ∀e in edges, ¬ e.IsDiag type_embed : fromEdgeSet (SetLike.coe σ.edges) ,→g fromEdgeSet (SetLike.coe edges) The expressionSetLike.coe edgesis the coercion that views the finite edge setedges : Finset (Sym2 (Fin n)) as an ordinary set of unordered pairs. This coercion is needed because Mathlib’s constructor fromEdgeSetbuilds an abstractSimpleGraphfrom a set of unordered vertex pairs, not from aFinset. Thus, fromEdgeSet (SetLike.coe edges)is the abstract graph decoded from the concrete edge data. The field typeembedthen says that the graph decoded fromσ’s edge set embeds into the graph decoded from the field edges. In other words, the concreteFinset-based representation still carries the usual flag-labeling map used by the specification layer. In this concrete definition, unlike in a generalSimpleGraph, Lean can enumerate all vertices of the type Fin n, namely 0,1,...,n−1. It can also check whether two verticesuandvare adjacent by testing whether the unordered pair u,v belongs to the explicit finite edge set edges. These basic choices then scale to the finite searches used by the evaluator. For example, to compute a densityp(F;G), the evaluator must range over possible placements ofFinside the hostG. Such a placement first chooses a finite set of vertices ofGthat contains all labeled vertices; this set then determines an induced subflag ofG, which can be tested for isomorphism withF. The followingFintypeinstance provides the enumeration used to range over these possible placements: structure Sym2InducedLabeledSubgraph k : N σ : Sym2FlagType k n : N (G : Sym2LabeledGraph σ n) where verts : Finset (Fin n) -- G.type_verts is the image of G.type_embed: the labeled vertices of G. verts_subset : G.type_verts ⊆ verts def Sym2InducedLabeledSubgraph.edges k : N σ : Sym2FlagType k n : N G : Sym2LabeledGraph σ n (H : Sym2InducedLabeledSubgraph G) : Finset (Sym2 (Fin n)) := G.edges.filter (fun (e : Sym2 (Fin n)) => ∀(v : Fin n), v ∈ e → v ∈ H.verts) instance k : N σ : Sym2FlagType k n : N (G : Sym2LabeledGraph σ n) : Fintype (Sym2InducedLabeledSubgraph G) where -- This Finset.univ enumerates all vertex subsets V : Finset (Fin n). elems := (Finset.univ : Finset (Finset (Fin n))).filterMap (fun (V : Finset (Fin n)) => if hV : G.type_verts ⊆ V then some ( verts := V, verts_subset := hV : Sym2InducedLabeledSubgraph G) else none) (by ...) -- complete proves that every H : Sym2InducedLabeledSubgraph G appears in elems. complete := fun (H : Sym2InducedLabeledSubgraph G) => ... The typeSym2InducedLabeledSubgraph Grepresents induced subflags ofG: it stores the chosen vertex set together with a proof that this set includes the labeled vertices. Its edge set is then computed by filteringG’s explicit edge set to the edges whose endpoints both lie in the chosen vertex set. TheFintype (Sym2InducedLabeledSubgraph G)instance provides an enumeration of all induced subflags ofG. Concretely, 25 the instance contains anelemsfield listing all elements of the typeSym2InducedLabeledSubgraph G, together with acompleteproof that this enumeration misses none of them. Here the enumeration is deliberately simple: since the vertices ofGareFin n, Lean enumerates all subsets of0,...,n−1, keeps exactly those containingG.typeverts, and stores the retained subset with the proof of containment. Each retained subset is then viewed as an induced subflag by usingGto compute the corresponding induced edge set. Thus, the subset enumeration becomes a finite list of candidatesH:Sym2InducedLabeledSubgraph G, which is the search space for the density calculation. To compute the numerator ofp(F;G), we still need to recognize which of these candidates are isomorphic to the patternF. This is the second basic ingredient: a decidable predicate on candidates which, givenH, decides whether the labeled graph associated toHis isomorphic to F , with the type labels respected. The schematic predicatecandidateMatches F Hbelow isolates this test. It is a one-pattern presentation of the isomorphism check that appears inside the implementation’s tuple-level predicatepredIsoSym2LabeledHl. It turns the induced subgraphHinto its associated labeled graph and asks whether the result is isomorphic toF, with the type labels respected. As stated,candidateMatches F His a proposition, not a program. The reflection step is to show Lean how to decide it from the concrete data stored inF,G, andH. The following small instance displays the mechanism used in the implementation: expose the finite vertex set of the candidate, read adjacency from explicit edge membership, reject candidates of the wrong size, and then invoke the finite isomorphism search. /-- Schematic one-pattern helper: H is isomorphic to the concrete pattern F. -/ def candidateMatches k m n : N σ : Sym2FlagType k (F : Sym2LabeledGraph σ m) G : Sym2LabeledGraph σ n (H : Sym2InducedLabeledSubgraph G) : Prop := Nonempty (H.toLabeledSubgraph.coe ≃f F.toLabeledGraph) /-- The finite edge-set representation turns the predicate into executable code. -/ instance candidateMatchesDecidable k m n : N σ : Sym2FlagType k (F : Sym2LabeledGraph σ m) (G : Sym2LabeledGraph σ n) : DecidablePred (fun H : Sym2InducedLabeledSubgraph G => candidateMatches F H) := fun H => by -- the vertex set of H is finite have : Fintype H.toLabeledSubgraph.subgraph.verts := by ... -- adjacency in H is decidable have : DecidableRel H.toLabeledSubgraph.coe.graph.Adj := by ... -- adjacency in F is decidable have : DecidableRel F.toLabeledGraph.graph.Adj := by ... exact if hsize : H.verts.card = m then (by dsimp [candidateMatches] -- unfold the definition of candidateMatches infer_instance) else isFalse (fun hIso => hsize (verts_card_of_coe_iso H F hIso)) /-- A one-pattern illustrative version of the reflection-layer density computation. -/ def sym2LabeledGraphDensity 1 k m n : N σ : Sym2FlagType k (F : Sym2LabeledGraph σ m) (G : Sym2LabeledGraph σ n) [DecidablePred (fun H : Sym2InducedLabeledSubgraph G => candidateMatches F H)] : Q := ((Finset.univ : Finset (Sym2InducedLabeledSubgraph G)).filter (fun H => candidateMatches F H)).card / Nat.choose (n - k) (m - k) The body ofcandidateMatchesdecodes both sides before comparing them. The pattern is decoded byF.toLabeledGraph, which readsF’s edgeFinsetthroughfromEdgeSetand keeps the type embed- ding, giving the abstractLabeledGraphof Section 3.1. The candidate is decoded in two steps. First, H.toLabeledSubgraphis the labeled subgraph ofG.toLabeledGraphwhose vertices areH.vertsand whose 26 edges are the induced ones computed above. Second,.coeviews that subgraph as a labeled graph in its own right, on the vertex typeH.verts, forgetting that it sits insideG. The two decoded labeled graphs are then compared with the isomorphism type≃ f of Section 3.1, andNonemptyturns it into the proposition that some such isomorphism exists. The proof of the instance is the computational heart of the example. After the localFintypeand DecidableRelinstances have been assembled, thehsizebranch reaches theinferinstanceline; this is the generic inference step. It asks typeclass search to decide theNonemptyproposition in the definition of candidateMatches, which says that such an isomorphism exists. The generic decidability instance does this by enumerating finitely many graph isomorphisms and checking the type-preservation condition. The schematic predicatecandidateMatches F Hhas therefore been reduced to a finite search. Thehsizebranch is not conceptually necessary for the definition, but it matches the implementation’s computation-oriented proof: a candidate whose vertex set has the wrong cardinality cannot be isomorphic toF, so it is rejected before the isomorphism search is run. Once the matching predicate is decidable, the density computation is ordinary finite evaluation. The illustra- tive definitionsym2LabeledGraphDensity 1 enumerates all candidatesH:Sym2InducedLabeledSubgraph G, filters them bycandidateMatches F H, counts the survivors, and divides by the number of ways to choose the non-type vertices. The same pattern is used for the multi-argument densityp(F 1 ,...,F t ;G) formalized in Section 3.2. There the numerator counts tuples of induced subgraphs that realizeF 1 ,...,F t insideG, with the chosen non-type vertices pairwise disjoint. The actual predicatepredIsoSym2LabeledHlin our Lean formalization is the computable version of this condition for tuples. Given the tuple of patternsHl and a tuple of candidate induced subgraphsGl, it checks, for everyi : Fin t, thatGl imatches the corresponding patternHl i, using the same decidable matching test as above, and that the candidates are disjoint away from the shared type vertices. Our computable implementation ofp(F 1 ,...,F t ;G) uses this predicate to filter the finite set of candidate tuples, and then counts the surviving tuples. In particular, the computable counterparts of the specification-level densities flagDensity 1 and flagDensity 2 are: def sym2FlagDensity 1 k : N σ : Sym2FlagType k m n : N (F : Sym2Flag σ m) (G : Sym2Flag σ n) : Q := ... def sym2FlagDensity 2 k : N σ : Sym2FlagType k m 0 m 1 n : N (F 0 : Sym2Flag σ m 0 ) (F 1 : Sym2Flag σ m 1 ) (G : Sym2Flag σ n) : Q := ... The arguments here are of typeSym2Flag, the reflection-layer counterpart ofFlagobtained by quotienting Sym2LabeledGraphby concrete isomorphism; Section 4.2 constructs it. Note that unlike the specification-level density functions, these definitions do not carry thenoncomputablekeyword: Lean has an executable algorithm for evaluating them. But computability alone does not say that they implement the density functions from the specification layer. The correspondence between this implementation and our noncomputable specification of p(F 1 ,...,F t ; G) is established by the adequacy theorems explained in the next subsection. 4.2 Adequacy Theorems for Reflection Section 3.1 defined flags by quotienting labeled graphs by isomorphism. The reflection layer repeats the same construction for the concrete graph representation from Section 4.1: def sym2LabeledGraphEqv k : N σ : Sym2FlagType k n : N (G G’ : Sym2LabeledGraph σ n) : Prop := ... instance sym2LabeledGraphSetoid k : N (σ : Sym2FlagType k) (n : N) : Setoid (Sym2LabeledGraph σ n) where r := sym2LabeledGraphEqv iseqv := ... -- reflexivity, symmetry, and transitivity of r def Sym2Flag k : N (σ : Sym2FlagType k) (n : N) : Type := Quotient (sym2LabeledGraphSetoid σ n) 27 The omitted definition ofsym2LabeledGraphEqvis standard, and says that two concrete labeled graphs are equivalent if there exists a label-preserving graph isomorphism between them. The displayed setoid instance packages this relation with its equivalence proofs, and Sym2Flag takes the resulting quotient. We now have two corresponding representations of flags. The specification-oriented development of Section 3.1 usesFlag, while the computation-oriented development of Section 4.1 usesSym2Flag. To use a computation from the reflection layer in a theorem stated in the specification layer, we need an explicit map from the latter representation to the former. We call this map Sym2Flag.toFlag: def Sym2Flag.toFlag k : N σ : Sym2FlagType k n : N (G : Sym2Flag σ n) : Flag (fromEdgeSet (SetLike.coe σ.edges)) (Fin n) := Quotient.lift (fun G : Sym2LabeledGraph σ n =>JG.toLabeledGraphK) ... -- proof that the lift respects the equivalence relation of the quotient G WithSym2Flag.toFlagin hand, we can carry out the reflection described in Section 4. It asks for a program and a theorem saying that the program’s output agrees with the abstract definition in the specification layer. Section 4.1 supplied the programs, and the theorems are the ones below. Our adequacy theorems state thatsym2FlagDensity 1 andsym2FlagDensity 2 agree with the abstract definitions offlagDensity 1 and flagDensity 2 after we decode Sym2Flags back to ordinary Flags using Sym2Flag.toFlag: theorem flagDensity 1 _eq_sym2FlagDensity 1 k : N σ : Sym2FlagType k m n : N (F : Sym2Flag σ m) (G : Sym2Flag σ n) : flagDensity 1 F.toFlag G.toFlag = sym2FlagDensity 1 F G := ... theorem flagDensity 2 _eq_sym2FlagDensity 2 k : N σ : Sym2FlagType k m 0 m 1 n : N (F 0 : Sym2Flag σ m 0 ) (F 1 : Sym2Flag σ m 1 ) (G : Sym2Flag σ n) : flagDensity 2 F 0 .toFlag F 1 .toFlag G.toFlag = sym2FlagDensity 2 F 0 F 1 G := ... A computable definition together with its adequacy theorem is what we call a reflected computation. With these adequacy theorems in place, a proof about a density in the specification layer can be reduced to a proof about the corresponding computable density in the reflection layer. Since this density is computable, Lean can then run the executable algorithm certified by the adequacy theorem to check the claimed value. For example, the density p(,;) = 1 2 from Example 2.4 is proved as follows: example : flagDensity 2 Sym2Flag_2_1_0_0.toFlag Sym2Flag_2_1_0_1.toFlag Sym2Flag_3_1_0_1.toFlag = 1 / 2 := by rw [flagDensity 2 _eq_sym2FlagDensity 2 ] decide +kernel In the code, the three displayed constants are concreteSym2Flags in the reflection layer:Sym2Flag2100 corresponds to,Sym2Flag2101corresponds to, andSym2Flag3101corresponds to. The statement appliestoFlagto each of these concrete flags, so it is a specification-level statement about flagDensity 2 . The commandrwuses the adequacy theoremflagDensity 2 eqsym2FlagDensity 2 and changes the goal to the closed reflection-layer computation sym2FlagDensity 2 Sym2Flag_2_1_0_0 Sym2Flag_2_1_0_1 Sym2Flag_3_1_0_1 = 1 / 2 The tacticdecide +kernelcloses a decidable goal by evaluating it inside the kernel. Here it runs the reflection-layer density computation above and closes the goal, so nothing outside the kernel is trusted. 28 The downward operator from Section 3.5 follows the same reflection pattern. The specification-level defi- nition uses the abstract downward normalizing factorq σ (F), implemented asdownwardNormalizingFactor. Its executable counterpart isdownwardNormalizingFactorSym2Flag. On a concreteSym2LabeledGraph over a flag type withklabels, onnvertices, Lean enumerates the finite set of type embeddings that produce an equivalent flag, takes its cardinality, and divides by the total numbern!/(n− k)! of injections of thek labels into thenvertices. The resulting computation is invariant under flag equivalence, so it can then be lifted through the Sym2Flag quotient. def isoEmbeddingCount_sym2LabeledGraph k : N σ : Sym2FlagType k n : N (G : Sym2LabeledGraph σ n) : N := (isoSym2TypeEmbeddingSetWithSameGraph G).card def downwardNormalizingFactor_sym2LabeledGraph k : N σ : Sym2FlagType k n : N (G : Sym2LabeledGraph σ n) : Q := let num_of_all_injections := n.factorial / (n - k).factorial isoEmbeddingCount_sym2LabeledGraph G / num_of_all_injections def downwardNormalizingFactor_Sym2Flag k : N σ : Sym2FlagType k n : N (F : Sym2Flag σ n) : Q := Quotient.lift (fun G => downwardNormalizingFactor_sym2LabeledGraph G) ... -- proof that downwardNormalizingFactor_sym2LabeledGraph respects the equivalence relation F These are executabledefs, rather than specification-levelnoncomputable defs. The first definition computes a natural number by taking the cardinality of the finite setisoSym2TypeEmbeddingSetWithSameGraph G . Its elements are the type embeddings ofσintoG’s graph, in the sense of thetypeembedfield of Sym2LabeledGraph, that give a labeled graph isomorphic toG. The second definition divides that count by the number of injections, so its value is exactlyq σ (G). The finalQuotient.liftapplies this same representative-level computation to aSym2Flag; its omitted representative-invariance argument proves that equivalent representatives give the same value. We then prove that the specification-level and executable implementations of the downward normalizing factor agree. theorem downwardNormalizingFactor_eq k : N σ : Sym2FlagType k n : N (F : Sym2Flag σ n) : downwardNormalizingFactor F.toFlag = downwardNormalizingFactor_Sym2Flag F := ... After decoding a concreteSym2Flagback to an abstractFlag, this adequacy theorem rewrites a goal about the specification-level coefficient as a goal about the executable functiondownwardNormalizingFactorSym2Flag. For instance, for the concreteσ-flag corresponding to, whereσis the one-vertex flag type, Lean proves q σ () = 2/3 by the same rewrite-and-evaluate pattern: example : downwardNormalizingFactor Sym2Flag_3_1_0_1.toFlag = 2 / 3 := by rw [downwardNormalizingFactor_eq] decide +kernel Here the command rw changes the goal to the closed computable equality downwardNormalizingFactor_Sym2Flag Sym2Flag_3_1_0_1 = 2 / 3 and decide +kernel evaluates that finite computation. The reflected normalizing factor is what makes the downward operator executable on concreteσ-flags. The reflection layer computes the underlying∅-flag and its normalizing factor, and the adequacy theorem certifies their product as the abstract downward image. By linearity, a finite linear combination of flag basis elements is handled term by term, so the downward identities needed in later flag-algebra proofs can be established by computation rather than by separate counting arguments. 29 4.3 Elaboration-Time Generation of Flags and Theorems The two examples in the preceding subsection show the basic unit of reflected computation. To prove the concrete densityp(,;) = 1/2, Lean rewrites the specification-level goal with the density adequacy theorem and then evaluates the resulting closedsym2FlagDensity 2 computation. To proveq σ () = 2/3, it performs the same two steps withdownwardNormalizingFactoreq. The adequacy theorems themselves are uniform: they prove the reflected evaluators correct for every possible input. What repeats in a concrete development is not the correctness argument, but its specialization to each concreteσ-flag and to each concrete density instance used by the later algebraic proof. The generated flags are named by a fixed scheme, already visible in the constants of Section 4.2. A name such asFlagnkmiorFlagAlgebrankmicarries four indices:nis the size of the flag,kis the size of its flag type,mis the position of the flag type’s graph in the enumeration of thek-vertex graphs, andiis the position of the flag itself in the enumeration of then-vertex flags of that flag type. Both enumerations are in a fixed canonical order. Graphs are ordered first by their number of edges and then by their canonical edge lists. The canonical edge list of a graph is the lexicographically smallest sorted edge list obtained by relabeling its vertices in all possible ways. The flags over a graph are ordered by the placement of their labels. The reflection-layer constantsSym2Flagnkmifollow the same scheme, and the empty flag type is written k=m= 0. Thus,Sym2Flag3101from Section 4.2 is flag number 1 among the three-vertex flags of the unique one-vertex type, namely, andFlagAlgebra3101is the corresponding basis element of the flag algebra. We use Lean’s metaprogramming facilities to automate this repetition. They specialize the uniform adequacy theorems to concrete flags and to the required single-pattern and pattern-pair density instances. More precisely, the generation commands displayed below are custom command elaborators written using Lean’s metaprogramming framework [24]. During elaboration, the phase in which Lean processes source commands and produces checked definitions and theorems, these commands run the finite enumerators and generate proofs of the required specialized facts. Once the resulting theorem families have been accepted by Lean, subsequent flag-algebra proofs use them as rewrite rules instead of evaluating the finite enumerators again. For the sizes and flag type used in the two examples of Section 4.2, the relevant commands have the following form: -- Generate empty-typed flags at pattern size 2 and host size 3. generate_empty_typed_flags 2 generate_empty_typed_flags 3 -- Use the unique flag type on one labeled vertex (k = 1, m = 0), -- and generate its flags at the sizes 2 and 3. generate_flags 2 1 0 generate_flags 3 1 0 -- Prove all pair densities, then all product expansions. generate_flag_pair_density_theorems_no_forbid 2 3 1 0 generate_mul_theorems 2 3 1 0 The numerical arguments are then,k,mof the naming scheme. The commandgenerateemptytyped flags ngenerates the empty-typed flags onnvertices, andgenerateflags n k mgenerates then-vertex flags of the flag type selected bykandm; herek= 1,m= 0 is the unique flag type on one labeled vertex. The density and multiplication commands take a pattern sizepand a host sizeh, followed by the same k,mdescribing the flag type, and the suffixnoforbidsays that no forbidden-graph filter is being applied. Here, a completeness lemma states that the generated names exhaust the relevant finite set: everyn-vertex σ-flag, up to label-preserving isomorphism, appears among the generated flags. For the empty flag type, this means that everyn-vertex graph is represented up to isomorphism; for a forbid-free enumeration, the same statement is restricted to theH-free flags. Table 1 collects the whole command family, including the forbid-free variants described below. 30 Table 1: The generation commands.nis a flag size andk,mselect the flag type, as in the naming scheme; the density and multiplication commands take a pattern sizepand a host sizeh. The forbid-free variants take a further argument H, a Sym2Graph term for the forbidden graph. CommandGenerates generateemptytypedflags nthe empty-typed flags onnvertices, with the completeness lemma generate flags n k mthen-vertex flags of flag type (k,m), with unlabelings, downward coefficients, and the completeness lemma generateflagpairdensitytheoremsnoforbid p h k mthe pair-density theorems for size-ppat- terns in size-h hosts generatemultheorems p h k mfor every pairF 1 ,F 2 ∈F σ p , the product expansion [F 1 ]· [F 2 ] = P G∈F σ h c G [G] generateforbidfreeemptytypedflags n HtheH-free empty-typed flags, with the filtered completeness lemma generateforbidfreeflags n k m HtheH-free typed flags, with unlabelings, downward coefficients, and the filtered completeness lemma generateforbidfreeflagpairdensitytheorems p h k m Hthe pair-density theorems over theH- free flags generateforbidfreemultheorems p h k m Hthe product expansions, valid modulo flags containing H generate forbidfreeflagdensitytheorems p i h Hthe single-flag densities ofFlagp00i in every H-free size-h host The important point is what each command contributes to subsequent proofs. The first four commands create the named two- and three-vertex flags used in the examples of Section 4.2, and each of the four also proves the corresponding completeness lemma. Generating the typed flags also computes and proves their downward identities, including the coefficientq σ () = 2/3. The pair-density command then generates a theoremflagDensity 2 F 1 F 2 G=cfor every unordered pair of two-vertex patterns (F 1 ,F 2 ) and every three-vertex hostG; this family includes the identityp(,;) = 1/2 displayed in Section 4.2. Finally, the multiplication command combines those coefficients with the completeness lemma for the hosts to prove the product expansion [F 1 ]·[F 2 ] = P G c G [G] for every pattern pair; completeness is what justifies summing over exactly the named hosts. Thus, elaboration produces the flags and their corresponding algebra basis elements, their unlabelings and downward coefficients, the density table, and the multiplication table, together with proofs of all the entries of these tables. Extremal applications work under a forbidden-graph assumption, and each of the commands above has a forbid variant for this situation. Thegenerateforbidfree*commands take one additional argument, a concreteSym2Graphterm for the forbidden graphH; the Mantel development, for example, definesK3 as the complete graph on three vertices and runsgenerateforbidfreeflags 3 1 0 K3. These variants emit constants and theorems only for flags whose underlying graphs avoidHas an ordinary, not necessarily induced, subgraph; their completeness lemmas state that the named flags exhaust precisely this set, using the same notion ofH-freeness as the forbidden-graph machinery of Section 3.6. One member of the family has no unforbidden counterpart:generateforbidfreeflagdensitytheorems p i h Hevaluates the single-flag densitiesflagDensity 1 of the empty-typed flagFlagp00iin everyH-free host of sizeh. The certificate compiler of Section 5 uses this table when the target is thep-vertex empty-typed flag indexed byi andp < h: the table provides the coefficients needed to express its density in terms of theH-freeh-vertex flags. 31 Optimizations. The pipeline employs the following optimizations to reduce the computational cost of elaboration. These optimizations do not eliminate the inherent combinatorial growth of flag enumeration and density computation, but they make the nontrivial examples considered in this paper feasible. • Size-inductive enumeration. The enumeration of flags is inductive in the size: the underlying n-vertex graph representatives are obtained by extending the (n−1)-vertex representatives by one vertex in all possible ways, and the typed flags onnvertices are obtained by placing the flag type’s labels on those representatives in every valid way. The working lists therefore stay close to one representative per isomorphism class, rather than covering all 2 ( n 2 ) graphs on a fixed vertex set. •Deduplication by cheap invariants. Both steps of that induction produce isomorphic duplicates: different vertex extensions, and different label placements, can yield the same flag. The enumeration therefore deduplicates as it goes, keeping a candidate only when it is isomorphic to no kept representative. These isomorphism tests are the expensive part, so each candidate carries a cheap isomorphism-invariant key, derived from its edge count and degree sequence, and the expensive test runs only when two keys collide. •Completeness from a verified enumerator. One way to certify a particular generated list would be to enumerate the full quotient type independently and compare it with that list. Such a check would establish completeness only for that particular run and would repeat the brute-force search that the size-inductive enumeration is designed to avoid. Instead, we prove once and for all, by induction on the size, that the enumeration algorithm of our Lean implementation produces a representative of every isomorphism class. A concrete generation run then needs only to check that the emitted constants coincide with the algorithm’s computed output. The completeness of that output follows by specializing the general theorem about the algorithm, rather than by independently searching the full space again. •Pruning under a forbidden graph. For a complete forbidden graph, the size induction itself prunes: onlyH-free representatives are extended, onlyH-free extensions are kept, and a cheap clique test decides containment, so flags containingHare never generated. For other forbidden graphs, the representative enumeration is filtered before any typed structure is built, so the labeled-graph work is spent only on the surviving graphs. The pruned generation nevertheless proves the same filtered completeness lemma. Its enumeration misses noH-free isomorphism class becauseH-freeness is invariant under isomorphism and preserved by deleting a vertex; the completeness statement therefore follows by induction on size. The pruning algorithm decidesH-freeness using ordinary subgraph containment. The filtered completeness lemma expresses the same condition in flag-algebra terms, by requiring every induced pattern whose underlying graph containsHto have density zero. Lean proves that these two tests retain exactly the same flags, so the enumeration can use the executable containment test while later proofs use the density-based completeness statement. Metaprogramming automates theorem construction, not verification: Lean still checks every generated proof, and a wrong coefficient makes that proof fail. Once accepted, these theorems let later arguments simplify downward images, densities, and products by rewriting rather than reopening the finite searches. Thus, the story of this section has three steps: concrete representations make the finite operations executable, adequacy theorems connect those operations to the abstract definitions, and elaboration-time generation turns their individual results into tables of proved facts. The next section uses those tables to automate complete flag-algebra arguments. 5 Automating Flag-Algebra Proofs Fix a forbidden familyH, a target graphF, and a proposed boundc. The task addressed in this section is to turn finite certificate data into a Lean proof of [F ]≤ H c· 1, 32 which expresses the desired asymptotic upper bound on the induced density ofFinH-free graphs. A flag-algebra certificate is a finite witness for this inequality: it specifies flags, rational matrices, and coefficients that purport to express the gapc·1−[F] as a sum of terms that are non-negative under theH-free condition. Flagmatic [18] uses semidefinite programming to search for such a witness. This section concerns certificate verification rather than certificate search. Our compiler accepts a certificate produced by Flagmatic as untrusted input, translates its flags, matrices, and target data into Lean, regenerates the required flags, recomputes their density and multiplication identities, verifies the rational matrix factorizations, and assembles the final inequality. Automating this translation is important because nontrivial certificates contain extensive finite bookkeeping that would be tedious and error-prone to reproduce manually. The resulting theorem is accepted only after Lean has checked every mathematical obligation. We first explain how positive semidefinite matrices justify the inequalities encoded by a certificate. We then identify the four obligations common to our examples and show how the compiler discharges them. Finally, we state the trust model and evaluate the compiler on seven certificates. 5.1 How a Certificate Proves a Bound At a high level, a flag-algebra certificate proves [F]≤ H c·1 by constructing two kinds of non-negative correction term. One kind consists of termsQ t , each obtained by applying the downward operator to a positive-semidefinite quadratic expression. The other is a remainderr, a linear combination ofH-free flags with non-negative coefficients. Under the H-free condition, these data yield the chain [F ]≤ H [F ] + X t Q t = c· 1− r ≤ H c· 1. The first inequality uses the non-negativity of theQ t , the equality is the finite calculation recorded by the certificate, and the final inequality uses the non-negativity ofr. Equivalently, the certificate decomposes the gap asc·1−[F] = P t Q t +r. Flagmatic [18] searches for this data using an SDP solver and outputs it as a certificate. Our compiler consumes the certificate as untrusted input and asks Lean to verify the non-negativity of the Q t and r and the intervening equality. Mantel’s theorem gives a small certificate with exactly the structure above. Here the target isF=K 2 , whose density is the edge density, and we abbreviate its basis element [K 2 ] byK 2 . We work with the one-vertex typeσ, choose a non-negative elementf ∈A σ , and use Theorem 2.9 to make its downward image Q :=JfK σ a non-negative correction term. We then show that K 2 + Q = 1 2 · 1− 1 3 · . Writer:= 1 3 · for the displayed remainder. The non-negativity ofQandrthen proves the desired bound. To constructf, take the two size-2σ-flagsand. We use these pictures directly in the algebraic calculation below. 3 Set f := 1 2 (( )− ()) 2 , Q :=JfK σ . For every positive homomorphism φ∈ Hom + (A σ ,R), φ(f ) = 1 2 φ (()− ()) 2 = 1 2 φ(()− ()) 2 ≥ 0. The first equality unfolds the definition offand uses preservation of scalar multiplication; the second uses preservation of multiplication, which rewrites the flag-algebra square as the square of the real number φ(()− ()). This makes the source of the non-negativity explicit: the final expression for φ(f ), 1 2 φ(( )− ()) 2 , 3 Strictly, each picture denotes a finiteσ-flag, whereas the algebraic operations below apply to its quotient class inA σ . We follow the usual convention of omitting brackets around pictorial basis elements. 33 is non-negative because it is a positive scalar multiple of the square of a real number. Thus,fis non-negative in A σ , and Theorem 2.9 gives 0≤ K 3 Q. To calculateQin the common size-three basis, we use the triangle-free flags,, and. The size-three expansion of K 2 from Equation (3) is K 2 = 1 3 ·+ 2 3 ·. Applying Equation (5) to the triangle-free empty-type flags of size three gives 1 = ++. A size-three product expansion followed by the downward operator gives Q = q 1 2 ()− () 2 y σ = q 1 2 +−+ y σ = 1 2 + 1 3 ·− 2 3 ·− 2 3 ·+ 1 3 · = 1 2 ·− 1 6 ·− 1 6 ·. The fractions produced by the downward operator are its normalizing factors: they record whether one, two, or all three choices of the labeled vertex produce the displayed σ-flag. Combining these identities now gives a derivation of the desired bound: K 2 ≤ K 3 K 2 + Q = 1 3 ·+ 2 3 · + 1 2 ·− 1 6 ·− 1 6 · = 1 2 ·+ 1 6 ·+ 1 2 · = 1 2 · ++ − 1 3 · = 1 2 · 1− 1 3 · ≤ K 3 1 2 · 1. The first inequality adds the non-negative downward squareQ. The successive equalities substitute the expansions ofK 2 andQ, collect their coefficients, and regroup the result as 1 2 · 1 minus the remainder using the unit expansion 1 =++. The final inequality follows because the remainderr= 1 3 ·is non-negative. The essential certificate data for this example are precisely the nontrivial terms in this derivation: the twoσ-flagsand, the downward imageQof their halved squared difference, and the non-negative remainderr= 1 3 ·. We chose this small certificate by hand; in larger examples, Flagmatic’s SDP search supplies the analogous flags, positive semidefinite matrices, and remainder coefficients. Checking even this certificate requires expanding a product, computing its downward image, expanding the target and the unit to a common host size, and collecting coefficients. These calculations remain suitable for automation but become impractical to perform and transcribe by hand for larger certificates; they are exactly what our compiler automates. The same idea scales by replacing one square with weighted sums of many squares. Chooseσ-flags E 1 ,...,E r , lete i := [E i ]∈ A σ be their basis elements, and collect these algebra elements into a vector v= (e 1 ,...,e r ) ⊤ . A symmetric matrixMis positive semidefinite (PSD) ifx ⊤ Mx ≥0 for every real vectorx. Consequently, whenM= (M ij ) is PSD, the flag-algebra quadratic form⟨v,Mv⟩= P i,j M ij e i e j is non-negative under every positive homomorphism: evaluating the algebra elements turns it into the ordinary real quadratic formx ⊤ Mx. The downward operator then transfers this non-negativity from the labeled algebra to the unlabeled one. 34 Flagmatic finds the matrices by turning this decomposition problem into a semidefinite program (SDP). It first fixes a host sizeNand chooses the flag types and flags that may occur. It expands the target, the unit, and the downward quadratic forms in the common basis of allowedN-vertex graphs, namely those that avoidH. At this point, the entries of the matrices are unknowns. Requiring the coefficient left over for every host graph to be non-negative gives linear constraints on those entries, and requiring each matrix to be PSD gives the semidefinite constraints. An SDP solver finds numerical matrices satisfying these conditions, after which Flagmatic converts them into exact rational matrices. A full certificate uses several flag types at once, one PSD matrix per flag type, so the single matrixM above becomes a family indexed by the flag type. The indextranges over the chosen flag typesσ t , each contributing its own flag vectorv t and matrixM t . We call the data for one such index, the flag typeσ t together withv t andM t , an SDP block ; the name reflects that the matricesM t are the diagonal blocks of the semidefinite program’s matrix variable. The downward quadratic form block t produces is Q t := q ⟨v t ,M t v t ⟩ y σ t . The resulting certificate specifies an identity, modulo the H-free condition, of the form [F ] + X t Q t = c· 1− r, where everyM t is PSD andris a linear combination ofH-free flags with non-negative coefficients. Equivalently, the certificate justifies the derivation [F ]≤ H [F ] + X t Q t = c· 1− r ≤ H c· 1. The first inequality adds the non-negative downward quadratic forms. The equality is the certificate identity checked after all terms have been expanded in the common host-size basis, and the final inequality follows from the non-negativity ofr. The certificate records the chosen flags, the rational matricesM t , and the target-density data needed to state this calculation. Our compiler does not trust the certificate’s derived density or multiplication tables: it recomputes them in Lean, proves the matrices are PSD, and checks the calculation. The rest of this section explains the four recurring parts of that verification and how the compiler generates them. 5.2 The Four-Part Compiler We organize the compiler around a four-part proof skeleton, with one part for each obligation in turning a certificate into a verified proof. The four parts are: 1. Generating the flags and density data. The proof must name the flags and corresponding flag- algebra basis elements it uses, restricted to those that are free of the chosen forbidden graph, and must prove the identities for single-flag densities, flag-pair densities, and products of flags sharing a common flag type. These identities support the algebraic rewrites used later in the proof. 2.Certifying the matrices. For each SDP blockt, the certificate supplies a rational matrixM t and a list ofσ t -flagsE t,i . The proof must define the vectorv t of their basis elementse t,i := [E t,i ] and must prove that M t is positive semidefinite. 3.Lifting the target (when needed). If the target graphFhas fewer thanNvertices, whereNis the host size chosen up front to bound the certificate search in Section 5.1, the proof must first lift [F] to the host-size basis, dropping the contributions that contain a copy of the forbidden graph. 4.Assembling the main theorem. WithQ t := q ⟨v t ,M t v t ⟩ y σ t and the certificate’s non-negative remainderr, the proof must assemble the bound [F]≤ H c·1 through the same chain as in Section 5.1: [F ] ≤ H [F ] + X t Q t = c· 1− r ≤ H c· 1. 35 The first inequality adds the non-negative downward quadratic forms arising from the matrices certified in Part 2. The middle equality is checked using the identities from Part 1 and, when needed, the target-lifting identity from Part 3. The final inequality follows becauserhas non-negative coefficients. The compiler handles each part with a small set of reusable proof-producing components. Consequently, a new theorem primarily requires new certificate data rather than a new proof architecture. For the certificate shapes supported by the current implementation, this four-part process is exposed through the gen-skeleton subcommand of flagmatictolean.py: python flagmatic_to_lean.py gen-skeleton <cert>.json <target>.lean Here <cert>.json is a placeholder for a Flagmatic certificate file, which identifies the target and forbidden graphs and contains the proposed bound, the flag types and flags used by each SDP block, and the rational matrix data. The argument<target>.leanis the path at which the script should write the generated Lean source file. The output file contains the flag and density generation commands of Part 1, the matrices and basis-element vectors of Part 2, the target-lifting lemma when Part 3 is needed, and the complete proof of the bound in Part 4. For example, applying the compiler to the Mantel certificate with the following command python flagmatic_to_lean.py gen-skeleton <mantel-cert>.json Mantel.lean --namespace Mantel --force generatesMantel.leanfrom the Mantel certificate. The optional--namespace Mantelargument selects the namespace of the generated declarations, and--forcepermits the script to replace an existing target file. Before generating the file, one can run the separate diagnostic command python flagmatic_to_lean.py inspect <mantel-cert>.json to check that the certificate can be parsed and that its flags can be matched to Lean’s enumeration. This command does not generate a proof file; it prints the resulting identifier mapping and the Part 1 generation commands. We now explain the generated Lean file one part at a time before showing an abridged assembled output. Generating the flags and density data (Part 1). This is where the reflection layer of Section 4 enters the compiler, making the finite bookkeeping involving flags and densities executable and checkable. Part 1 defines the certificate’s forbidden graph as aSym2Graphterm and invokes thegenerateforbidfree* commands of Section 4.3 on it. The commands choose between two enumeration procedures according to the forbidden graph: they use size-inductive clique pruning when the forbidden graph is complete, and the general ordinary-subgraph filtering procedure otherwise. During elaboration, they enumerate the flags that avoid the forbidden graph, with isomorphic flags appearing only once. For each enumerated flag, the commands emit a concrete reflection-layer constant, either aSym2EmptyTypedFlagat the empty flag type or aSym2Flagat a nonempty flag type, together with its decoded specification-levelFlagandFlagAlgebrabasis element. As in Section 4.3, the commands also prove the completeness lemma stating that the emitted flags exhaust the flags avoiding the forbidden graph. After emitting these flags, Part 1 generates the rewrite theorems, which are used later in Parts 3 and 4 of the proof. Concretely, for each emittedσ-flagF, Part 1 evaluates the downward normalizing factorq σ (F) from Section 3.5. For each relevant pair ofσ-flagsF 1 ,F 2 and hostσ-flagG, it also evaluates the pair density flagDensity 2 F 1 F 2 G, which supplies the coefficient of [G] in the product expansion of [F 1 ]·[F 2 ]. When the target must be lifted in Part 3, the generated file similarly contains proved evaluations of the required single-flag densities. The adequacy theorems from Section 4 turn all these reflection-layer evaluations into specification-level statements about the decoded flags. The multiplication generator then combines the pair-density identities with the general multiplication theorem and the completeness lemma for the generated flag set to derive the required product expansions. 36 Certifying the matrices (Part 2). With the flags and their rewrite theorems in place, Part 2 discharges the positive-semidefiniteness obligations. For each SDP block, the certificate stores rational matricesQ ′ t and R t withM t =R t Q ′ t R ⊤ t , whereR t may be rectangular andQ ′ t is a smaller symmetric matrix. Flagmatic’s user guide [17] explains the format:Q ′ t is chosen to be positive definite, which implies the positive semidefiniteness of M t . Our verification takes these data through a different, equally elementary witness. We state one Lean lemma for every PSD obligation, based on an exact rational LDL ⊤ factorization: theorem posSemidef_real_of_LDLt n : N M L : Matrix (Fin n) (Fin n) Q d : Fin n →Q (hd : ∀ i, 0 ≤ d i) (hM : M = L * Matrix.diagonal d * L ⊤ ) : (ratMatrixToReal M).PosSemidef := ... The lemma says that if a rational matrixMfactors asL diag(d)L ⊤ with every entry ofdnon-negative, then the entrywise real cast of M , written ratMatrixToReal M, is positive semidefinite; the Q-to-R casting happens inside the lemma. To use it, the compiler script reconstructsM t fromQ ′ t andR t in exact rational arithmetic, computes a factorizationM t =L t diag(d t )L ⊤ t withL t square and unit lower triangular, and emits M t ,L t , andd t in the generated Lean file. Lean treats the emitted factorization only as a candidate witness: thepsdrealldlttactic must prove the lemma’s two hypotheses. The non-negativity of every entry ofd t is checked withfincasesandnormnum. For the factorization equality, both sides are concrete finite matrices overQ, sodecide +kernelevaluates their decidable equality and has the Lean kernel certify that their rational entries agree. No eigenvalue or floating-point calculation enters this check. Lean does not separately compareM t with the originalQ ′ t andR t fields of the certificate; that reconstruction is performed by the unverified compiler script. An incorrectLDL ⊤ witness is therefore rejected, while fidelity to the source certificate is a separate concern discussed in Section 5.3. In either case, the emitted matrix can contribute to the final theorem only if both its PSD proof and the subsequent algebraic calculation are accepted by Lean. Lifting the target (Part 3). The first two parts provide the algebraic data used by the certificate. Part 3 aligns the target with that data when necessary. The certificate identities are expressed at the host sizeN, so when the target graphFitself hasNvertices, its basis element [F] already lives in that basis and nothing needs to be done. WhenFis smaller, the compiler proves an auxiliary identity that expands [F] over the N -vertex H-free ∅-flags, [F ] = X G∈F ∅ N G H-free p(F ; G) [G]modulo the H-free condition, with coefficients p(F ; G) given by the single-flag densities generated in Part 1. All certificates considered here have a singleton forbidden familyH=H. The generated proof invokes theflagexpandhfree N Ktactic, whereNis the host size andKis the reflection-layerSym2Graphencoding ofH. The qualifier on the identity above matters, because our development works in the ambient algebra. In the built-inH-free algebra (Remark 3.2), the restricted sum would simply be the expansion identity(2), all of whose flags areH-free there. In the ambient algebra, however, the flags containingHare nonzero basis elements, so dropping their terms cannot give a literal equality; the auxiliary identity instead says that every empty-type positive homomorphism satisfying theH-freeness condition of Definition 3.1 gives both sides the same value. Part 1 selected theH-free flags by a concrete computation onK. Bridging the two requires proving that the underlying graph of every flag that computation discarded containsHas a subgraph; the H-free condition then forces those flags’ terms to vanish, which justifies expanding over exactly the flags Part 1 emitted. From N and K alone, the tactic establishes this bridge itself. Assembling the main theorem (Part 4). Part 4 assembles the outputs of the preceding parts and realizes the chain of inequalities from Section 5.1. The certificate identity [F] + P t Q t =c·1− rsupplies its middle equality, while the non-negativity of theQ t and ofrsupplies its two inequalities. In the Mantel 37 example, there is oneQ t , namelyQ= q 1 2 (()−()) 2 y σ , andr= 1 3 · . The generated Lean proof does not definerexplicitly; it appears as the coefficientwise difference left after the two sides are expanded in a common basis. The first step is to prove [F ]≤ H [F ] + P t Q t . It uses the following general lemma: theorem forbidLEWith_add_QuadraticForm k n : N σ : FlagType (Fin k) C : ForbidCondition f g : FlagAlgebra ∅ t (M : Matrix (Fin n) (Fin n) R) (hM : M.PosSemidef) (v : FlagAlgebraVec σ n) : forbidLEWith C f g → forbidLEWith C f (g +JflagQuadraticForm M vK 0 ) := ... HereCis a predicate encoding the forbidden-subgraph setH; for a problem forbidding a single graphH, it isforbiddenCondition H, theH-freeness condition of Definition 3.1 used throughout this section. Thus, forbidLEWith C f gis the implementation-level form off ≤ H g. The lemma says that iff ≤ H g, then the inequality remains true after the non-negative downward quadratic form determined by the PSD matrixM and flag vectorvis added to the right-hand side;hMis the proof of positive semidefiniteness generated in Part 2. The proof starts from the reflexive inequality [F]≤ H [F] and applies this lemma once for each SDP block. After all blocks have been added, its conclusion is precisely [F ]≤ H [F ] + P t Q t . It remains to prove [F] + P t Q t ≤ H c·1. The compiler checks this comparison by rewriting both sides in the basis ofH-free flags at the host sizeN. When necessary, the Part 3 lemma first expands [F] to that basis. Expanding each quadratic form produces downward images of products of basis elements; the reducedownwardflagmultactic rewrites them using the multiplication and downward identities generated in Part 1. Theexpandonehfreeattactic similarly expands 1 in the same basis, dispatching on the forbidden graph exactly asflagexpandhfreedoes in Part 3. Finally, theflagsumacsortrhspipelinetactic collects the coefficients of matching basis elements. After these rewrites, the difference between the right- and left-hand sides is exactly the remainderrfrom the certificate calculation. The tacticflagnonnegchecks that its coefficients are non-negative and then uses the non-negativity of every basis element to conclude 0≤ H r. In this way, the normalization and the final non-negativity check together verify the conceptual equality [F] + P t Q t =c·1− rand the last inequality c· 1− r ≤ H c· 1. The compiler script. The compiler script performs the certificate-specific assembly. It parses the target, bound, forbidden graph, host size, and SDP blocks from the Flagmatic file. For each graph or flag represented by a compact string, it finds the isomorphic entry in Lean’s canonical enumeration; the resulting index selects the correspondingFlagAlgebrankmiconstant. The script also reconstructs the rational matrices, computes candidate exact LDL ⊤ witnesses, and determines whether the target requires lifting. From these data, the script emits one Lean source file organized according to the four parts above: the generation commands of Part 1, the matrix and flag vector declarations and PSD proofs of Part 2, the optional target expansion of Part 3, and the final theorem of Part 4. Certificates change the generated data and the number of SDP blocks, but not this proof structure. The generated file is a proof proposal that Lean checks independently, including all its intermediate propositions and its final bound. The source certificate itself is not an input to Lean, however, so this check establishes the validity of the generated theorem rather than the fidelity of the translation. The next subsection makes this boundary precise. 5.3 Trust Model There are two distinct questions of trust: is the theorem that Lean accepts valid, and is it the statement the certificate was meant to yield? For the first question, neither the SDP solver nor the compiler script is trusted for the logical validity of a theorem that Lean accepts. The complete generated files used here introduce neither axiom declarations nor sorry, so every claim is carried by a proof term Lean checks: the emitted matrices must be proved positive semidefinite, the certificate calculation must normalize to non-negative coefficients, and the final theorem must typecheck. Subject to Lean’s trusted base, erroneous data cannot make an invalid proof term valid. 38 Table 2: Certificates carried end-to-end through the compiler.His the forbidden graph,n F the number of vertices of the target graph F , N the host size, and T the number of SDP blocks. CaseH n F N TBound Mantel (edge density)K 3 2311/2 P 3 densityK 3 3313/4 C 4 densityK 3 4423/8 Edge densityK 4 2422/3 Erd ̋os pentagon (C 5 density) K 3 55324/625 Edge densityK 5 2543/4 Edge densityC 5 2541/2 For the second question, the compiler script is trusted for translation fidelity : it parses the certificate, chooses the corresponding entry in Lean’s canonical enumeration for each certificate flag, reconstructs M t =R t Q ′ t R ⊤ t , and selects the target, bound, and forbidden graph. These choices are visible in the generated declarations and theorem statement, but Lean does not prove that they faithfully reproduce the source certificate. A translation error could therefore produce a valid theorem different from the one intended. Guarding against this does not require trusting the script; it requires reading the final theorem statement. In this sense the script marks an auditability boundary, rather than a soundness gap in the generated Lean theorem. The proof obligations also use two evaluation mechanisms. Five of the seven generated files evaluated in Section 5.4, including the Erd ̋os pentagon, discharge every finite computation, from the exact matrix equalities of the PSD proofs to the enumerations and density calculations, bydecide +kernel; the kernel checks all of it, and no compiled-evaluation axiom appears. In theK 5 -free andC 5 -free edge-density certificates, kernel reduction of the generated computations was too slow to be practical, so those two files usenativedecideand additionally trust Lean’s native compiler and runtime. Finally, the custom tactics are unverified metaprograms whose dependence on elaborated expression shapes affects robustness and portability. They construct proof terms that Lean checks, so a tactic failure leaves the proof incomplete rather than establishing an invalid theorem. 5.4 Evaluation We evaluated the compiler on seven certificates spanning host sizesN ∈3,4,5, targets at and below the host size, between one and four SDP blocks, and four forbidden graphs (K 3 ,K 4 ,K 5 , andC 5 ). For each certificate, the compiler produces a complete Lean source file. All seven files compile and contain neither sorrynor generated axiom declarations. No certificate coefficient is transcribed into Lean by hand. All but theK 5 - andC 5 -free edge-density files are checked entirely bydecide +kernel; those two usenativedecide. Table 2 summarizes the seven cases; Section A reports their compilation times and peak memory under both evaluation modes. The cases play complementary roles. Mantel is a hand-checkable baseline: its single 2×2 SDP block is the explicit square from Section 5.1. Here the dimension of a block is the dimension of its certificate matrix, equivalently the length of its associated flag vector. The C 4 -density certificate has two blocks, with matrices of dimensions 4×4 and 3×3, while the Erd ̋os pentagon certificate has three blocks, with matrices of dimensions 8×8, 6×6, and 5×5. TheK 5 - andC 5 -free edge-density cases each use four blocks, all with 8×8 matrices. These certificates are Flagmatic’s output as produced, with no attempt to minimize the number of blocks or the matrix dimensions; more compact certificates for the same bounds may exist, but the unoptimized output already compiles end to end. Together, these examples exercise targets both at and below the host size, and increasingly large multi-block normalizations. TheC 5 -free edge-density case shows that the forbidden graph need not be complete; the generated file proves that graphs containing no C 5 subgraph have edge density at most 1/2. 39 The generated certificate argument establishes only the upper-bound direction. For Mantel and the Erd ̋os pentagon, the matching lower bounds are proved directly in Lean using the underlying formalization (Section 6), completing the Tur ́an densities 1 2 and 24 625 of Examples 2.7 and 2.8. Limitations. We point out three limitations of the current compiler. First, this evaluation establishes coverage of the seven cases above, not completeness of the compiler. Even a certificate within the compiler’s intended scope may expose a normalization shape not handled by the custom tactics. Such failures are safe: an unsupported or malformed input is rejected or yields an explicitly incomplete skeleton containingsorry, and a tactic failure leaves the proof incomplete, so neither case produces an unchecked theorem. Second, fully kernel-checked compilation does not yet scale. For theK 5 -free andC 5 -free edge-density certificates, we attempted to check the generated files entirely bydecide +kernel; the runs did not finish in an acceptable time and were abandoned, which is why those two files usenativedecide(Section 5.3). Third, as explained in the trust model, we do not verify translation fidelity: Lean does not check that the generated declarations faithfully transcribe the source certificate. For each of the seven evaluated certificates, however, the compiler fills the fixed proof skeleton without manual editing, and Lean checks every proof obligation in the generated file under the trust model of Section 5.3. Thus, the fidelity of the generated theorem to the source certificate remains a limitation, while the logical validity of the generated theorem itself is checked by Lean. 6 Using the Formalization Beyond Certificate Compilation The certificate compiler of Section 5 is one application of our development, not its full scope. Underlying the compiler is a reusable formalization of flag-algebra expressions, positive homomorphisms and their semantics, and the passage from finite graphs to limiting densities. These components can also be used directly, without first translating an argument into a certificate. This section illustrates three such uses. The Mantel development gives a direct flag-algebra proof and shows what it is like to work with the formalization without the compiler. The matching lower bounds for Mantel’s theorem and the Erd ̋os pentagon theorem combine explicit finite constructions with the convergence of normalized extremal numbers, completing the corresponding exact Tur ́an-density results. Finally, two inequalities of Goodman show that the same framework supports flag-algebra arguments outside the certificate problems considered in Section 5. Mantel’s theorem. Example 2.7 statesπ(K 2 ;K 3 ) = 1 2 . The Lean development records it in four statements: theorem Mantel_flag_bound : K2 ≤ (1 / 2 : R) • 1 + K3 := ... theorem Mantel_flag_bound’ : ∀ (φ : PositiveHom ∅ t ), φ K3 = 0 → φ K2 ≤ 1 / 2 := ... lemma extremal_density_K3_ge (n : N) (hn2 : n ≥ 2) : (extremalNumber n (completeGraph (Fin 3)) / n.choose 2 : R) ≥ 1 / 2 := ... theorem Mantel_Turan : turanDensity (completeGraph (Fin 3)) = 1 / 2 := ... HereK2andK3denote the basis elements [K 2 ] and [K 3 ]. The compiler of Section 5 already produces the upper bound in Mantel’s theorem. We include this separate development for a different reason: it shows what a proof looks like when one works directly with the flag-algebra formalization instead of supplying a certificate to the compiler. Accordingly, this proof uses neither the compiler nor theforbidLEinterface of Section 3.6. The direct upper-bound argument takes place in the ambient algebra and keeps the triangle contribution explicitly: K 2 ≤ 1 2 · 1 + K 3 . 40 This inequality is formalized asMantelflagbound. If a positive homomorphismφrepresents a triangle-free limit, thenφ([K 3 ]) = 0, and evaluating the displayed inequality givesφ([K 2 ])≤ 1 2 . This pointwise statement is recorded as Mantelflagbound’, and the remaining argument proceeds from it. The matching lower bound comes from the balanced complete bipartite graphK ⌊n/2⌋,⌈n/2⌉ and is formalized asextremaldensityK3ge. This graph is triangle-free: among any three vertices, two lie in the same part and are therefore non-adjacent. Its⌊n 2 /4⌋edges make up at least half of the n 2 vertex pairs. HereextremalNumberdenotes the maximum number of edges in aK 3 -free graph onnvertices. It agrees withex(n, K 2 ;K 3 ) because the induced copies ofK 2 are precisely the edges. Whenn= 2k, Lean uses completeBipartiteGraph (Fin k) (Fin k)as the witness and compares itsk 2 edges with 1 2 2k 2 . The case of oddnfollows by comparison with the next even graph size, using the fact that the normalized extremal numbers are non-increasing. Finally, the construction and the upper bound are combined inMantelTuran, using the compactness argument of Lemma 2.6 directly rather than the machinery of Section 3.6. If the normalized extremal numbers exceeded 1 2 +εfor infinitely many values ofn, we could choose extremal triangle-free graphs of those sizes and pass, by Theorem 2.5, to a convergent subsequence. Its limit would be a positive homomorphismφ withφ([K 3 ]) = 0 andφ([K 2 ])≥ 1 2 +ε, contradictingMantelflagbound’. The construction gives the lower bound 1 2 , so the normalized extremal numbers converge to 1 2 , which is the statement of MantelTuran. The Erd ̋os pentagon theorem. This example shows how an explicit construction and the passage from finite graphs to limiting densities complement a compiler-generated upper bound. The full result of Example 2.8, theorem ErdosPentagon_Turan : generalizedTuranDensity K3 C5 = 24/625 := ... is the conjunction of the upper bound of Section 5.4 and the lower bound theorem ErdosPentagon_Turan_lowerBound : generalizedTuranDensity K3 C5 ≥ 24/625 := ... proved by an explicit construction in Lean. We first describe the construction and the analytic steps mathematically, and then match them with the formal development. Since, by the convergence theoremtendstogeneralizedTuranDensityof Section 3.6, the normalized extremal numbersex(n, C 5 ;K 3 )/ n 5 converge toπ(C 5 ;K 3 ), it suffices to exhibit, for infinitely many graph sizes, one triangle-free graph whose normalized count of induced copies ofC 5 is at least 24 625 . The witness is the n-fold blow-up ofC 5 : replace each vertex ofC 5 by a class ofnvertices, and join two vertices of distinct classes exactly when the corresponding vertices ofC 5 are adjacent; vertices of a common class remain non-adjacent. The blow-up is triangle-free: adjacent vertices lie in distinct classes, so the classes of a hypothetical triangle would form a triangle inC 5 itself, which has none. It also contains many copies ofC 5 : picking one vertex from each of the five classes yields five vertices that inherit exactly the adjacencies ofC 5 , so each of the n 5 choice functions induces a copy ofC 5 . These copies are induced, as the density convention of Section 1 requires. (In a triangle-free graph, the distinction disappears anyway: everyC 5 subgraph is induced, since any chord, an edge joining two non-consecutive vertices of the cycle, would create a triangle.) The blow-up is therefore a triangle-free graph on 5n vertices with at least n 5 induced copies of C 5 , so ex(5n, C 5 ; K 3 )≥ n 5 , and normalizing gives, for every n≥ 1, ex(5n, C 5 ; K 3 ) 5n 5 ≥ n 5 5n 5 ≥ n 5 (5n) 5 /5! = 24 625 . The bound thus holds along the subsequence of graph sizes 5n, and taking the limit yieldsπ(C 5 ;K 3 )≥ 24 625 . The Lean development mirrors each step of this outline: def blowUp V : Type [Fintype V] (G : SimpleGraph V) (n : N) : SimpleGraph (V × Fin n) := Adj v w := G.Adj v.1 w.1 symm v w := by apply G.symm 41 theorem blowUp_K3_free m : N G : SimpleGraph (Fin m) (n : N) (hfree : K3.Free G) : K3.Free (blowUp G n) := ... lemma subgraphCount_blowUp_C5_ge (n : N) : subgraphCount C5 (blowUp C5 n) ≥ n 5 := ... theorem generalizedExtremalNumber_K3_C5_ge (n : N) : generalizedExtremalNumber (5 * n) K3 C5 ≥ n 5 := ... TheblowUp G nis then-fold blow-up of an arbitrary base graphG: its vertex type is the product typeV × Fin n , whose elements are the pairs (v,i) of a vertexv : Vand an indexi : Fin n, so the class of a base vertexvconsists of the pairs with first coordinatev, and theAdjfield compares first coordinates through G. Vertices of a common class are non-adjacent becauseGhas no loops, and two classes over adjacent base vertices are completely joined. TheblowUpK3freetheorem states the triangle-freeness property. Its proof transports a hypothetical triangle back to the base graph: composing a copy ofK 3 in the blow-up with the first projection gives a copy ofK 3 inG, where injectivity survives the projection because vertices of a common class are non-adjacent. InstantiatingGwithC 5 , whose own triangle-freeness is a finite check, shows that the blow-up ofC 5 is triangle-free. ThesubgraphCountblowUpC5gelemma expresses the counting property; heresubgraphCount C5 Gis the number of induced subgraphs ofGisomorphic toC 5 , matching the induced-copy convention of Section 1. The proof converts the one-vertex-per-class recipe into an injection from(Fin 5 → Fin n)into the induced copies ofC 5 in the blow-up: a choice functiongis sent to the subgraph induced on the five vertices (i,g(i)) fori : Fin 5, and distinct choice functions give distinct subgraphs. The preceding two results give a triangle-free graph on 5nvertices containing at leastn 5 induced copies of C 5 . The theorem generalizedExtremalNumberK3C5ge records the resulting finite bound ex(5n, C 5 ; K 3 )≥ n 5 . There is one additional representation step in Lean. The natural vertex set ofblowUp C5 nis the product Fin 5 × Fin n, whilegeneralizedExtremalNumbertakes its maximum over graphs onFin (5 * n). The graphblowUpfinsimply reindexes the blow-up on this latter vertex set; it is proved isomorphic toblowUp and is used as the witness. Normalizing the finite bound above and passing to the limit along the graph sizes 5n then gives ErdosPentagonTuranlowerBound. Direct Goodman inequalities. The final examples use the core flag-algebra infrastructure directly for two inequalities outside the Tur ́an-density certificate problems considered in Section 5. Both are due to Goodman [12]. The first is the algebraic lower bound K 3 ≥ K 2 · (2K 2 − 1), which bounds the triangle density from below in terms of the edge density: under a positive homomorphism with edge densitye, the triangle density is at leaste(2e−1), a quantity that becomes positive as soon ase exceeds the Mantel threshold 1 2 . The proof combines the size-three expansion ofK 2 with the Cauchy–Schwarz inequality for the downward operator, Jf gK 2 σ ≤ Jf 2 K σ ·Jg 2 K σ , which is a separate theorem in Razborov’s paper [1] and is proved in the development in this general form asCauchySchwarzinequality; here it is applied to the edge flag labeled at one endpoint. The resulting inequality is formalized as Goodmanboundontriangledensity. The second result is K 3 + K 3 ≥ 1 4 · 1, 42 whereK 3 is the empty graph on three vertices: asymptotically, at least a quarter of all vertex triples induce a triangle or an independent set. Reading a graph and its complement as the two color classes of a 2-edge-colored complete graph turns this into Goodman’s classical bound on the number of monochro- matic triangles; the proof reuses the downward square certificate of Mantel’s theorem. It is formalized as GoodmantheoremonRamseymultiplicity. Together, the examples in this section show that certificate compilation is only one use of the formalization. The same framework supports direct flag-algebra derivations, explicit finite constructions and their limiting arguments, and inequalities beyond maximizing the induced density of one graph while forbidding another as a subgraph. 7 Engineering Obstacles The specification layer of Section 3 makes explicit several proof obligations that ordinary combinatorial notation hides. A construction defined on a concrete labeled graph must be proved invariant under isomorphism before it can be lifted to flags. Because a flag’s size is part of its Lean type, identities relating flags of different sizes, such as the expansion identity, require additional type-level bookkeeping. Reusing a theorem about a tuple of flags can create a similar problem after the tuple is reordered: mathematically identical tuples need not have types that Lean identifies. Finally, finite counting depends on a chosen enumeration, and the same choice must be used consistently throughout a proof. These obligations do not change the underlying mathematics, but they recur often enough to impose a substantial proof-engineering cost. Although these difficulties often appear together, their causes differ. Invariance under isomorphism is the well-definedness condition required to define an operation on a quotient. The size and tuple-reordering issues reflect a limitation of Lean’s underlying type theory: mathematically equal types need not be definitionally equal, and therefore may require explicit casts. The enumeration issue, by contrast, is not primarily a consequence of the underlying type theory. It arises from elaboration and typeclass inference, which may synthesize different enumerations at different occurrences. The following subsections treat these obstacles separately. Counting identities present one further challenge: two density expressions may count the same configura- tions using different finite representations. Our most reliable proof method is to identify the two finite sets, construct an explicit bijection between them, and deduce equality of their cardinalities. The final subsection explains this recurring pattern. 7.1 Computing with Graphs up to Isomorphism As described in Section 3.1, a flag is an isomorphism class of concrete labeled graphs. Thus, two isomorphic labeled graphsGandG ′ may use different vertex names and be represented by different Lean values, but they denote the same flag. Representing flags by isomorphism classes is mathematically natural because subsequent statements on flags should not depend on arbitrary vertex names. At the same time, this quotient representation creates a recurring well-definedness obligation whenever a construction is first described using a concrete representative. Suppose such a construction assigns a valueA(G) to a labeled graphG. To define the corresponding value of the flag represented by G, one must prove G≃ f G ′ =⇒ A(G) = A(G ′ ). Only then is the rule [G]7→ A(G) independent of the representative. Lean packages this step asQuotient.lift. The use ofQuotient.liftis itself short; the substantive obligation is proving that the representative-level construction is invariant under isomorphism. This pattern occurs when lifting densities and graph operators to flags and also at the reflection boundary. For example, decoding an executable edge-set representation must yield the same abstract flag for every isomorphic concrete encoding. Rather than exposing the two representations in every later theorem, we prove this compatibility once and let subsequent proofs operate on the resulting flag. The same issue appears one 43 level higher when flag vectors are quotiented by the zero-space relations to formFlagAlgebra: a construction on vectors must respect those relations before it can be lifted to the algebra. One could avoid these compatibility proofs by choosing a canonical representative for every isomorphism class. That choice would make the representation easier to compute with, but it would introduce canonical- ization details into the statements and proofs of algebraic lemmas. We instead keep the quotient specification close to Razborov’s mathematics and concentrate the representation-specific work at the boundaries where a construction is lifted to equivalence classes. 7.2 Comparing Flags of Different Sizes In Lean, a flag’s size is part of its type: theσ-flags of sizeℓform the typeFlag σ (Fin ℓ), which varies withℓ. A statement comparing flags of different sizes must therefore cross between different types, a crossing that paper mathematics performs silently. The situation arises throughout the development: the expansion identity(2)equates a size-mflag with a linear combination of size-nflags, and the product formula of Equation(4)must be proved independent of its auxiliary size. This subsection explains how such cross-size statements are made and proved. Consider the expansion identity(2). Its left-hand side involves a flag of typeFlag σ (Fin m), whereas the flags on the right have typeFlag σ (Fin n). A term of the first type cannot be used where Lean expects a term of the second, and an ordinary equality can only compare terms having the same type. Thus, the identity is not merely hard to prove; as written, it is not a well-typed statement. The first formalization task is therefore to construct explicitly the common ambient space that paper mathematics leaves implicit. Mathematically, we regard every fixed-size familyF σ ℓ as part of the all-size familyF σ , and hence regard combinations of flags of different sizes as vectors in the same space. In Lean, however, the typesFlag σ (Fin ℓ)vary withℓand do not come with such a common ambient type. We therefore use the dependent sum FinFlag σ = Σ ℓ:N Flag σ (Fin ℓ). A size-m σ-flagFis therefore stored as the tagged pair⟨m,F⟩, while a size-n σ-flagGis stored as⟨n,G⟩. The second components have different types, but both tagged pairs belong to the single typeFinFlag σ. Recall thatFlagVector σis the vector space of finitely supported real-valued functions onFinFlag σ, or equivalently of finite formal real linear combinations of its elements. Thus, the two taggedσ-flags index basis vectors in the same vector space, and equations mixing flags of different sizes can be stated in that common space. The packaging provides a common home, not an identification: when their size tags differ,⟨m,F⟩and ⟨n,G⟩remain distinct elements ofFinFlag σand index distinct basis vectors. Identifying them is the quotient’s job, and it needs no further argument: the difference between the two sides of the expansion identity(2)is one of the generators of the zero space, so the identity holds in the flag algebra by definition. Later cross-size comparisons, including the independence of the product formula from its auxiliary size, reason modulo this relation. 7.3 Comparing Reordered Flag Tuples The multi-flag density is invariant under reordering its pattern flags. One instance is the symmetry p(F 0 ,F 1 ;G) =p(F 1 ,F 0 ;G), which is what makes flag-algebra multiplication commutative, since the product formula(4)expands a product of two flags into a sum weighted by exactly these pair densities. On paper, the invariance is proved once, in full generality: for any number of pattern flags, reordering the tuple does not change its density in a host. The two-flag symmetry is then read off by taking the permutation that swaps the two positions, and this instantiation is not counted as a proof step. The formalization takes the same route, and the friction appears exactly in the instantiation, a step with no counterpart on paper. Recall from Section 3.2 that a tuple of pattern flags is a dependent function: an element ofFlagList σ t Vl assigns aσ-flag on the vertex typeVl ito each indexi : Fin t, andflagListDensitycomputes the 44 multi-flag density of such a tuple in a host flag. Both the entries and their types vary with the index, and the vertex-type family Vl is itself an argument of the tuple’s type. Reordering is defined by precomposition: abbrev Perm (t : N) := Fin t ≃ Fin t def listTypePermute t : N (Vl : Fin t → Type) (π : Perm t) : Fin t → Type := fun i => Vl (π i) def FlagList.permute T : Type σ : FlagType T t : N Vl : Fin t → Type (Fl : FlagList σ t Vl) (π : Perm t) : FlagList σ t (listTypePermute Vl π) := fun i => Fl (π i) A permutationπ : Perm tis a bijection of the index setFin t. The permuted tupleFl.permute πplaces Fl (π i)at positioni, so the entry types are reordered along with the entries: the vertex-type family of the result islistTypePermute Vl π, the reordered familyfun i => Vl (π i), and it appears in the type of the result. The invariance is then proved once, for every lengthtand every permutation; the symmetry to be derived from it is the pair case: theorem flagDensity_permute T W : Type σ : FlagType T t : N Vl : Fin t → Type (Fl : FlagList σ t Vl) (G : Flag σ W) (π : Perm t) : flagListDensity Fl G = flagListDensity (Fl.permute π) G := ... theorem flagPairDensity_comm T U 0 U 1 W : Type σ : FlagType T (F 0 : Flag σ U 0 ) (F 1 : Flag σ U 1 ) (G : Flag σ W) : flagDensity 2 F 0 F 1 G = flagDensity 2 F 1 F 0 G := ... HereflagDensity 2 is the pair specialization offlagListDensity, so the second theorem states precisely the two-flag symmetry introduced at the beginning of this subsection. To derive the second statement from the first, suppose theσ-flagsF 0 andF 1 have vertex typesU 0 andU 1 , and letVlbe the vertex-type family withVl 0 = U 0 andVl 1 = U 1 , so that the two-entry flag tuple[F 0 , F 1 ] f , using theFlagListnotation introduced in Section 3.2, is an element ofFlagList σ 2 Vl. Takeπto be the permutation ofFin 2withπ(0) = 1 andπ(1) = 0. ThenflagDensitypermuteequates the density of [F 0 , F 1 ] f with that of its permuted tuple; the permuted tuple placesF 1 at position 0 andF 0 at position 1, and its vertex-type family islistTypePermute Vl π. The theoremflagPairDensitycommspeaks instead of the directly constructed pair[F 1 , F 0 ] f , an element ofFlagList σ 2 Vl’for the vertex-type familyVl’ withVl’ 0 = U 1 andVl’ 1 = U 0 . The familieslistTypePermute Vl πandVl’are pointwise equal, since both send 0 toU 1 and 1 toU 0 , but Lean need not reduce the two expressions to the same term. The family is an argument of the tuple’s type, so the permuted tuple and[F 1 , F 0 ] f inhabit types,(FlagList σ 2 (listTypePermute Vl π)) andFlagList σ 2 Vl’, that are not definitionally the same. The permuted tuple and the directly constructed pair therefore cannot yet be compared by ordinary equality. The formal proof must first establish equality of their vertex-type families and then use that equality to compare the tuples. This type-alignment step has no counterpart on paper, where the two expressions simply denote the same reordered pair. The bridging lemmaflagListDensityHEqeqpackages these requirements: if the two vertex-type families are equal and the two tuples agree after their types are aligned, then the two densities coincide. theorem flagListDensity_HEq_eq T W : Type σ : FlagType T t : N Vl 0 Vl 1 : Fin t → Type Fl 0 : FlagList σ t Vl 0 Fl 1 : FlagList σ t Vl 1 (h_Vl_eq : Vl 0 = Vl 1 ) (h_HEq : HEq Fl 0 Fl 1 ) (G : Flag σ W) : flagListDensity Fl 0 G = flagListDensity Fl 1 G := ... In this application, Vl 0 is listTypePermute Vl π and Vl 1 is Vl’, so hVleq states listTypePermute Vl π = Vl’, 45 proved by checking the two indices ofFin 2. The hypothesishHEqexpresses that the permuted tuple and the directly constructed tuple[F 1 , F 0 ] f are equal even though Lean initially assigns them different types. Concretely, both tuples place F 1 at position 0 and F 0 at position 1. The role ofhVleqis to align these two tuple types. Once their vertex-type families have been identified, hHEqcan be used as an ordinary equality, allowing one tuple to be substituted for the other. The lemma flagListDensityHEqeqthen concludes that their densities are equal. Thus, the formal argument recovers the mathematically immediate fact that permuting[F 0 , F 1 ] f produces the same pair as directly constructing [F 1 , F 0 ] f . 7.4 Controlling Finite Enumerations Lean distinguishes a proof that a type is finite from a mechanism for enumerating its elements. An instance ofFinite Tprovides only the former: it asserts thatThas finitely many elements but gives no way to visit them. An instance of Fintype T provides the latter: class Fintype (T : Type) where elems : Finset T complete : ∀ x : T, x ∈ elems The fieldelemsis aFinset T, a concrete finite set of elements ofT, andcompleteproves that every element ofTbelongs to it. The setelemscarries no mathematically significant order, but it allows generic operations to count the elements, inspect every candidate, and form finite sums and products. Thus,Fintypeis the interface needed by counting algorithms, whereasFiniterecords only the underlying finiteness fact. Every Fintypeinstance impliesFinite. In the other direction,Fintype.ofFiniteproduces aFintypeinstance from a proof of finiteness by invoking Lean’s choice axiomClassical.choice. The resulting instance is noncomputable: itselemsexists as a term that proofs can mention, and every lemma aboutFintypeapplies to it, but the definition carries no executable code, so Lean cannot evaluateelemsto list the elements ofT. This costs nothing when a proof relates cardinalities to one another by lemmas, which is how the counting below proceeds. What a noncomputable instance rules out is evaluation. Proving a concrete numeric value of Fintype.card Tby computation, or enumerating the elements executably, requires a computableFintype instance; the reflection layer (Section 4) builds its enumerations in that form. This distinction becomes especially important when formalizing cardinalities of finite sets and finite counting arguments. A setS=x:T | P(x)is represented as a predicate of typeSet T; when we count its elements, the relevant type is the subtype of termsx:TsatisfyingP(x). Lean can often infer that this subtype isFinitewithout having a particularFintypeenumeration available, but the cardinality function Fintype.cardand the lemmas about it, such asFinset.cardunivandFintype.cardcongr, require a Fintypeinstance. The elaborator does synthesizeFintypeinstances automatically; the difficulty is not obtaining an instance but obtaining the same one every time. In a development with multiple overlapping constructions (quotient types, embedded subgraphs, partial-function spaces), the same type can receive differentFintypeinstances from different elaboration paths. As sets, theirelemsfields cannot disagree, since completeforces each to contain every element of the type; what can differ is the term denoting that set. When the twoelemsterms do not reduce to a common term definitionally, the kernel rejects the goal even though the instances are provably equal. The formalization responds in two ways. The first is preventive: the moment a finite set is named, the intended instance is chosen and bound withlet, so that every later occurrence elaborates against the same binding rather than a fresh search: -- S0 and S1 are the two finite sets being counted. -- Choose and name the Fintype enumeration used for each one. let hS0 : Fintype S0 := Fintype.ofFinite S0 let hS1 : Fintype S1 := Fintype.ofFinite S1 -- h_iso_S0_S1 is a bijection between the two sets. -- The @ notation exposes the Fintype arguments that Lean normally inserts. 46 have card_eq : @Fintype.card S0 hS0 = @Fintype.card S1 hS1 := @Fintype.card_congr S0 S1 hS0 hS1 h_iso_S0_S1 -- Rewrite the toFinset counts in the goal to Fintype cardinalities. have count_eq : S0.toFinset.card = S1.toFinset.card := by -- These two toFinset terms also use hS0 and hS1, respectively. rw [Set.toFinset_card, Set.toFinset_card] exact card_eq The displayed@notation makes explicit where the two named instances enter the proof:hS0supplies the enumeration used byFintype.card S0, andhS1supplies the one used byFintype.card S1; both are also arguments ofFintype.cardcongr. The subsequentS0.toFinsetandS1.toFinsetexpressions use the same instances implicitly, as do the two applications ofSet.toFinsetcard. Thus,Set.toFinsetcard rewrites the two concrete counts to exactly the cardinality terms appearing incardeq. Without the local bindings, Lean could synthesize those hidden arguments independently at the different occurrences, producing terms that are propositionally equal but do not match for rewriting. This pattern appears inflagDensitypermutefrom Section 7.3. There,S0andS1are the sets of tuples of pairwise-disjoint induced copies that realizeFlandFl.permute π, respectively. The mathematical step is the reindexing bijectionhisoS0S1; the namedFintypeinstances ensure that the cardinality equality obtained from this bijection rewrites the counts occurring in the density definition. The flag-operator proofs use the same pattern for the isomorphism set associated with a fixed underlying graph. The second response repairs mismatches that do occur. Once the mathematical steps of such a proof are done, what remains is a goal of a characteristic shape: an equality whose two sides print identically and differ only in the inferred instances inside them. The tacticcongr!closes such goals; it decomposes the equality into congruence subgoals and discharges the instance mismatches, which is sound because any two Fintypeinstances of the same type are provably equal (Fintype Tis a subsingleton). The bridging lemma flagListDensityHEqeqof Section 7.3 is finished exactly this way: it carries aFintypeListinstance for each vertex-type family, supplying aFintypeinstance for every component type. Once the families and the tuples have been identified, the two sides of the goal differ only in theFintypeinstances supplied for the component types; congr! resolves these remaining differences. These explicitFintypechoices are needed only where finite sets are converted toFinsets or their cardinalities are compared. Once the required counting identity has been proved, the subsequent algebraic argument uses that identity without referring to the chosen instances. 7.5 Proving Counting Identities by Bijections Explicit bijections became an unexpectedly prevalent proof pattern in the specification layer. We did not set out to make bijective arguments the default: we expected many of these equalities to follow from existing counting lemmas or symbolic simplification, with explicit equivalences needed only occasionally. In practice, however, unfolding and simplifying the definitions repeatedly exposed the same structure: the two sides are cardinalities of finite sets of configurations presented in different ways. Our most reliable proof method is to identify the two sets, construct an explicit bijection between them, and use the bijection to prove equality of their cardinalities. The bijection carries the main mathematical content of the proof. Our experience proving the density chain rules (Lemma 2.2) made this pattern particularly clear. A chain rule identifies two sampling procedures: choosing the required subflags directly in the host, or making the same choice in stages through an intermediateσ-flag. On paper, these procedures are readily seen as two descriptions of the same experiment. In Lean, after unfolding the definitions, the proof came down to a bijection between the finite sets of choices made by the two procedures. This bijection yielded equality of the corresponding counts and hence the chain rule. The same method proves permutation invariance, invariance under inserting an empty flag, the downward- operator counting identities, and the adequacy of the computational subgraph representation. Although these obligations arise in different parts of the formalization, each reduces to an explicit correspondence between two finite sets. The bijection contains the mathematical argument, while the instance discipline of Section 7.4 47 handles the resulting cardinalities. We do not claim that bijections are the only possible approach, but their effectiveness across these different obligations made them our default method for finite counting identities. 8 A Meta-Theory of Ensemble Semantics The definition offorbidLEin Section 3.6 was a deliberate departure from the usual presentation of constrained flag algebras. Rather than building a new algebra for each forbidden family, it retains the same ambient algebra and imposes the forbidden-graph condition only when interpreting its elements. It considers only unlabeled positive homomorphisms satisfying that condition, applies the corresponding random-extension measure to each one, and requires the desired inequality to hold with probability one under that measure. This engineering choice exposed a mathematical problem in its own right: when does this ensemble semantics validate exactly the same typed inequalities as a flag algebra in which the constraint is built in from the beginning? This led us to develop a separate mathematical meta-theory. This section gives the definitions and main results needed to state that answer; a forthcoming paper will present the full theory and its applications. The constrained positive-homomorphism space. LetGbe the class of all finite simple graphs, letK⊆G be a hereditary class, and fix a flag typeσ. Here hereditary means closed under taking induced subgraphs: ifG∈KandS ⊆ V(G), thenG[S]∈K. In particular, theH-free classes used earlier are hereditary, because taking an induced subgraph cannot create a new subgraph isomorphic to H. To make the underlying graph class explicit, we writeA σ [G] for the ambientσ-typed flag algebra andA σ [K] for the algebra constructed using only graphs inK. Onlyσ-flags whose underlying unlabeled graphs belong toKoccur in this constrained algebra. BecauseKis hereditary, the remainingσ-flags, whose underlying graphs lie outsideK, span an ideal, 4 and the usual constrained algebra is canonically isomorphic to the quotient of the ambient algebra by this ideal. We therefore have a canonical quotient map q σ :A σ [G]↠A σ [K] that sends everyσ-flag outsideKto zero and every remainingσ-flag to its counterpart in the constrained algebra. Let X σ := Hom + A σ [G],R be the compact space of positive homomorphisms on the ambient algebra, with the topology of pointwise convergence onσ-flags. Pullback alongq σ embeds the positive homomorphisms of the constrained algebra into X σ . Its image is Q σ := ψ◦ q σ ψ ∈ Hom + A σ [K],R ⊆ X σ .(8) Thus, Q σ is the space of all σ-typed positive homomorphisms admitted by the constrained quotient. There is also an intrinsic description: Q σ =χ∈ X σ | χ([F ]) = 0 for every σ-flag F whose underlying graph lies outside K.(9) The inclusion from left to right is immediate. Ifχ=ψ◦ q σ belongs toQ σ , thenq σ ([F]) = 0 for everyσ-flag F outside K, and hence χ([F ]) = 0. For the reverse inclusion, suppose thatχ∈ X σ vanishes on everyσ-flag outsideK. Here heredity ensures that the span of these flags is an ideal. Everyσ-flagFappearing in the product of aσ-flagF ′ outsideK with anotherσ-flagF ′ containsF ′ as an induced subflag. The flagFmust therefore also lie outsideK, since otherwise heredity would imply that the underlying graph ofF ′ lies inK. Thus, the span of the flags outsideKis precisely the ideal killed byq σ . The homomorphismχvanishes on this ideal and therefore factors throughq σ as a positive homomorphism on the constrained algebra. Henceχ ∈ Q σ , proving the 4 Here an idealIis a linear subspace of the flag algebra that is also closed under multiplication by arbitrary algebra elements. Thus,Iis closed under addition and real scalar multiplication, and ifx∈ Iandabelongs to the flag algebra, thenax∈ I. This property makes the quotient by I an algebra in which every element of I is identified with zero. 48 reverse inclusion. Equation(9)also shows thatQ σ is closed inX σ , since it is an intersection of zero sets of continuous evaluation maps. We writeQ 0 :=Q ∅ for the corresponding space of constrained empty-type positive homomorphisms. Random extensions and the root-planting space. Assume thatσis non-degenerate forK: that is, there is someφ 0 ∈ Q 0 for whichφ 0 (⟨σ⟩ 0 )>0. By Razborov’s random-extension result recalled in Section 2.5, every suchφ 0 determines a unique probability measureExt σ (φ 0 ) onX σ . It is obtained by choosing a uniformly random occurrence ofσin each member of a graph sequence converging toφ 0 and passing to the limit. For a probability measureμonX σ , its supportsupp(μ) consists of those pointsχ∈ X σ for which every open neighborhood of χ has positive μ-measure. Define S σ := [ φ 0 ∈Q 0 φ 0 (⟨σ⟩ 0 )>0 supp Ext σ (φ 0 ) ⊆ X σ .(10) Thus, to formS σ , we first collect the supports ofExt σ (φ 0 ) over allφ 0 ∈ Q 0 for whichσhas positive density. We then take the closure inX σ , adding every point that can be approximated arbitrarily closely by points in those supports. The support of each random-extension measure is contained in the constrained space: supp Ext σ (φ 0 ) ⊆ Q σ φ 0 ∈ Q 0 ,φ 0 (⟨σ⟩ 0 ) > 0 . Indeed, letFbe aσ-flag outsideK. Applying the downward operator to [F] produces a non-negative multiple of [F| ∅ ], whose underlying graph also lies outsideK. Everyφ 0 ∈ Q 0 evaluates [F| ∅ ] to zero. Therefore, if φ∼ Ext σ (φ 0 ), the random-extension identity in Equation (6) gives E[φ([F ])] = 0. Since every positive homomorphismφ ′ satisfiesφ ′ ([F])≥0, it follows that forφ ∼ Ext σ (φ 0 ), we have φ([F]) = 0 with probability one. Applying this argument to the countable collection ofσ-flags outsideK shows that a positive homomorphism sampled fromExt σ (φ 0 ) belongs toQ σ with probability one. SinceQ σ is closed, Equation (10) yields the fundamental inclusion S σ ⊆ Q σ .(11) We say that (G,K,σ) is root-plantable 5 when S σ = Q σ . Definition 8.1 (Quotient and ensemble orders). For f,g ∈A σ [G], define f ≤ quot K,σ g ⇐⇒ χ(f )≤ χ(g) for every χ∈ Q σ , and f ≤ ens K,σ g ⇐⇒Ext σ (φ 0 ) χ∈ X σ | χ(f )≤ χ(g) = 1 for every φ 0 ∈ Q 0 with φ 0 (⟨σ⟩ 0 ) > 0. The first is the ordinary semantic order in the constrained quotient algebra: equivalently, every positive homomorphismψ:A σ [K]→ Rsatisfiesψ(q σ (f))≤ ψ(q σ (g)). The second quantifies over eachφ 0 ∈ Q 0 on its right-hand side. For such aφ 0 , the measureExt σ (φ 0 ) is the probability distribution onX σ obtained by taking 5 The vertices distinguished by the flag typeσare often called the roots, which explains the first part of the term root-plantable. A finiteσ-flag (G,θ) records a profile ofσ-flag densities relative to a specified embeddingθ:σ → G, whose image consists of the labeled vertices. To plant this profile in a larger graphH ∈K, without specifying labels in advance, is to produce many embeddings b θ :σ → Hwhose profiles ofσ-flag densities approximate the profile specified by (G,θ). Here “many” means that these embeddings form a fraction bounded away from zero of all embeddings ofσinH. Consequently, a uniformly chosen occurrence ofσreproduces the prescribed profile with non-vanishing probability. The equalityS σ =Q σ says that every constrained σ-typed positive homomorphism can be approximated by finite constructions of this kind. 49 a sequence of finite graphs converging toφ 0 , choosing uniformly at random an embedding ofσinto each of them, using the embedded vertices as labels, and passing to the limit. Thus, the second display requires that the random positive homomorphismχ∼ Ext σ (φ 0 ) satisfyχ(f)≤ χ(g) with probability one. For the H-free class, consisting of graphs containing no subgraph isomorphic toH,forbidLE H f gin our Lean formalization implements this ensemble order. The corresponding notions of non-negativity are 0≤ quot K,σ f and 0≤ ens K,σ f . Theorem 8.2 (Support-closure criterion). LetKbe hereditary and letσbe non-degenerate forK. For every f,g ∈A σ [G], f ≤ quot K,σ g=⇒ f ≤ ens K,σ g. Moreover, the two orders agree for every pair (f,g) if and only if the class is root-plantable at σ: ∀f,g, f ≤ quot K,σ g ⇐⇒ f ≤ ens K,σ g ⇐⇒ S σ = Q σ . The proof explains why the equalityS σ =Q σ is exactly the condition under which the two orders agree. Evaluation ofg− fdefines a continuous functionχ7→ χ(g− f) onX σ . Almost-sure non-negativity under a measure is equivalent to non-negativity on its support; continuity then shows that non-negativity in the ensemble semantics is exactly non-negativity onS σ . Non-negativity in the quotient semantics is, by definition, non-negativity onQ σ . The inclusion in Equation(11)proves the forward implication, andS σ =Q σ proves equivalence. The necessity of root-plantability requires more than this observation. IfS σ ⊊ Q σ , chooseχ ∗ ∈ Q σ \ S σ . Topological separation gives a continuous function that is strictly positive onS σ and strictly negative at χ ∗ . The Stone–Weierstrass theorem then approximates this function by evaluation of a flag-algebra element. The resulting element is non-negative in the ensemble semantics but not in the quotient semantics, so the two orders cannot agree for all elements. Thus, Theorem 8.2 is a completeness theorem: quotient proofs are always sound for ensemble semantics, and they capture all ensemble-valid typed inequalities exactly under root-plantability. When root-plantability holds. The criterion in Theorem 8.2 reduces semantic completeness to a structural problem about the graph class. Our main positive result gives a broad answer. GivenG∈K, a vertexv ∈ V(G), and a graphJ, writeG[v 7→ J] for the graph obtained by replacingvbyJ, keeping the edges insideJ, and joining every vertex ofJto every former neighbor ofv. CallKblow-up-closed if, for everyG ∈ K,v ∈ V(G), andN ∈ N, some graphJon exactlyNvertices satisfiesG[v 7→ J]∈ K. For a hereditary class, this is equivalent to asking only for|J|≥ N: choose an inducedN-vertex subgraphJ ′ ofJ, and observe thatG[v 7→ J ′ ] is an induced subgraph ofG[v 7→ J]. The interior graphJmay depend onG,v, and N ; the definition requires the existence of a suitable interior, not that every interior works. Theorem 8.3 (Blow-up closure implies root-plantability). Every blow-up-closed hereditary graph class is root-plantable at every nonempty flag type that is non-degenerate for the class. The empty flag type is root-plantable for every hereditary graph class, independently of blow-up closure. Consequently, quotient and ensemble orders agree at every non-degenerate flag type in a blow-up-closed class. The proof starts from a targetχ ∈ Q σ , represented by a sequence of finiteσ-flags whose underlying graphs lie inK. For each suchσ-flag (G,θ), the proof applies the preceding replacement construction once for each vertex ofG: the verticesv ∈ V(G) are replaced one at a time by graphsJ v , and at every step blow-up closure supplies an interior for which the current graph remains inK, so the final blow-up also lies inK. The resulting blow-up has a natural projection back toG: every vertex ofJ v is mapped tov. We callV(J v ), the inverse image of v under this projection, the fiber over v. The fibers over the labeled verticesθ(i) are made large enough that a uniformly chosen embedding ofσ places each labeliin the corresponding fiber with probability bounded away from zero. When a fixed finite σ-flag is sampled from the blow-up, its sampled vertices lie in distinct fibers with probability tending to one. On this event, their adjacencies are determined by the corresponding vertices ofG, so the internal structure of the replacement graphs J v does not affect the sampled σ-flag. 50 These estimates connect the finite blow-up construction to the definition ofS σ . LetUbe any open neighborhood ofχinX σ . BecauseX σ has the topology of pointwise convergence onσ-flags, membership inUcan be ensured by approximating the values of finitely manyσ-flags within a prescribed tolerance. Choose (G,θ) sufficiently far along the sequence representingχ, and then choose its blow-up sufficiently large. The construction ensures that a positive fraction of the embeddings ofσinto the blow-up produceσ-typed density profiles lying inU: the labeled vertices enter the designated fibers with probability bounded away from zero, while the distinct-fiber estimate preserves the required σ-flag densities. Passing to a limit of these unlabeled blow-ups gives some φ 0 ∈ Q 0 for which Ext σ (φ 0 )(U ) > 0. Therefore,Uintersectssupp(Ext σ (φ 0 )). Since every neighborhoodUofχhas this property,χlies in the closure of the union of these supports, namelyS σ . HenceQ σ ⊆ S σ , while the opposite inclusion is Equation (11). Independent blow-ups, in which every replacement graphJ v is an independent set, cover allK r -free classes forr ≥3, including triangle-free graphs. Complete blow-ups, in which everyJ v is a clique, cover, for example, graphs whose connected components are cliques. Both are instances of Theorem 8.3. Why the criterion is nontrivial. Heredity alone does not imply root-plantability. LetKbe the class ofC 4 -free graphs, those containing noC 4 as a subgraph, and letσ 1 be the one-vertex type. Every large C 4 -free graph haso(n 2 ) edges, so a vertex chosen uniformly at random has normalized degree tending to zero. Let d∈A σ 1 [G] be the flag-algebra element represented by the following two-vertex σ 1 -flag: d := 1 The filled vertex carries label 1, and the open vertex is unlabeled. Thus, the density ofdin a finiteσ 1 -flag is the normalized degree of its labeled vertex: the probability that one additional uniformly sampled vertex is adjacent to it. The preceding observation implies that everyχ∈ S σ 1 satisfiesχ(d) = 0, so−dis non-negative in the ensemble semantics. On the other hand, arbitrarily large stars areC 4 -free: the starK 1,t consists of one vertex, its center, adjacent totpairwise non-adjacent leaves, and contains no cycle at all. Label the center of K 1,t to obtain aσ 1 -flag, and letχ ∗ ∈ Q σ 1 be the positive homomorphism arising as the limit of this sequence ofσ 1 -flags. Every leaf is adjacent to the center, soχ ∗ (d) = 1. Since every point ofS σ 1 evaluatesdto zero, χ ∗ /∈ S σ 1 , and hence S σ 1 ⊊ Q σ 1 .(12) Moreover,χ ∗ (−d) =−1<0, so−dfails to be non-negative in the quotient semantics. The example exhibits a genuine gap between the two typed orders: quotient semantics permits a specially chosen vertex to carry the label, whereas ensemble semantics obtains the labeled vertex by uniform random sampling. The gap does not invalidate the final unlabeled density bounds of this paper. The certificate pipeline consumes its typed inequalities only through the downward operator, which preserves non-negativity in the ensemble semantics (downwardpreservesemanticCone, Section 3.5). Its conclusions land at the empty flag type, which is root-plantable for every hereditary class by Theorem 8.3. The final conver- sion (generalizedTuranDensityleofforbidLE, Section 3.6) then turns these conclusions into classical statements about Tur ́an densities. Root-plantability is therefore not a hypothesis of any of these results. It concerns only the completeness of the intermediate typed calculus, whether typed ensemble reasoning proves exactly the typed inequalities of the constrained algebra. Formalization and scope. The Lean formalization of the meta-theory presented in this section is included in the public release of our flag-algebra development linked in Section 1, under the module LeanFlagAlgebras.MetaTheory. The constrained spaceQ σ in Equation(8), the root-planting spaceS σ in Equation(10), and the conditionS σ =Q σ are formalized asQσ,Sσ, andRootPlantable, respec- tively. The special cases 0≤ quot K,σ fand 0≤ ens K,σ fof the two orders in Definition 8.1 are formalized as 51 QuotientNonnegandEnsembleNonneg, respectively; the general comparisonf ≤ gis expressed by applying these predicates tog− f. At the theorem level,quotientimpliesensembleformalizes the unconditional implication in Theorem 8.2, whilesupportcriterionformalizes its characterization of when the two orders agree;blowupClosedrootplantableandheredClassemptyTyperootPlantableformalize, respectively, the nonempty-type and empty-type claims of Theorem 8.3; andc4freenotrootPlantable, together with SσsubsetQσ, formalizes the strict inclusion in Equation (12). These Lean files were generated by Claude Code from an already-developed mathematical account and its theorem targets. Lean checks the resulting proof terms, and the released development builds without incomplete proofs. This autoformalization was feasible because it extended, rather than rebuilt, the manual formalization reported in the preceding sections. The manual library had already fixed the representations and semantic interfaces and provided the ambient flag algebra, positive-homomorphism spaces, random extensions, the downward operator, and the density and representation theorems on which the meta-theory depends. The generated meta-theory files could therefore focus on the new constrained layer, beginning with the forbidden ideal and constrained quotient, while reusing these established foundations. The present section isolates the core meta-theoretic consequences offorbidLE: quotient inequalities always imply ensemble inequalities, root-plantability characterizes when the converse holds, and blow-up closure is a broad sufficient condition for root-plantability. A forthcoming paper will give the complete mathematical and formal account and pursue three extensions. First, it will develop the finite planting criterion. For every fixed flag size and error tolerance, this criterion asks that each sufficiently large finiteσ-flag in the class admit a larger graph in the class with a positive-density set ofσ-embeddings that reproduce, to the specified accuracy, all of itsσ-flag densities up to that size. This finite condition implies root-plantability. Second, the forthcoming work will study further graph classes for which quotient and ensemble semantics agree or disagree. A representative source of disagreement is a pinning obstruction: every admissible random-extension measure forces the density of a particularσ-flag to one value almost surely, while the constrained quotient contains a positive homomorphism assigning it a different value. Third, it will develop relative ensemble semantics for arbitrary sets of admissible unlabeled positive homomorphisms, allowing non-hereditary limit constraints such as fixing the edge density. 9 Open Design Questions The formalization and end-to-end certificate proofs presented above are fully checked in Lean. This section instead concerns design questions whose broader consequences cannot be settled by the present implementation alone: when forbidden-graph constraints should enter the theory, which engineering costs are specific to Lean, whether specification and computation should use separate representations, and how far the current computational layer can scale. For each question, we distinguish what the present development demonstrates from what would require alternative implementations or larger computations to determine. When should a forbidden-graph constraint enter the formalization? The predicateforbidLE (Section 3.6) keeps the ambient flag algebra independent of the forbidden graph and imposes the constraint later, when a semantic inequality is stated. Razborov’s universal-theory presentation instead incorporates the constraint into the construction of the flags, algebras, and positive homomorphisms. Consequently, the two approaches give different semantics to intermediate inequalities involving labeled flags: the former restricts their interpretations, whereas the latter removes inadmissible flags through the constrained algebra. As Theorem 8.2 shows, this distinction disappears precisely when the underlying hereditary class is root-plantable; in that case, the two semantics validate the same typed inequalities. Even without root-plantability, every quotient inequality implies the corresponding ensemble inequality. This one-way implication is sufficient for transferring the formal flag-algebra inequalities used here to the final unlabeled Tur ́an bounds. These semantic results do not by themselves determine which design is preferable in a proof assistant. Even when root-plantability ensures that the two semantics validate the same inequalities, the implementations may have different proof-engineering costs. Deferring the constraint allows core definitions and algebraic 52 lemmas to be reused across forbidden graphs; incorporating it at the outset may streamline arguments specific to a fixed extremal problem. Evaluating this tradeoff would require formalizing comparable certificate proofs under both designs. Which engineering obstacles are Lean-specific? Section 7 includes both obligations common to quotient-based formalizations and difficulties tied more closely to Lean. If flags are represented as isomorphism classes, a construction first defined on labeled graphs must be proved invariant under isomorphism before it can be applied to flags. The same well-definedness obligation would arise in any proof assistant using this representation. The remaining difficulties have causes more closely tied to Lean. Binding a particular Fintypeinstance is needed because Lean’s elaborator may synthesize different instance terms for different occurrences of the same carrier type. The use ofHEqreflects Lean’s dependent type theory: pointwise-equal type families need not be definitionally equal, so terms indexed by them cannot immediately be compared using ordinary equality. Other proof assistants handle finite enumeration, implicit arguments, and dependent equality differently. We therefore do not know which of these Lean-specific proof-engineering techniques would be needed in a port to Rocq, Agda, or Isabelle/HOL. The underlying combinatorial identities and the well-definedness obligations created by quotient representations would remain, but their formal expression and proof cost could differ. Should specification and computation use separate representations? Our development maintains two representations (Sections 3 and 4). The specification layer uses quotients and definitions close to the mathematics, allowing the abstract theory to ignore choices of graph representatives. The reflection layer uses the concreteSym2Graphrepresentation to evaluate finite densities, downward coefficients, and multiplication tables. Adequacy theorems connect the two, turning these evaluations into facts about the specification-level definitions. The density and multiplication facts used throughout our case studies are obtained in this way. This separation lets us keep the abstract development simple while retaining an efficient executable representation. It also creates a substantial bridge of adequacy proofs. One alternative is to state the theory directly on a concrete, canonical representation: this would reduce the bridge, but representation and canonicalization choices would become visible in the statements and proofs of the abstract theory. We have not carried this alternative through comparable case studies, so we do not know which architecture minimizes the total proof and computation cost. Can the computational layer scale beyond five vertices? Our seven end-to-end certificates (Section 5.4) expand their calculations over graphs on three, four, or five vertices. At this scale, the optimized enumeration of Section 4.3, size-inductive, deduplicated, and pruned under the forbidden graph, keeps the required families of finite identities manageable. For the Erd ̋os pentagon certificate, whose calculations expand over five-vertex graphs, the three flag types require 1800, 672, and 360 pair-density theorems, respectively. Lean checks all 2832 identities bydecide +kerneland then uses the resulting theorems in the complete certificate proof. This confirms that certificates at the five-vertex scale do go through the current reflection and automation layers, though only just: the Erd ̋os pentagon is the largest certificate carried entirely on the kernel-checked path. Going substantially beyond five vertices remains a major engineering challenge. As the number of vertices grows, so do the families of flags, the density and multiplication identities generated from their pairs, and the expressions that the final algebraic proof must normalize. The cost of kernel-checked evaluation grows with them: already at five vertices, the two largest certificates, with 10,332 and 8,172 pair-density theorems, could not be checked bydecide +kernelin acceptable time and fall back tonativedecide(Table 3), and eliminating that fallback is part of the same scaling problem. Scaling to larger certificates will therefore likely require more efficient executable graph representations and counting algorithms in the reflection layer, as well as improvements to theorem generation and algebraic normalization. This ceiling is not unique to formal verification: certificate generation itself faces the same combinatorial growth, and Flagmatic is in practice limited to expanding its calculations in the basis of graphs on about seven or eight vertices. The formal 53 pipeline reaches its limit earlier, and we have not yet determined which of its costs dominates or how much of the gap such optimizations can close. 10 Related Work Formalizations of combinatorics. Substantial combinatorial arguments have already been formalized in Lean. Dillies and Mehta formalized Szemer ́edi’s regularity lemma and the qualitative form of Roth’s theorem [10], and Mehta the Kruskal–Katona theorem [13]. Subercaseaux et al. [14] verified the empty-hexagon number against a SAT certificate. The collaborative PFR project [16] formalized the Gowers–Green–Manners– Tao proof [15] of the polynomial Freiman–Ruzsa conjecture in characteristic two. These developments lean on heavy computation or on a large supporting library. A flag-algebra argument needs both at once: it combines quotient and measure-theoretic semantics with thousands of exact finite-density computations and an externally computed semidefinite certificate. Proof by reflection in proof assistants. Proof by reflection is a classical technique in the Rocq (previously called Coq) community; Chlipala gives an extended treatment [19], and Lean supports verified computation through tactics such asdecideandnormnum. Cohen et al. [20] develop a systematic methodology for building efficiently computable representations alongside their abstract counterparts in Rocq. Our Sym2Graph/SimpleGraphpair with its adequacy theorems follows the same philosophy, adapted to Lean 4’s type-class and instance-search mechanism. Computer-assisted flag algebra arguments. The Flagmatic software [18] automates the computation of exact and approximate flag-algebra bounds, but it does not produce proof-assistant proof terms; Razborov’s survey [2] organizes many early applications of the method. Our work adds a proof-producing reconstruction stage: certificate data proposes a calculation, while Lean verifies the finite identities, the positive-semidefinite matrices, and the final combinatorial statement. A concurrent formalization of local flag algebras. Concurrently with and independently of our work, Davey, Hurley, de Joannis de Verclos, Kang, and Volec formalized in Lean 4 the theory of local flag algebras introduced in their accompanying paper [28] and applied in its companion [29]. The local calculus normalizes densities by the maximum degree ∆ rather than by the number of vertices, so that the method still yields nontrivial bounds for sparse graphs of small maximum degree. Under this normalization, no quotient is taken: their algebra is defined directly on formal combinations of isomorphism classes, evaluation at a finite graph is multiplicative only up to an error bounded by a constant multiple of 1/∆, and positivity is again captured by a semantic cone. Their formalization machine-certifies the new bounds of both papers, on pentagon counts in triangle-free graphs [28] and on the strong chromatic index [29]. Independently, their design arrives at the reflection pattern of Section 4: a noncomputable specification mirrored by a computable Boolean-adjacency representation with adequacy lemmas. Our development formalizes the classical theory instead (the quotient algebra, positive homomorphisms, and the ensemble semantics) and is organized as a reusable library and proof-generating pipeline rather than around individual bounds, so the two developments are complementary in both scope and design. A concurrent formalization of computational flag algebras. A further concurrent development is Spiegel’s computational flag algebras in Lean [30]. It is an independent ongoing work on the Lean formalization of the flag algebras, which focuses on carrying out flag-algebra inequality proofs fully and automatically inside Lean, without relying on an external tool or solver. SDP certificate verification. The verification of SDP certificates has been studied for sum-of-squares proofs, which relax polynomial optimization problems to semidefinite programs, as studied by Parrilo and Sturmfels [22]. Harrison [21] verifies sum-of-squares certificates for polynomial inequalities in HOL Light, 54 with numerical methods finding the certificates and the proof assistant checking them. Morrison’ssostactic, recently added under the officialleanproverorganization [23], implements Harrison’s procedure in Lean 4: it finds a certificate with an external semidefinite solver, rounds it to rational form, and verifies it through an LDL ⊤ factorization. We use the same discovery-versus-verification separation, applied to flag-algebra certificates rather than polynomial inequalities. Graph limits and Tur ́an densities. The mathematical foundation of flag algebras (convergent graph sequences, positive homomorphisms, the graphon limit) is developed in depth by Lov ́asz and Szegedy and by Lov ́asz [26,25]. Freer has independently formalized a substantial graphon theory in Lean 4, including cut distance, weak regularity, counting and inverse-counting lemmas, compactness, and the equivalence of two notions of convergence [27]. Our development works with convergent flag sequences, positive homomorphisms, and random extensions rather than graphons; connecting the two formalizations into a common formal account of the flag-algebra/graphon correspondence remains future work. 11 Conclusion We have developed a Lean 4 formalization of Razborov’s flag algebra method for simple graphs. Its specification layer represents flags as quotients modulo isomorphism, constructs the quotient algebra of density-expansion relations, defines positive homomorphisms and the semantic non-negativity cone, and introduces the ensemble semantic order, which imposes forbidden-subgraph constraints only when algebra elements are compared. On top of this specification, an executable reflection layer computes finite flag data and connects these computations to the abstract definitions through adequacy theorems, while a certificate-to-proof compiler uses the resulting identities to reconstruct Lean proofs from externally generated flag-algebra certificates. We evaluated the compiler on seven upper-bound certificates: Mantel’s theorem, bounds on theP 3 - and C 4 -densities of triangle-free graphs, the Erd ̋os pentagon theorem, and edge-density bounds forK 4 -free,K 5 -free, andC 5 -free graphs. The formalization also supports proofs written directly against its mathematical interface: we used it to prove the matching lower bounds for Mantel’s theorem and the Erd ̋os pentagon theorem, as well as two inequalities of Goodman. Finally, we summarized a separately developed mathematical meta-theory comparing the ensemble and quotient semantics. Non-negativity in the quotient semantics always implies non-negativity in the ensemble semantics, while the converse holds for every typed expression exactly when the constrained class is root-plantable at that flag type. We do not claim to have found the uniquely right way to formalize flag algebras. Our aim has instead been to make the development’s design choices and their consequences explicit: the engineering obstacles they create, the executable and automation layers needed to address those obstacles, the proof patterns that may transfer to other formalizations, and the questions that remain open. Some engineering decisions reflect what is computationally feasible in the current implementation rather than a principled design preference. Most notably, the two largest certificates still use nativedecide; we have stated this trust tradeoff explicitly. We expect the architecture to support additional parts of Razborov’s flag-algebra calculus, especially the differential structure developed in Section 4.3 of his original paper [1]. Formalizing this structure would test how much of the existing quotient-level semantics and finite-counting infrastructure can be reused beyond the certificate arguments considered here. We have also not tested whether the architecture extends to richer combinatorial structures, such as hypergraphs, directed graphs, and oriented graphs. Other directions for future work include building a formal bridge between our positive-homomorphism semantics and graphon theory. In particular, the representation of every positive homomorphism by a graphon would connect our development more directly to the Lov ́asz theory [25] and to the existing Lean graphon formalization [27]. Automating the discovery of SDP certificates within Lean, rather than importing them from external solvers, is a longer-term goal. More immediately, extending thedecide +kernelpath from the five certificates it currently covers to the two certificates that still usenativedecide, or replacing the latter with a formally verified external checker, would eliminate the remaining dependency on Lean’s native compiler. This dependency is a feasibility constraint of the current encoding, not a logical limitation of the method. 55 Use of AI Assistance The layers of this development used AI assistance to different degrees. The specification and reflection layers of Sections 3 and 4, including the quotient constructions, their interface theorems, and the adequacy proofs, were formalized manually by the authors. In the certificate-to-proof compiler of Section 5, most of the required metaprogramming, including the elaboration-time generation commands, the custom tactics, and the certificate compiler, was developed with the help of Claude Code. Finally, the mathematical results of the meta-theory summarized in Section 8 were obtained with the help of GPT Pro, and their Lean development was autoformalized entirely by Claude Code. We also used Codex and Claude Code to assist with writing and revising this paper. Acknowledgments We would like to thank Jineon Baek, Taeyoung Kim, Hyunwoo Lee, Joonkyung Lee, Christoph Spiegel, and Jan Volec for helpful discussions on Razborov’s flag algebras and their Lean formalization. We are also grateful to Ross Kang and Sidharth Hariharan for encouraging us to work harder to removenativedecide in our Lean formalization. This work was supported by the National Research Foundation of Korea (NRF) grant funded by the Korean Government (MSIT) (No. RS-2023-00279680) and by the Institute for Basic Science (IBS-R029-C1). References [1] A. A. Razborov.Flag algebras.Journal of Symbolic Logic, 72(4):1239–1282, 2007. DOI: 10.2178/jsl/1203350785. [2]A. A. Razborov. Flag algebras: An interim report. In R. L. Graham, J. Neˇsetˇril, and S. Butler, editors, The Mathematics of Paul Erd ̋os I, 2nd ed., pages 207–232. Springer, 2013. DOI: 10.1007/978-1-4614- 7254-416. [3] A. Grzesik. On the maximum number of five-cycles in a triangle-free graph. Journal of Combinatorial Theory, Series B, 102(5):1061–1066, 2012. DOI: 10.1016/j.jctb.2012.04.001. [4]H. Hatami, J. Hladk ́y, D. Kr ́al’, S. Norine, and A. Razborov.On the number of pentagons in triangle-free graphs. Journal of Combinatorial Theory, Series A, 120(3):722–732, 2013. DOI: 10.1016/j.jcta.2012.12.008. [5]A. A. Razborov. On the minimal density of triangles in graphs. Combinatorics, Probability and Computing, 17(4):603–618, 2008. DOI: 10.1017/S0963548308009085. [6] A. A. Razborov. On 3-hypergraphs with forbidden 4-vertex configurations. SIAM Journal on Discrete Mathematics, 24(3):946–963, 2010. DOI: 10.1137/090747476. [7]R. Baber and J. Talbot. New Tur ́an densities for 3-graphs. Electronic Journal of Combinatorics, 19(2):#P22, 2012. DOI: 10.37236/2360. [8] J. Balogh, P. Hu, B. Lidick ́y, and F. Pfender. Maximum density of induced 5-cycle is achieved by an iterated blow-up of 5-cycle.European Journal of Combinatorics, 52:47–58, 2016. DOI: 10.1016/j.ejc.2015.08.006. [9] J. Balogh, P. Hu, B. Lidick ́y, F. Pfender, J. Volec, and M. Young. Rainbow triangles in three-colored graphs. Journal of Combinatorial Theory, Series B, 126:83–113, 2017. DOI: 10.1016/j.jctb.2017.04.002. [10]Y. Dillies and B. Mehta. Formalising Szemer ́edi’s regularity lemma in Lean. In Proc. ITP 2022, LIPIcs 237, pages 9:1–9:19, 2022. DOI: 10.4230/LIPIcs.ITP.2022.9. 56 [11] W. Mantel, Problem 28, Wiskundige Opgaven, 10:60–61, 1907. [12] A. W. Goodman. On sets of acquaintances and strangers at any party. The American Mathematical Monthly, 66(9):778–783, 1959. DOI: 10.2307/2310464. [13]B. Mehta. Formalising the Kruskal–Katona theorem in Lean. In Intelligent Computer Mathematics (CICM 2022), LNCS 13467, pages 75–91, 2022. DOI: 10.1007/978-3-031-16681-55. [14] B. Subercaseaux, W. Nawrocki, J. Gallicchio, C. Codel, M. Carneiro, and M. J. H. Heule. Formal verification of the empty hexagon number. In Proc. ITP 2024, LIPIcs 309, pages 35:1–35:19, 2024. DOI: 10.4230/LIPIcs.ITP.2024.35. [15]W. T. Gowers, B. Green, F. Manners, and T. Tao. On a conjecture of Marton. Annals of Mathematics, 201(2):515–549, 2025. DOI: 10.4007/annals.2025.201.2.5. [16]A. Anderson et al. Formalization of the polynomial Freiman–Ruzsa conjecture of Marton. Formalization project, version 0.1.0, 2023. https://teorth.github.io/pfr/. [17] E. R. Vaughan. Flagmatic user’s guide, version 1.5, 2012. Distributed with the Flagmatic software; archived copy of the distribution site athttps://web.archive.org/web/20160112235442/http:// flagmatic.org/. [18] E. R. Vaughan. Flagmatic 2.0. Computer software, 2013. Archived copy available athttps://github. com/jsliacan/flagmatic-2.0. [19]A. Chlipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. [20]C. Cohen, M. D ́en`es, and A. M ̈ortberg. Refinements for free! In Proc. CPP 2013, LNCS 8307, pages 147–162, 2013. DOI: 10.1007/978-3-319-03545-110. [21]J. Harrison. Verifying nonlinear real formulas via sums of squares. In Proc. TPHOLs 2007, LNCS 4732, pages 102–118, 2007. DOI: 10.1007/978-3-540-74591-49. [22]P. A. Parrilo and B. Sturmfels. Minimizing polynomial functions. In Algorithmic and Quantitative Real Algebraic Geometry, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 60, pages 83–99, 2003. [23]K. Morrison. Harrison’s sum-of-squares decision procedure for nonlinear real arithmetic in Lean 4. Computer software, 2026. https://github.com/leanprover/sos. [24]G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and L. de Moura. A metaprogramming framework for formal verification. Proc. ACM Program. Lang., 1(ICFP):34:1–34:29, 2017. DOI: 10.1145/3110278. [25]L. Lov ́asz. Large Networks and Graph Limits. American Mathematical Society Colloquium Publications, volume 60, 2012. [26] L. Lov ́asz and B. Szegedy. Limits of dense graph sequences. Journal of Combinatorial Theory, Series B, 96(6):933–957, 2006. DOI: 10.1016/j.jctb.2006.05.002. [27]C. Freer. Graphon theory in Lean 4. Computer software, 2026.https://github.com/cameronfreer/ graphon. [28]E. Davey, E. Hurley, R. de Joannis de Verclos, R. J. Kang, and J. Volec. Local flag algebras. arXiv:2607.12461, 2026. [29] E. Davey, E. Hurley, R. de Joannis de Verclos, R. J. Kang, and J. Volec. Strong edge-colouring via local flag algebras. arXiv:2607.17421, 2026. 57 [30]C. Spiegel. Computational flag algebras in Lean. Talk at the workshop Flags in the Mountains, CSU Mountain Campus, June 2026. Slides athttps://christophspiegel.berlin/assets/slides/ FlagsMountains_2026.pdf. A Compilation Times Table 3 reports end-to-end compilation time and peak memory for all seven compiler examples of Section 5.4, compiled with Lean 4 (v4.27.0) on an Intel Core i7-14700K (20 cores) with 64 GB of RAM under Windows 11. Each measurement covers the complete source file: flag enumeration, pair-density and multiplication lemma generation, PSD certificate checking, the objective expansion, and the main theorem. The generated files differ only in how their bridging lemmas are discharged. Underdecide +kernel(theflagGen.kernelDecide option), the file introduces no compiled-evaluation axiom; undernativedecide, it is faster but additionally depends on theLean.ofReduceBoolandLean.trustCompileraxioms. We report both modes for the five examples where kernel evaluation is tractable; for the two largest, theK 5 - andC 5 -free edge-density examples, only nativedecide was measured. Each figure is the mean over five runs of a single-file compilation against the prebuilt library, with the sample standard deviation; memory is the peak resident set, taken as the maximum over the five runs. Wall-clock times are highly repeatable (standard deviation below 0.5% of the mean in every configuration except the Erd ̋os pentagon under kernel evaluation, at 3.9%). Table 3: End-to-end Lean compilation time (mean of five runs,±sample standard deviation) and peak resident memory (maximum over five runs) for all seven examples, underdecide +kernelandnativedecide. “Lemmas” is the total count of generatedflagDensity 2 lemmas. A dash marks a configuration not measured under kernel evaluation. decide +kernel nativedecide CaseForbid N LemmasTime (s) RAM (GB)Time (s) RAM (GB) Mantel (edge density)K 3 31514.1± 0.32.411.5± 0.12.0 P 3 densityK 3 31513.3± 0.12.411.1± 0.02.0 C 4 densityK 3 421074.4± 0.18.219.8± 0.22.3 Edge densityK 4 4390 133.3± 0.311.227.9± 0.12.5 Erd ̋os pentagon (C 5 density) K 3 52832 2786± 10842.3 123.4± 0.54.2 Edge densityK 5 510332— 342.6± 0.68.1 Edge densityC 5 58172— 539.6± 0.58.6 58

Instant research discovery