Combinatorics

Motivation

Chemical reaction networks can contain reactions whose rates differ by powers of a large scaling parameter. A species may then change on one time scale while other combinations of species remain nearly fixed until a later one. This matters when replacing a detailed network by a smaller model: the quantities retained at the first scale need not be the quantities that evolve at the next. Kang and Kurtz formulate this separation using the reaction exponents and the changes made by each reaction, before analyzing the stochastic process limits in their paper. This mission concerns the algebraic separation of the first two natural time scales in Lemma 4.4, rather than a convergence theorem for the stochastic processes.

Setting

A reaction network has a finite set of species and a finite set of indexed reactions. For reaction $k$, the nonnegative integer $\nu_{ik}$ is the number of molecules of species $i$ consumed, and $\nu'_{ik}$ is the number produced. Its net change is $\zeta_{ik}=\nu'_{ik}-\nu_{ik}$. The two reaction vectors may coincide; allowing such a reaction does not make it change any species. The paper introduces a nonnegative abundance exponent $\alpha_i$ for each species and a real rate exponent $\beta_k$ for each reaction. The exponent relevant to a reaction under that abundance scaling is $\rho_k=\beta_k+\sum_i\nu_{ik}\alpha_i$ §2 and §3.2.

A nonnegative vector $\theta$ assigns weights to the species. The weighted quantity changes by $\theta\cdot\zeta_k$ when reaction $k$ occurs. Define $\Gamma^+_\theta$ and $\Gamma^-_\theta$ as the reactions for which this dot product is respectively positive and negative. Let $\alpha_\theta$ be the greatest $\alpha_i$ among indices with $\theta_i>0$. The natural time scale of this combination is

An empty maximum is $-\infty$, so a combination unaffected by every reaction has $\gamma_\theta=+\infty$. In particular $\gamma_0=+\infty$; the unused value of $\alpha_0$ has no effect. A coordinate vector gives a single species' scale $\gamma_i$. The first time scale is $r_1=\min_i\gamma_i$ (3.5), Definition 3.1, and (4.1).

At scale $r_1$, define $\Gamma_i^{r_1}=\{k:r_1+\rho_k=\alpha_i\}$. It contains every reaction meeting that exponent equation, including one that leaves species $i$ unchanged. Let $\mathbb S_1$ consist of the coordinate vectors $e_i$ for which $\Gamma_i^{r_1}$ is nonempty, and let $\Pi_1$ be the coordinate projection onto their span. The nonnegative combinations whose projection is unchanged by each such reaction form

The second time scale is $r_2=\inf_{\theta\in\mathbb K_2}\gamma_\theta$. This is the paper's minimum over $\mathbb K_2$: despite the infinite set of eligible vectors, every finite value of $\gamma_\theta$ is a difference of one of finitely many $\alpha_i$ and one of finitely many $\rho_k$ §4, p. 21.

Formalization targets

The first milestone compares each weighted combination with the species in its positive support and identifies $r_1$ among all nonnegative combinations:

The second milestone is the first sentence of Lemma 4.4. For $\theta\in\mathbb K_2$ and $l\in\Gamma_i^{r_1}$, a nonzero $\theta\cdot\zeta_l$ implies $\alpha_\theta>\alpha_i$. The goal is the lemma's strict separation:

These statements and their source order are on p. 21 of the preprint. The goal allows $r_2=+\infty$, which represents the absence of a later changing combination in $\mathbb K_2$.

Significance

The strict inequality says that the quantities eligible for the second scale cannot move at the first scale. It makes the two-scale terminology precise for this exponent model and separates an algebraic fact about reaction vectors from the later analysis of stochastic limits. A reduced process on the second scale requires additional stability and convergence conditions; Lemma 4.4 alone supplies neither. The paper explicitly discusses that limitation immediately after its proof on p. 22.

This mission packages the reaction-exponent definitions and the scale-separation statements as Lean declarations. Their proof obligations remain open in the proposal. Reusable parts include the finite reaction indexing, real-valued net-change vectors, the explicit convention for empty maxima, and the extended-real scale definitions. A complete development may also establish supporting facts about the finite range of $\gamma_\theta$ and the coordinate projection; such facts are useful beyond this lemma. The paper's stochastic limit theorems are outside this mission's scope.

Difficulty

Checking separately that every $\theta\in\mathbb K_2$ has $\gamma_\theta>r_1$ does not establish $r_2>r_1$: an infimum of strictly larger values can still equal $r_1$. The statement needs the finite-range property of the scale function, together with the interaction between the fast-reaction equation defining $\Gamma_i^{r_1}$ and the projected orthogonality condition defining $\mathbb K_2$. Empty reaction sets and zero weighted combinations also require explicit extended-real values. Replacing their scales with a default real number would change the claim Lemma 4.4, pp. 21–22.

Formalization scope

Species and reactions are Fin s and Fin r; their indices begin at zero, while the paper numbers them from one. The stoichiometric arrays have natural-number entries, $\zeta$ and $\rho$ are real-valued, and theorems carry $\alpha_i\geq0$. The sets of changing reactions and the positive support of $\theta$ are finite sets. Empty maxima use a bottom-extended real, while $\gamma_i$, $\gamma_\theta$, $r_1$, and $r_2$ live in extended reals. Finite scale differences are calculated in the reals before conversion. The formulas define $\rho$ from $\nu,\alpha,\beta$ and construct $\mathbb K_2$ from $r_1$; neither is a free input. No extra positivity condition is imposed on $\beta$.

The coordinate projection $\Pi_1$ retains the indices belonging to $\mathbb S_1$. The infimum for $r_2$ ranges over all of $\mathbb K_2$, including the zero vector and combinations unchanged by every reaction. The goal assumes that some reaction changes a species. Without this necessary nondegeneracy condition, $r_1=r_2=+\infty$ and the strict conclusion is false. It adds no condition on the initial stochastic state: the assumption at the start of §4 belongs to its process-limit statements. The paper develops at-most-binary mass-action rates in §2, but Lemma 4.4 uses only the indexed reaction vectors and their exponents; the Lean declarations expose exactly those algebraic data.

Selected references

• H.-W. Kang and T. G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010; published in Annals of Applied Probability 23(2), 2013. Preprint, DOI.

Why reaction-network balance matters

A stochastic reaction network tracks the counts of chemical species as reactions occur. Different species and reaction rates may grow at different powers of a large system-size parameter. Kang and Kurtz's model-reduction paper uses these powers to identify candidate time scales and combinations of species that can remain bounded. Before a reduced model can be justified, the dominant reactions that increase a combination must be compared with those that decrease it. Condition 3.2 makes that comparison.

Checking the condition for every nonnegative linear combination is a large task even for a finite network: the weights range over a continuum, and changing a weight can change which reactions increase or decrease the combination. The paper's Lemma 3.4 relates this task to the directed graph of species. It says that combinations supported on different strongly connected components can be checked component by component. This mission formalizes that result and the claims in its proof that carry the reduction.

The network and its graph

There are finitely many species $S_i$ and finitely many indexed reactions $k$. Reaction $k$ consumes $\nu_{ik}$ molecules of species $i$ and produces $\nu'_{ik}$ molecules of that species. The stoichiometric change is $\zeta_{ik}=\nu'_{ik}-\nu_{ik}$. Species $i$ has a nonnegative scaling exponent $\alpha_i$, and reaction $k$ has a real exponent $\beta_k$. The effective reaction exponent is $\rho_k=\beta_k+\sum_i\nu_{ik}\alpha_i$.

For a vector of nonnegative weights $\theta$, the scalar $\theta\cdot\zeta_k$ is the change in its linear combination when reaction $k$ occurs. Write $\Gamma^+_\theta$ for reactions with positive change and $\Gamma^-_\theta$ for reactions with negative change. The balance equation equates the largest $\rho_k$ on these two sets. If that equation fails, the time-scale inequality permits a chosen exponent $\gamma$ only when it is no larger than $\gamma_\theta$, the largest $\alpha_i$ on the support of $\theta$ minus the largest $\rho_k$ on $\Gamma^+_\theta\cup\Gamma^-_\theta$. Condition 3.2 is the disjunction of these two alternatives.

The species graph has an edge $S_i\to S_j$ when one reaction consumes $S_i$ and produces $S_j$. Its strongly connected components are the maximal sets of species that can reach one another by directed paths. A single species is a component when it shares no larger mutual-reachability class. A nonnegative vector supported in one such component is a component-level test vector.

Formalization targets

The goal is Lemma 3.4, p. 15. Suppose $\theta=\sum_{j=1}^m\theta^j$, each $\theta^j$ is nonnegative and supported within one maximal strongly connected component, and distinct pieces belong to distinct components. For fixed $\gamma$, the lemma asserts all three implications:

The companion consequence on the same page quantifies over all nonnegative vectors: if any one of these properties holds for every vector supported in a strongly connected subgraph, then it holds for every vector. The milestones mirror the paper's proof: a chain of component pieces cannot revisit a piece; under Condition 3.2 the maximal positive exponent either satisfies the time-scale bound or is bounded by the maximal negative exponent; and the two uniform cases yield their respective alternatives.

What the result establishes

Lemma 3.4 replaces a global family of tests with tests inside individual strongly connected components. In the paper this narrows the balance checks needed before the authors study separated time scales and reduced stochastic models. The uniform balance and uniform time-scale clauses matter separately: the first preserves equality of dominant positive and negative exponents, while the second preserves the same admissible $\gamma$ across a sum of pieces. The general Condition 3.2 clause allows different pieces to satisfy different alternatives.

The mathematical result was proved in the 2010 arXiv preprint and published in 2013; it is not an open conjecture. This proposal supplies Lean statements and a reusable finite reaction-network vocabulary, with proofs left for solvers. The local sanity file checks the empty-maximum and zero-vector behavior without using sorry. The draft theorem files compile as statements, but their six proofs are not yet machine checked.

Where the reasoning is difficult

The obvious inequality for a sum says that a reaction increasing $\theta$ increases at least one piece. It does not say that the piece's dominant increasing reaction also increases the sum: contributions from other pieces can cancel it. Consequently, taking a maximum separately on each piece does not directly give the balance equation for the sum. The graph restriction is decisive because a sequence of compensating reactions would otherwise be able to cycle among pieces. The milestones isolate that no-repetition property and the two inequalities the paper obtains from it.

Formalization scope

Species, reactions, and pieces are represented by Fin s, Fin r, and Fin m; these are zero-based versions of the paper's one-based indices. The stoichiometric coefficients are natural numbers, the changes $\zeta_k$ and all scaling exponents are real, and $\alpha_i\ge0$. Following the standing restriction on p. 5, each reaction consumes at most two molecules. The paper's $\rho_k$ is computed from $\beta_k$, $\nu_k$, and $\alpha$, not supplied independently.

For a reaction set $A$, $\max_{k\in A}\rho_k$ uses WithBot ℝ, so the maximum of an empty set is $-\infty$, as the paper explicitly uses on p. 17. The support maximum in $\gamma_\theta$ is an ordinary real maximum when relevant. The value $\gamma_\theta$ is represented in EReal: when $\Gamma^+_\theta\cup\Gamma^-_\theta$ is empty, it is $+\infty$ and the time-scale inequality holds for every real $\gamma$. Subtraction is performed in the reals before conversion to EReal. Thus zero vectors do not acquire a spurious bound from a default-valued maximum or extended-real subtraction.

An edge uses positive consumption and positive production in the same indexed reaction, matching the wording on pp. 4 and 15. Mutual reachability defines a component. Each piece is required to lie in one component, and different pieces in different components. These conditions prevent splitting a single component into separately balanced pieces, which would make the goal false. An empty family of pieces is permitted; its sum is zero. The definition file is useful for the other balance results in the paper, while the graph and component lemmas can support later work on reaction-network decomposition.

Selected references

• Hye-Won Kang and Thomas G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010, especially §2 and §§3.2–3.4, pp. 4–17. Preprint.
• Hye-Won Kang and Thomas G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, Annals of Applied Probability 23(2), 2013. DOI. The numbered statements in this mission follow the pinned 2010 preprint.

Motivation

A text index answers questions about occurrences of a pattern without scanning the whole text. One reason to compress such an index is that many stored texts are repetitive: multiple versions of a document or genome often share long passages. The Burrows–Wheeler transform (BWT) rearranges a text's symbols in a way that groups related contexts. A small number of equal-symbol runs in the BWT is therefore a useful measure of repetition. Gagie, Navarro, and Prezza use the number of runs to state space bounds for text searching and suffix-tree operations in Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space.

This mission isolates one exact counting result underneath those data-structure bounds. A length-$s$ substring is called an $s$-mer. The number of different $s$-mers measures how many local patterns the text contains; repeated occurrences of the same string count once. Lemma 9 of the 2019 preprint bounds this number directly in terms of BWT runs. The result makes a relation between two notions of text repetition precise: clustering in the BWT and diversity of fixed-length substrings.

Setting

Let $T[1..n]$ be a text over the ordered alphabet $[1..\sigma]$. Its final symbol is a unique terminator \=1$, smaller than every other symbol in the text. For each$i\in[1..n]$, the **suffix**$T[i..n]$starts at$i$and ends at the terminator. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$that lists these suffixes in increasing lexicographic order. Thus$SA[p]$is the starting position of the$p$th suffix. This is the setup of §2 of the source preprint, pp. 7–9.

The BWT symbol at position $p$ is the character just before the suffix at $SA[p]$. When that suffix is the whole text and has no preceding character, its predecessor is read cyclically as T[n]=\$$. The BWT partitions into maximal runs of equal symbols; r$denotes their number. The first and last BWT positions in each run correspond to **sampled text positions**. A text substring$T[i..j]$ is primary when its interval contains a sampled text position, as in Definition 5, p. 16.

For $1\le s\le n$, let $\mathcal S_s(T)$ be the set of length-$s$ strings occurring in $T$:

The braces matter: two windows with identical contents give one element. The final allowed window includes the terminator. The text is not padded in this definition.

Formalization targets

Primary occurrences

Lemma 8, p. 17 states that every nonempty substring of $T$ has an occurrence with the same contents that is primary. With $\operatorname{Sampled}(T)$ denoting sampled text positions, the assertion is

The mission's milestones also capture the suffix-array interval of a pattern, the sampled occurrence of each individual character, and the bound $|\operatorname{Sampled}(T)|\le 2r$ stated in the proof of Lemma 9. These give precise intermediate claims in the paper's route to the count.

Distinct $s$-mers

The main goal is Lemma 9, p. 17:

Here $r$ is calculated from the BWT of the text's suffix array. Both inequalities on $s$ are part of the source statement. The bound concerns distinct strings of a fixed length, not the number $n-s+1$ of substring windows.

Significance

The theorem gives an explicit upper bound on the number of different length-$s$ strings that can appear when the BWT has few runs. In §4.2 the authors use it to bound the text area holding all distinct length-$s$ substrings; that area supports the alphabet-mapping component of their compressed index. This exact combinatorial assertion remains meaningful independently of a machine model or a choice of data structure. Its role in the broader construction is described around Lemmas 8 and 9, pp. 16–17.

The result is proved in the paper. The work here is to give its objects and claims machine-checkable statements and then close their proofs in Lean. The mission has not already supplied a machine-checked proof of these claims. A completed development would also provide reusable definitions of suffix arrays, BWT run boundaries, and finite sets of distinct substrings for later formalizations of compressed text indexes.

Difficulty

The count is immediate only after every substring can be represented by an occurrence containing a sampled position. A direct count of all starting positions cannot yield the claimed bound: $n$ may be large even when $r$ is small. The difficult step is therefore the primary-occurrence claim of Lemma 8. Its statement has to preserve both parts of “occurrence”: the replacement interval must have the same length and symbols, and it must stay inside the text. The suffix-array range used there depends on lexicographic order, while sampled positions are defined through changes between adjacent BWT symbols. Connecting those two views of the text is the central obstacle.

Formalization scope

The Lean representation uses $\mathbb N$ for symbols and 1-based positions. The functions $T$ and $SA$ are read only on $[1..n]$. An IsText hypothesis enforces $n\ge1$, membership in $[1..\sigma]$, and the unique final terminator \=1$. An `IsSuffixArray` hypothesis says that$SA$maps$[1..n]$injectively into itself and orders its suffixes strictly; it does not presuppose any claim about BWT samples. Because that finite domain has$n$elements, these conditions describe a permutation. The BWT is computed from$T$and$SA$, with the predecessor of position 1 read as position$n$. Runs are counted by their starting cells; samples are the corresponding text positions from both ends of every run. The model follows the first sentence of Definition 1, including the last character of the final run. The source's following explanatory clause omits that endpoint.

The set of $s$-mers is a finite set of lists formed from every valid window. It is not restricted to primary windows, which would make the goal a different and easier statement. A primary substring carries valid endpoints and a sampled position inside them. The formal statements do not assume that the desired primary occurrence exists; that is precisely the content of Lemma 8. The paper's $O(\cdot)$ space and time results are outside this mission: the goal is their explicit substring-counting content.

A complete proof needs elementary facts about list prefixes and lexicographic order, finite interval images, the BWT's run partition, and cardinalities of substring windows near samples. The definitions and interval lemmas can be reused by other missions on suffix arrays and compressed strings. Contributions proving any of the listed milestones or strengthening the surrounding reusable string infrastructure are within scope.

Selected references

• Travis Gagie, Gonzalo Navarro, and Nicola Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv:1809.02792v2, 2019. Preprint.
• Travis Gagie, Gonzalo Navarro, and Nicola Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, Journal of the ACM 67(1), 2020. DOI:10.1145/3375890. The mission follows the preprint's numbering and wording.

Motivation

The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms: components express what remains connected after deleting vertices, while a small fixed number of parts gives a compact way to state constraints on a partition. Lemma 2.9 identifies exactly when the two forms agree for the half-balance threshold. The same result appears again in the paper as Lemma 6.2, where the authors use it in a later section.

The result does not require a tree decomposition or a treewidth hypothesis. It holds for every finite graph. That generality makes it a useful standalone target: the definitions of deletion, connected components, and the weighted three-partition can be reused wherever graph separators are studied. The mission follows the published SIAM article, with printed page 328 for the main lemma and pages 363–364 for its restatement and the supporting combinatorial observation.

Setting

Let $G$ be a finite simple graph with vertex set $V(G)$. Let $S$ and $X$ be subsets of its vertices. The deleted graph $G\setminus X$ retains precisely the vertices outside $X$ and the edges joining them. Two remaining vertices are in the same connected component when a walk joins them without passing through any vertex of $X$. Write $C_X(u)$ for the vertex set of the component containing $u\notin X$. This interpretation follows the paper's notation on page 320.

A balanced $S$-separator is a set $X$ for which each component of $G\setminus X$ contains at most half the vertices of $S$:

The paper introduces this phrase on page 321. Here balance is a property of $X$ relative to $S$; it imposes no bound on the size of $X$. The denominator counts all vertices of $S$, including any that lie in $X$.

A three-part partition of $V(G)\setminus X$ is a triple $(M_1,M_2,M_3)$ of pairwise disjoint sets whose union is $V(G)\setminus X$. A part may be empty. Two parts have no edge between them if no edge of $G$ joins a vertex of one to a vertex of the other. Since the graph is undirected, checking the three unordered pairs of distinct parts covers the requirement for every $i\ne j$.

Formalization targets

Lemma 2.9: balanced separators and three parts

The goal is the equivalence stated on page 328, also restated as Lemma 6.2 on page 363:

The equivalence is the target, including both directions. It applies even when $S$ or $V(G)\setminus X$ is empty. It does not include a bound on $|X|$.

Lemma 6.3: three bounded sums

The main supporting result on page 363 says that nonnegative integers $a_1,\ldots,a_p$ with total $q$ and $a_i\le q/2$ can be divided into three classes, each with sum at most $q/2$. The milestone list also records the paper's merge inequality and its assertion that a component cannot cross between parts having no edge between them. These are the specific claims used in the published discussion of Lemma 2.9.

Significance

Lemma 2.9 lets a componentwise balance condition be represented by three sets whose coverage, disjointness, edge separation, and cardinalities can be inspected directly. It gives an exact equivalence, so the three-part formulation loses no balanced separators and introduces none that fail the original definition. That is the mathematical content needed when a later argument represents a separator by a bounded number of regions rather than by a list of all its components. The result is already proved in the 2016 paper; the open work in this mission is a machine-checked formalization of that known result and its cited supporting claims.

Formalizing the equivalence also establishes reusable interfaces for vertex deletion and component membership in a finite simple graph. A future development can state a separator condition using IsBalancedSSep, or use the three-part conclusion without redefining what a component of $G\setminus X$ means. The independent integer-partition lemma has uses whenever indivisible nonnegative weights, each no larger than half the total, must be grouped into three bounded classes. Nothing in that statement depends on graphs.

Difficulty

There may be arbitrarily many components of $G\setminus X$, although the conclusion permits only three parts. Simply assigning all components to one part can violate the half bound, while splitting a component between different parts may create forbidden edges. A component's weight is the number of its vertices in $S$, and those weights can be uneven or zero. The theorem has to accommodate all such patterns without changing the threshold $|S|/2$. In the converse direction, the absence of edges between the three parts must control entire walks, not only their first edge; ordinary connectivity in $G$ would allow a walk through $X$ and would describe the wrong components.

Formalization scope

The Lean development uses SimpleGraph V with V : Type, [Fintype V], and [DecidableEq V]. Vertex sets are Finset V. The shared walk-based AvoidReach G X u v requires every vertex on a walk to lie outside $X$, including both endpoints; avoidComp G X u collects the vertices reachable in this way. It is used only for $u\notin X$ when quantifying over components. This shared definition matches the paper's $G\setminus X$. The graph itself need not have decidable adjacency, since the statements concern propositions rather than computations.

Half bounds are written as $2c\le |S|$ or $2c\le q$ in natural-number arithmetic. This is equivalent to the paper's rational half bound and avoids any interpretation of natural-number division. The three parts may be empty, so $X=V(G)$ is a genuine boundary case. The set $S$ may meet $X$; the right-hand denominator remains $|S|$. The graph may have no vertices. There is no treewidth parameter or size condition on $X$: adding one would change Lemma 2.9 and can make its reverse implication false. Nor may components be computed using connectivity in the original graph, where paths through deleted vertices could merge them.

The required infrastructure is finite graph walks, finite sets, cardinalities, sums over finite index types, and the three original claims in the milestone list. The graph-component definitions and the integer grouping theorem are reusable beyond this mission. Contributions that prove any milestone or the full equivalence under exactly these conventions are in scope.

Selected references

• H. L. Bodlaender, P. G. Drange, M. S. Dregi, F. V. Fomin, D. Lokshtanov and M. Pilipczuk, A c^k n 5-approximation algorithm for treewidth, SIAM Journal on Computing 45(2):317–378, 2016. DOI: 10.1137/130947374.

Motivation

Treewidth measures how closely a graph resembles a tree. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) study an algorithm for producing tree decompositions. Its headline result is algorithmic; this mission formalizes one combinatorial lemma used in its analysis.

In §4.3.2, p. 349, the authors isolate a purely combinatorial fact, Lemma 4.3, which bounds the number of nodes of a rooted tree in terms of a measure placed on its nodes. They use it for the partial tree decomposition built by FindPartialTD, with a measure of the form $\mu(i) = w_i/\log n$. This mission formalizes Lemma 4.3 and the steps of its proof. The lemma is self-contained and does not mention graphs or treewidth.

Setting

A rooted tree $T$ consists of a finite vertex set $V(T)$, a root $r \in V(T)$, and a parent map $p$ defined on $V(T) \setminus \{r\}$ such that every vertex reaches $r$ by iterating $p$. If $p(c) = v$, then $c$ is a child of $v$ and $v$ is the parent of $c$. A vertex without children is a leaf. The descendants of $v$ are the vertices $u$ with $p^i(u) = v$ for some $i \ge 0$ (including $v$ itself), and the subtree $T_v$ rooted at $v$ is the tree they span; $|V(T_v)|$ is its number of vertices, and $T_r = T$.

A measure is any function $\mu : V(T) \to \mathbb R$. Lemma 4.3 considers measures with three properties, for a constant $C$:

1. $\mu(v) \ge 1$ for every $v \in V(T)$;
2. for every vertex $v$ with children $v_1,\dots,v_p$ (where $p \ge 0$), $\sum_{i=1}^{p} \mu(v_i) \le \mu(v)$;
3. $0 < C < 1$, and $\mu(v') \le C\,\mu(v)$ whenever $v$ is the parent of $v'$.

Throughout, $K = 1 + \frac{1}{1-C}$.

Formalization targets

Goal: Lemma 4.3 (p. 349)

Under properties (i)–(iii),

Milestones (the proof on pp. 349–350)

Each step is stated for an arbitrary vertex $v$ of $T$, with the subtree $T_v$ in the role of the paper's tree.

• Base case (p. 349). If $v$ is a leaf, then $|V(T_v)| = 1 \le K\mu(v) - 1$.
• Summed bound (p. 350). If $v$ has children $v_1,\dots,v_p$ and $|V(T_{v_i})| \le K\mu(v_i) - 1$ for each $i$, then

• Case $p \ge 2$ (p. 350). With the same hypothesis on the children and at least two children, $|V(T_v)| \le K\mu(v) - 1$.
• Case $p = 1$ (p. 350). With the same hypothesis and exactly one child, $|V(T_v)| \le K\mu(v) - 1$.
• Subtree form (p. 350). Under (i)–(iii), $|V(T_v)| \le K\mu(v) - 1$ for every vertex $v$; this is the statement the induction proves, and at $v = r$ it is the goal.

Significance

The result. Lemma 4.3 converts two local conditions, superadditivity of the measure over the children of each node and geometric decay by a factor $C$ along each parent–child edge, into a global linear bound on the size of the tree. Superadditivity alone does not bound the size: a long path with constant measure satisfies (i) and (ii). Decay alone does not either: a star with many leaves satisfies (iii). The counting principle can also be used when a recursive construction splits a resource among child nodes while reducing that resource along every edge.

Formalizing it. The lemma is proved in the paper. The mission produces formal statements of the lemma and the main bounds in its proof, over a published, reusable encoding of finite rooted trees by parent maps. A complete development would also establish structural facts about descendants and children that can be reused for other results about finite rooted trees.

Difficulty

The summed bound for the children's subtrees contains the term $1-p$. When $p=1$, superadditivity alone does not give the target's final $-1$: a path with constant measure is a counterexample if geometric decay is omitted. Formalization also has to account for the fact that the reusable tree representation is a parent map on a finite type, rather than an inductively constructed tree.

Formalization scope

The rooted tree is the published definition HarelTarjan.Compressed.RootedTree: a finite vertex type V with a root and a total parent map in which every vertex reaches the root, with the convention $p(r) = r$. $|V(T)|$ is Fintype.card V, and $|V(T_v)|$ is the published subtree size size T v (the number of descendants of $v$, including $v$). The local definition file adds IsChild T v c ($c \ne r$ and $p(c) = v$) and children T v; the condition $c \ne r$ removes the pseudo-edge $r \to r$, so the root is never its own child.

Conventions: $\mu$ is real valued, as on the page; property (ii) is a sum over a possibly empty set of children; the constant $C$ of property (iii) is a parameter with the two hypotheses $0 < C$ and $C < 1$, because the conclusion is stated with that same $C$. The fraction $\frac{1}{1-C}$ is real division, and the hypothesis $C < 1$ keeps it away from Lean's convention $1/0 = 0$. The bound keeps the page's "$-1$".

A trivializing formalization is ruled out explicitly: the parent–child relation is directed by the root, so property (iii) constrains each edge in one direction only. A symmetric reading ("$\mu(c) \le C\mu(v)$ for all adjacent $v, c$") would be unsatisfiable for $C < 1$ and make every statement vacuous; the hypotheses here are satisfied, for example, by the two-vertex tree with $\mu = (2, 1)$ and $C = 1/2$.

A complete development needs the decomposition of size T v as $1 + \sum_{c \in \mathrm{ch}(v)} \mathrm{size}\,T\,c$ and an induction principle for parent-map trees. Both are reusable for statements about rooted trees given by parent maps, and contributions of them as separate lemmas are welcome. The paper's subsequent application is outside this mission's scope.

Selected references

• H. L. Bodlaender, P. G. Drange, M. S. Dregi, F. V. Fomin, D. Lokshtanov, M. Pilipczuk, A $c^k n$ 5-approximation algorithm for treewidth, SIAM Journal on Computing 45(2):317–378, 2016. https://doi.org/10.1137/130947374 (Lemma 4.3 and its proof: pp. 349–350.)
• D. Harel, R. E. Tarjan, Fast algorithms for finding nearest common ancestors, SIAM Journal on Computing 13(2):338–355, 1984. https://doi.org/10.1137/0213024 (source of the rooted-tree encoding reused here.)
• N. Robertson, P. D. Seymour, Graph minors. II. Algorithmic aspects of tree-width, Journal of Algorithms 7(3):309–322, 1986. https://doi.org/10.1016/0196-6774(86)90023-4

Motivation

In the 1993 essay Dimensional Reduction in Quantum Gravity (arXiv:gr-qc/9310026), G. 't Hooft argued that, once gravitational collapse is taken into account, the number of quantum states available to a region of space grows with the area of its boundary rather than with its volume. The essay is the origin of what is now called the holographic principle (developed further by Susskind, arXiv:hep-th/9409089). Besides the physical counting argument, the essay contains a small, fully precise mathematical model: a cellular automaton on the cubic lattice $\mathbb Z^3$ whose data on a one-dimensional line determine the data everywhere. This mission formalizes the quantitative estimates and the automaton statements of the essay.

Setting

Entropy estimates (eqs. (4)–(11)). In natural units, a region bounded by a sphere of radius $R$ has volume $V=\tfrac43\pi R^3$ and area $A=4\pi R^2$. A thermal gas of $Z$ particle species at temperature $T$ has energy $E=C_1 Z V T^4$ and entropy $S=C_2 Z V T^3$ with positive constants $C_1,C_2$. It stays outside its own Schwarzschild radius if $2E<R$. A black hole of mass $M$ has entropy $4\pi M^2$ (eq. (1), additive constant dropped).

Plaquette automaton (eqs. (12)–(19)). Data $f:\mathbb Z^3\to\mathbb Z/p$ live on lattice sites. An elementary plaquette has lowest corner $x$ and is spanned by two of the unit vectors $e^1,e^2,e^3$; its corners in cyclic order are $x,\;x+u,\;x+u+v,\;x+v$. On every plaquette a relation $g(f_1,f_2,f_3,f_4)=0$ is imposed such that any three entries determine the fourth uniquely. The relations may differ from plaquette to plaquette. On the unit cube with corners $A=0$, $B=e^1$, $D=e^2$, $E=e^3$, $C=e^1+e^2$, $F=e^1+e^3$, $H=e^2+e^3$, $G=e^1+e^2+e^3$, the six face relations are (12a–f). The staircase (eq. (14)) is the sequence

A family of face relations is consistent (eq. (16)) if every choice of $f(A),f(B),f(D),f(E)$ extends to data on the cube satisfying all six relations; equivalently, the three values of $f(G)$ produced by (12b), (12d), (12f) agree. Linear relations (eq. (17)) have the form $\sum_j a_j f_j+b \equiv 0 \pmod p$, with every $a_j$ invertible mod $p$.

Formalization targets

Goal: the staircase determines everything

For any family of plaquette relations with the three-determine-the-fourth property, two solutions on $\mathbb Z^3$ that agree on the staircase agree everywhere:

Milestones

1. Eqs. (4)–(8): $T<C_3Z^{-1/4}V^{-1/6}$ and $S<C_4Z^{1/4}V^{1/2}=C_5Z^{1/4}A^{3/4}$ for the thermal gas.
2. Eqs. (9)–(11): black holes that fit inside the sphere have total entropy $<A/4$, and $A/4$ is the supremum.
3. Discussion of Fig. 1: on one cube, the data at $D,H,E,F$ determine all eight corners.
4. Eqs. (17)–(19): consistent linear relations with invertible coefficients exist for every modulus $p\ge 2$.
5. Eqs. (14), (17): for the linear relation $f_1-f_2+f_3-f_4\equiv0$, any data on the staircase extend uniquely to a global solution. The staircase data are then exactly the free degrees of freedom.

Significance

The goal is the essay's concrete mathematical example of dimensional reduction: in a $2+1$-dimensional lattice model, a one-dimensional set of data carries all the information. Milestone 5 shows that the reduction is sharp in the linear case: no data beyond the staircase are needed, and none of the staircase data are constrained. Milestones 1–2 are the scaling estimates behind the area law $S_{\max}=A/4$. The physical argument around them (black-hole thermodynamics, the Schwarzschild criterion) is taken as modelling input, not formalized. The results are stated in the essay but, as far as is known, have not been machine-checked.

Difficulty

The local step (one cube, Milestone 3) is elementary. The goal needs a global propagation argument. The staircase is a thin zig-zag line, and each application of a plaquette relation fixes only one new site. So the proof has to show that repeated local determination starting from the line eventually reaches every site of $\mathbb Z^3$, in both directions along the line and in both transverse directions. Layer-by-layer propagation in $t=x_1+x_2+x_3$ does not apply directly, because the staircase is not a full layer.

Formalization scope

Sites are ℤ × ℤ × ℤ. Data take values in ZMod p for an arbitrary natural number $p$; the uniqueness statements hold for every $p$. The three-determine-the-fourth property is stated with unique existence ($\exists!$) for each slot, which matches "uniquely determined" in the essay. Relations may depend on the plaquette, so no translation invariance is assumed. Consistency (16) is encoded as extendability of the four free values on the unit cube. In Milestones 1–2 the region is a round sphere of radius $R$, so $V$ and $A$ are expressions in $R$, and the constants are existentially quantified before all physical variables. Contributions welcome: proofs of each milestone, and further faithful statements from the triangular-lattice model (eqs. (20a–f)).

Selected references

• G. 't Hooft, Dimensional Reduction in Quantum Gravity, essay in honour of A. Salam, 1993. https://arxiv.org/abs/gr-qc/9310026
• L. Susskind, The World as a Hologram, J. Math. Phys. 36 (1995) 6377. https://arxiv.org/abs/hep-th/9409089

Motivation

An assignment problem pairs each of $n$ sources with exactly one of $n$ destinations while minimizing a specified cost. A permutation records those pairings. The number of permutations grows as $n!$, so a direct search quickly becomes impractical. In discrete optimal transport, the same data can be placed in a linear optimization problem over nonnegative matrices: a matrix entry records how much mass moves from one source to one destination. That formulation permits a source's mass to be split, which gives it many more feasible solutions than the assignment problem. The question for this mission is whether the added flexibility can improve the optimum when every source and destination carries the same mass. The setting and answer are given in Peyré and Cuturi, Computational Optimal Transport, §2.2–2.3.

This capstone is the first in a series based on the textbook. It links a finite combinatorial optimization problem to the matrix model used throughout later chapters. The general transport model is needed again when marginals are unequal, when cost matrices come from distances, and when entropy is added to the objective. The uniform matching case isolates a useful boundary: relaxing an assignment to allow fractional flows expands the feasible set, yet it does not change the best objective value.

Setting

Fix an integer $n>0$ and a real $n\times n$ cost matrix $C$. The entry $C_{ij}$ is the cost of sending a unit of mass from source $i$ to destination $j$. No sign or metric assumption is imposed on $C$. A permutation $\sigma$ assigns source $i$ to destination $\sigma(i)$, with every destination used once. The assignment objective of equation (2.2) is