Motivation

In the mid-1960s the success of $SU(6)$ as an approximate symmetry of hadrons raised the question whether the Poincaré group and an internal symmetry group could be combined into a larger relativistic symmetry group that is not simply their direct product. A series of no-go theorems for Lie groups (Coleman 1965, Weinberg 1965, Michel–Sakita 1965) relied on artificial assumptions and did not cover infinite-parameter groups. Coleman and Mandula (Phys. Rev. 159, 1251 (1967)) settled the question using information about the S matrix: any connected symmetry group of a non-trivial, Lorentz-invariant S matrix with a reasonable particle spectrum is locally the direct product of the Poincaré group and an internal symmetry group. The theorem is the standard reason why space-time and internal symmetries do not mix in relativistic quantum field theory, and its loopholes (graded Lie algebras, i.e. supersymmetry; conformal symmetry for massless theories) shaped later model building (Haag–Łopuszański–Sohnius 1975).

Setting

Momenta are four-vectors $p=(p^0,p^1,p^2,p^3)$ with Minkowski product $p\cdot q=p^0q^0-\vec p\cdot\vec q$. The one-particle spectrum is organised by mass hyperboloids $H_k=\{p : p\cdot p=m_k^2,\ p^0>0\}$, $m_k\ge 0$, indexed by a set of distinct masses. On $H_k$ there are $N_k<\infty$ one-particle states of each momentum, and a Lorentz transformation $\Lambda$ acts on them through unitary Wigner matrices $W_k(\Lambda,p)$. The two-particle block of the T matrix, $S=1-i(2\pi)^4\delta^4(P-P')T$ (Eq. (2) of the paper), is a family of matrices $T(p,q\to p',q')$ defined for $p+q=p'+q'$, covariant under Lorentz transformations.

A symmetry generator is a Hermitian operator on momentum-space wave functions that acts on two-particle states as $A\otimes 1+1\otimes A$ and commutes with $S$. A generator commuting with the translations is a multiplication operator $B$: on $H_k$ it multiplies the wave function at $p$ by a Hermitian matrix $B(p)$, and on two-particle states it acts by $B(p,q)=B(p)\otimes 1+1\otimes B(q)$ (Eq. (19)). An internal symmetry generator is one commuting with the whole Poincaré group.

The paper's hypotheses are: (1) Lorentz invariance; (2) particle finiteness — finitely many particle types below any mass; (3) weak elastic analyticity of the elastic amplitudes near the physical region, except at normal thresholds $s=(m_a+m_b)^2$; (4) occurrence of scattering — any two momentum eigenstates scatter, except at isolated energies $s$; (5) a technical assumption that the generators have distribution kernels.

Formalization targets

Goal: the infinitesimal Coleman–Mandula theorem (Lemma 9)

Assume every particle is massive. Let $\mathfrak A$ be a real-linear set of Hermitian generators containing the Poincaré generators $P_a$ (multiplication by $a\cdot p$) and $M_X$ ($X\in\mathfrak{so}(3,1)$), closed under $A\mapsto i[P_a,A]$, whose members act on the hyperboloids as differential operators of one finite order $N$ (the same on every hyperboloid), and whose translation-commuting members commute with the S matrix. Then every $A\in\mathfrak A$ has the form

$$A \;=\; M_X \;+\; a\cdot P \;+\; b,$$

with $X\in\mathfrak{so}(3,1)$, $a$ a constant four-vector, and $b$ an infinitesimal internal symmetry transformation. The paper states that this Lemma 9 "is just the infinitesimal form of our theorem".

Correction note (revised draft). An earlier version of this draft stated the goal without the positive-mass hypothesis and with an order bound that could depend on the hyperboloid. That version is false, and the drafter formally disproved it in Lean: take one massless scalar particle with trivial Wigner cocycle and constant non-zero $T$, and let $\mathfrak A$ consist of the operators that agree on test functions with a real combination of the translation generators, the Lorentz generators and the dilation generator $i(v\cdot\nabla_v+1)$. All hypotheses hold, but the dilation is not of the form $M_X+a\cdot P+b$. This is the known conformal loophole of the theorem for massless theories; the paper's hypothesis (2) and its proof implicitly use massive particles. The goal is now ColemanMandula.coleman_mandula_corrected, which adds hmassive : ∀ k, 0 < D.mass k and a single order bound n for each generator on all hyperboloids (the paper's single finite order $N$ in the proof of Lemma 9). Update: in the drafter's local project (Lean 4.28.0, Mathlib 8f9d9cf), Lemmas 3–8 and the corrected goal have been proved without sorry, using only the standard axioms; this is the drafter's own work, not an independent check. The drafter has not shown that the uniform order bound is needed.

Milestones (Lemmas 3–8 of the paper)

• Lemma 3. Forward elastic amplitudes stay non-zero under small rotations in the centre-of-mass frame.
• Lemma 4. $K(p,q)$ depends only on $p+q$.
• Lemma 5. If $B^*(p,q)=0$ for one non-null pair on a hyperboloid, the traceless part $B^*$ vanishes on the whole hyperboloid.
• Lemma 6. The traceless part $B^*$ is an infinitesimal internal symmetry transformation.
• Lemma 7. $\operatorname{Tr}B(p)$ is a linear (affine) function of $p$.
• Lemma 8. $B(p)=a_\mu p^\mu+b$ with $b$ internal.

Significance

The result rules out any non-trivial relativistic mixing of space-time and internal symmetries for theories with a non-trivial S matrix, covering infinite-parameter groups, and it yields as a corollary that all particles in a supermultiplet have the same mass (a generalisation of O'Raifeartaigh's theorem). The paper itself makes "no claim for corresponding standards of rigor"; a machine-checked version fixes a precise model in which the argument is correct, and exposes exactly which analytic facts (analyticity, continuity of the Wigner cocycle, the structure of compact Lie algebras, the absence of non-trivial finite-dimensional unitary representations of the Lorentz group) carry the proof. To the proposer's knowledge the theorem has not been formalized in Lean before.

Difficulty

The central step is Lemma 6: the traceless parts of the translation-commuting generators restricted to a hyperboloid form a Lie algebra that embeds (via Lemma 5) into $\mathfrak{su}(n)\oplus\mathfrak{su}(n)$, hence is compact reductive; the Lorentz group acts on it by automorphisms. One has to show this action is trivial — on the semisimple part because the Lorentz group has no non-trivial homomorphism into a compact group, and on the Abelian part by a separate $SO(2)$ argument. None of this infrastructure (compact Lie algebras, their automorphism groups, Lorentz-group representation theory) is currently available in Mathlib in usable form. Lemmas 3–5 in turn need analyticity and connectivity arguments on the manifold of momentum-conserving configurations.

Formalization scope

The formalization works in a momentum-space model (definitions ColemanMandula_Kinematics, ColemanMandula_Scattering):

• Four-vectors are Fin 4 → ℝ with signature $(+,-,-,-)$; Lorentz transformations are $4\times4$ real matrices with $\Lambda^T\eta\Lambda=\eta$, $\det\Lambda=1$, $\Lambda^0{}_0>0$. Massless hyperboloids are allowed (the apex is excluded).
• The spectrum is indexed by distinct masses (Shell), each with finitely many states per momentum; all particle types of one mass are grouped together. The Wigner cocycle is an arbitrary continuous cocycle, smooth in $p$.
• Only the $2\to2$ block of $T$ is modelled. "Commutes with $S$" is encoded as $B(p',q')T=TB(p,q)$ on momentum-conserving configurations.
• Assumption 3 is stated as real-analyticity of the elastic amplitude in the momentum variables on a neighbourhood of the physical region minus normal thresholds; assumption 4 is stated in the form used in Lemma 3, as non-vanishing of the forward elastic amplitude $\langle v,T(p,q\to p,q)v\rangle$ (equivalent to Eq. (3) by unitarity/the optical theorem), except on a set of isolated exceptional energies.
• Algebraic recasting (footnote 12 of the paper). Assumption 5 and the conclusions of Lemmas 1–2 are built into the model of the generators: members of $\mathfrak A$ act on each hyperboloid as finite-order differential operators in the spatial momentum with smooth matrix coefficients (in particular they do not connect different hyperboloids). Lemmas 1 and 2 are therefore not milestones of this mission; smooth rather than distributional coefficients are assumed, which also merges the paper's classes $\mathfrak B$ and $\mathfrak B_S$. The goal is the infinitesimal form of the theorem (Lemma 9); the group-level statement about local isomorphism of an infinite-dimensional group is not formalized.
• "Internal symmetry" is formalized covariantly, as commutation with every Lorentz transformation, $b(\Lambda p)W(\Lambda,p)=W(\Lambda,p)b(p)$, which is the paper's definition and does not depend on a choice of spin bases.

The model is non-vacuous: a single massive scalar particle with a constant non-zero T matrix satisfies all hypotheses, with $\mathfrak A$ spanned by the Poincaré generators and the identity. Contributions are welcome on: continuity/analyticity arguments on two-body phase space (Lemmas 3–5), compact Lie algebra structure theory and triviality of finite-dimensional unitary representations of the Lorentz group (Lemma 6), and the functional equation for additive collision invariants (Lemma 7).

Selected references

• S. Coleman, J. Mandula, All Possible Symmetries of the S Matrix, Phys. Rev. 159, 1251 (1967). https://doi.org/10.1103/PhysRev.159.1251
• R. Haag, J. T. Łopuszański, M. Sohnius, All possible generators of supersymmetries of the S-matrix, Nucl. Phys. B 88, 257 (1975). https://doi.org/10.1016/0550-3213(75)90279-5
• S. Weinberg, The Quantum Theory of Fields, Vol. III, Cambridge University Press (2000), Sec. 24.B. https://doi.org/10.1017/CBO9781139644174

Bound $L_4$: $33,070,982 \le R$

This mission formalizes the lower bound $33,070,982 \le R$ on the number of reversible binary cellular automata on the $3 \times 3$ Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.

A convex polytope has both geometric coordinates and a finite pattern of faces. Moving its vertices can change distances and angles while preserving which vertices belong to which faces. Enumeration by combinatorial type asks for those incidence patterns, with geometrically different realizations of the same pattern counted together. Grünbaum’s enumeration theorem establishes that the complete collection can be determined algorithmically when the dimension and number of vertices are prescribed Convex Polytopes, §5.5, p.91.

A d-polytope here is a nonempty convex hull of finitely many points in real d-dimensional coordinate space, with affine span equal to the whole space. A face is obtained by maximizing a linear functional over the polytope; the collection of faces also includes the empty face and the polytope itself. Inclusion orders this collection. Two polytopes have the same combinatorial type when their full face collections admit an order isomorphism. This notion retains the incidence structure and forgets metric measurements.

To describe a type with finite data, label the k vertices by the integers from zero through k−1. Record the set of vertex labels belonging to each nonempty proper face. This family of subsets is the polytope’s scheme. A finite list of finite lists of natural numbers encodes such a family. The order of labels and repeated occurrences of a label do not change the represented subset. A scheme is realized only when its recorded subsets are exactly the vertex sets of the nonempty proper faces: it cannot add faces, omit faces, or introduce labels outside the prescribed range.

The target is a single total computable function

$$E : \mathbb N\times\mathbb N\longrightarrow \operatorname{List}(\operatorname{List}(\operatorname{List}(\mathbb N))).$$

For every dimension d and vertex count k, each scheme in E(d,k) must have a realizing d-polytope with exactly k vertices. Every d-polytope with k vertices must realize some scheme in that output. Finally, if polytopes realizing two output positions have isomorphic full face posets, those positions must be equal. These requirements say that the output contains precisely one representative of every combinatorial type. The existential choice of one function precedes both numerical inputs, so the algorithm must work uniformly for all dimensions and vertex counts.

The result supplies an effective finite classification at each prescribed size. It is stronger than the observation that only finitely many incidence families can be written down: those families need not all arise from real convex polytopes. It also addresses termination, since a total algorithm must return its entire finite answer for every input. The theorem is a known mathematical result in the cited textbook. The present formal target asks for a proof of its stated algorithmic conclusion; no machine-checked proof of that conclusion is asserted here.

The principal difficulty is the connection between finite incidence data and geometric realizability. Combinatorial consistency alone does not supply real coordinates for a convex polytope. The source distinguishes this realizability question from the enumeration conclusion and identifies decidability over the real numbers as relevant to it §5.5, p.91. The mission retains the complete enumeration conclusion, including realizability of each answer, coverage of every type, and absence of duplicate types.

The formal representation uses real coordinates without a rationality restriction and permits nonsimplicial polytopes. Vertices are labelled injectively and exhaustively. The number of vertices is expressed as the number of nonempty zero-dimensional exposed faces. Nonemptiness separates the empty face, whose book dimension is −1, from the natural-valued dimension used to count faces. For finite convex hulls the face collections are finite, so this cardinality has its usual meaning.

Natural-number dimensions include dimension zero. The unique point has one vertex and no nonempty proper faces, and therefore uses an empty scheme. This is an explicit extension of the source’s positive-dimensional scheme convention. Unrealizable dimension and vertex-count pairs require an empty output. Finite-polytope faces, their ordered collection, vertex counts, and finite scheme realizations are the concrete objects needed to state the goal; total computability applies to the complete finite output rather than to individual tests alone.

Reference: Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.5, Theorem 2 (5.5.2), printed p.91, PDF p.117; definitions in §§2.4 and 3.1. Source text.

Binary choices and polyhedral complexity

A vector whose coordinates are all zero or one records a collection of yes-or-no choices. Taking the convex hull of a collection of these vectors gives a 0/1-polytope, also called a binary polytope. Such objects connect discrete choices with geometry: points describe feasible combinations, while supporting inequalities describe restrictions that every feasible combination satisfies. Grünbaum's discussion in §4.9 emphasizes the role of facets of these polytopes in combinatorial optimization and cutting-plane descriptions.

The question here concerns how many facets can occur when the dimension grows. Restricting every generating point to binary coordinates gives a finite, highly structured collection of possible points. Nevertheless, this restriction still allows polytopes with very many distinct boundary faces. The theorem of Bárány and Pór establishes superexponential growth in the largest possible number of facets. The mission concerns the form of this growth asserted in Grünbaum's 2003 notes, printed page 69a, rather than a prescribed numerical constant.

Polytopes, dimension, and facets

Fix a natural number d. The ambient space is the real coordinate space R^d. A convex hull consists of all convex combinations of the generating points, meaning weighted averages with nonnegative weights whose sum is one. A polytope is the convex hull of a finite set of points. It is full-dimensional when its affine span is all of R^d; this rules out a polytope lying in a proper affine subspace.

For a binary polytope, every generating point belongs to {0,1}^d. A subset of this cube is automatically finite. Nonemptiness and full dimension are imposed separately in the target. Consequently, the dimension in the facet bound is the actual dimension of the polytope as well as the dimension of its coordinate space.

An exposed face is the set of all points of the polytope that maximize a given linear functional. A facet is a face of affine dimension d−1. Facets are counted as geometric sets. Two different inequalities that expose the same face do not contribute two facets. Write f_(d−1)(P) for this number.

The growth target

The target is the following existence statement:

$$\exists c>1\;\exists D\in\mathbb N,\ D\ge2,\quad \forall d\ge D\;\exists P\subseteq\mathbb R^d,\quad P\text{ is a full-dimensional binary polytope},\qquad f_{d-1}(P)>c^{d\ln d}.$$

The constant c and threshold D are chosen before the dimension d. The polytope P may depend on d. The assertion therefore supplies a witness in every sufficiently large dimension. It does not merely assert the existence of one complicated polytope or of witnesses along an unspecified subsequence.

The logarithm is natural. Replacing it by another fixed base greater than one changes the admissible constant c, while preserving the shape of the theorem. The statement leaves both c and D unspecified. The Bárány–Pór paper, Theorem 1.1, supplies the asymptotic context for the book's formulation.

What superexponential growth says

For any fixed c greater than one, the expression c^(d ln d) eventually exceeds A^d for every fixed A greater than one. Thus a single exponential base cannot bound the facet counts of all binary polytopes across dimensions. The binary-coordinate restriction alone does not yield that kind of uniform bound.

The underlying mathematical result is established in the literature. The formalization task is to prove its stated existence conclusion with the precise geometric definitions above. The conclusion concerns actual facets of actual polytopes, so a family of redundant inequalities or a list with repetitions would not satisfy the counting requirement.

Why the existence statement is demanding

A large supply of binary points does not by itself identify the supporting hyperplanes of their convex hull. Counting points and counting facets are different tasks. Moreover, the theorem requires the same growth constant across all sufficiently large dimensions. Verifying individual examples, even examples with many facets, leaves that uniform asymptotic requirement unresolved.

The book describes certain random polytopes as witnesses. Its stated conclusion gives no probability distribution or numerical probability bound. The target records the resulting extremal existence assertion; it imposes no extra probabilistic hypothesis on the witness.

Geometric conventions

The coordinate model is Fin d → ℝ. IsDPolytope requires a nonempty finite convex hull with full affine span. IsZeroOnePolytope specifies the hull of binary-coordinate points. faceCount P k counts nonempty exposed faces with affine dimension k. These concrete notions also apply to other questions about finite-dimensional polytopes.

Face counts use natural cardinality. On the domain of finite polytopes there are only finitely many faces, so this is the ordinary finite count. Requiring D at least two ensures that d−1 represents the facet dimension without a low-dimensional subtraction convention and that the logarithm's argument is positive. Full dimension excludes the whole polytope from the facet count, and nonemptiness excludes the empty face.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §4.9, printed p.69a; definitions in §§2.4 and 3.1. Book.
• Imre Bárány and Attila Pór, On 0-1 Polytopes with Many Facets, Advances in Mathematics 161 (2001), 209–228, Theorem 1.1. Paper.

Recognizing a convex set from its projections

A convex set can be studied through its images in spaces of smaller dimension. Each image records part of the geometry, while losing the information along the directions that are collapsed. A finite convex hull always has finite convex hulls as its affine images. The converse asks whether sufficiently rich projection data can force the original set to have a finite description by points. This mission concerns the recognition theorem attributed to Klee in Grünbaum's Convex Polytopes, §5.1, Theorem 8, printed page 74.

The question concerns all projections into a suitable dimension, rather than an individual view of a set. A single image may conceal directions in which the original set has additional structure. The theorem identifies a condition on the entire family of images that characterizes polytopes among bounded convex sets.

Sets, convex hulls, and affine projections

Fix an integer $d\geq3$. Real coordinate space $\mathbb R^d$ consists of vectors with $d$ real coordinates. A set $K\subseteq\mathbb R^d$ is convex if it contains the line segment joining any two of its points. It is bounded if its points remain within some finite distance of the origin. Neither condition requires $K$ to fill the ambient space.

The convex hull of a set $V$, written $\operatorname{conv}(V)$, is the smallest convex set containing $V$. A polytope is the convex hull of a finite set. The generating set need not be a minimal set of vertices. Grünbaum gives this characterization in §3.1, printed page 31. The empty generating set is permitted, as are generating sets contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map $f:\mathbb R^d\to\mathbb R^j$ has a $j$-dimensional target and reaches every point of that target. When $j<d$, such a map loses dimensions. This represents the singular affine images called projections in §5.1, printed page 71, with coordinates chosen on the target affine space. Translation of the target is allowed.

The recognition target

For every bounded convex set $K\subseteq\mathbb R^d$, the goal is the equivalence

$$K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\quad 2\leq j<d,\quad \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\quad f(K)\text{ is a polytope}.$$

The dimension $j$ may depend on $K$, but it is chosen before testing the affine maps. Every surjective affine map with that target dimension is tested. For each such map, the finite set generating the image can be different. No common set of projected vertices or uniform bound on the number of generators is required.

This is one recognition theorem, containing both implications. The selected source grouping does not introduce separate supporting theorem targets.

What the criterion establishes

The theorem characterizes a global finite convex-hull property through lower-dimensional images. In particular, the conclusion concerns the original set itself; it does not merely assert that its closure has a finite generating set. This distinction matters because boundedness and convexity alone do not assert closedness.

The result is a known mathematical theorem in the source. The formalization target is its complete equivalence with the stated domain and quantifier order. A proof of only the preservation of polytopes under affine maps would leave the recognition implication unresolved.

Why the converse requires more than one image

Every tested image can have its own finite generating set. Finiteness of each image does not directly supply a finite generating set that works in the original ambient space. The recognition implication must connect the universal family of images to the geometry of the whole set. Replacing that family by a convenient fixed projection would change the question.

Mathematical conventions

Real $d$-space is represented by functions from Fin d to the real numbers. Boundedness and convexity use the ordinary Mathlib predicates, and being a polytope is expressed directly by existence of a finite set with the specified convex hull. No full-dimensional polytope structure is imposed on $K$.

The hypothesis $d\geq3$ makes explicit the admissible ambient dimension needed for $2\leq j<d$. In dimension three, the only available target dimension is two. No assertion of the displayed existential criterion is made in dimensions zero, one, or two. Empty sets, singleton sets, and other lower-dimensional subsets remain within the domain in every admissible ambient dimension.

Affine maps are required to be surjective onto the selected coordinate space. Thus their rank is exactly the selected target dimension, rather than an accidentally smaller rank. Closedness, nonemptiness, rational coordinates, and a predetermined number of vertices are not additional hypotheses. The mathematical ingredients are real convex hulls, finite sets, bounded sets, and affine images.

Selected references

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003. Theorem 5.1.8, printed page 74 (source.pdf page 100); projection convention, printed page 71 (PDF97); polytope convention, printed page 31 (PDF51). The source pages are included in this package's evidence directory.

A polytope can be represented by cutting a higher-dimensional simplex with an affine flat. The geometry of the cut determines the resulting polytope. Perles's prescribed-point theorem adds a constraint to this representation: the cutting flat must pass through a point chosen in advance inside the simplex. Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition (2003), shows that this requirement can always be met when the simplex has enough facets. The source is §5.1, printed page 74, with the section convention introduced on printed page 71.

A polytope is the convex hull of finitely many points. In this mission it is nonempty and full-dimensional in its ambient real coordinate space. Thus a d-polytope P in R^d contains enough points to span that space affinely. A face is the set of points on which a supporting linear functional attains its maximum; a facet is a face of dimension d−1. Different supporting functionals can describe the same face, so the facet allowance counts geometric faces rather than inequalities used to describe them.

A k-simplex is the convex hull of k+1 affinely independent points. Write its vertices as v₀,…,vₖ in R^k and its convex hull as T. Affine independence means there is no nontrivial affine relation among these vertices. The simplex therefore has dimension k, and its interior is taken in the whole space R^k. No restriction is placed on its side lengths or angles. A d-flat is a translate of a d-dimensional linear subspace. A section of T by such a flat L is the entire intersection T ∩ L.

The target is the following existence assertion. For every d-polytope P with at most k+1 facets, every k-simplex T in R^k, and every p in the interior of T, there is a d-flat L such that

$$p\in L,\qquad T\cap L\text{ is affinely equivalent to }P.$$

An affine equivalence here preserves affine combinations and is invertible on the affine spans. It can change lengths and angles. In the stated coordinates, it is represented by an injective real affine map A from R^d onto L satisfying

$$A(P)=T\cap L.$$

All input data, including the interior point p, are universally quantified before the flat and map are chosen. The flat can depend on these data. The source writes the facet allowance as f and the simplex dimension as f−1; the notation here uses f=k+1.

The prescribed-point conclusion gives control beyond the existence of some simplex section representing P. It permits the simplex and an interior point to be fixed while the cutting flat is selected to recover the given polytope. The conclusion concerns its full affine geometry: the image of every point of P lies in the section, and every point of the section belongs to that image. This is the additional representational constraint discussed immediately before Theorem 10 on printed page 74.

The difficulty lies in meeting these requirements simultaneously. A flat through the chosen point can have an intersection of the wrong affine shape. A section with the correct affine shape need not contain the prescribed point. The theorem requires both properties for every allowed simplex and point, while retaining the original facet bound. Neither a special regular simplex nor a selected interior point captures this quantifier structure.

The formal statement uses real coordinate spaces indexed by finite sets, finite convex hulls, affine spans, exposed faces, and affine maps. Nonempty faces are counted by their affine dimension. In dimension zero the facet allowance is automatic: under the convention counting the empty face it contributes at most one facet, which fits the allowance k+1. This avoids interpreting natural subtraction d−1 as a facet dimension at d=0. The zero-dimensional simplex and zero-dimensional polytope remain within the statement.

This is a known geometric theorem whose formal proof remains to be supplied. The target contains one proof placeholder. The definitions specify the underlying geometry concretely. The mission consists of the single prescribed-section theorem; its definitions support that statement, and no separate supporting theorem is included as a milestone. The source is Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 10, printed page 74 (source.pdf page 100); see also §5.1, printed page 71 (PDF page 97), for the section convention.

Gale data and combinatorial type

A convex polytope has geometric coordinates and a combinatorial structure: its faces, ordered by inclusion. Different coordinates can describe the same combinatorial type. Gale transforms connect these viewpoints by encoding affine dependencies among the vertices as another point configuration, often in a smaller-dimensional space.

Let P and Q be full-dimensional d-polytopes in real coordinate space, each with n vertices. Choose injective lists V and W containing all their vertices and fix a permutation θ of the n indices. The question is whether this prescribed vertex correspondence extends to an isomorphism between the full face posets of P and Q. The empty face and the whole polytope are included in these posets.

An affine dependency of V is a list of real coefficients a whose sum is zero and whose weighted sum of the vertices is zero. These coefficient lists form a vector space of dimension n−d−1. Choose any basis and put its vectors into the columns of a matrix. The n rows of this matrix form a Gale transform G of V. A Gale transform H of W is constructed in the same way, with its own choice of basis. The rows may repeat and may be zero; there is no general-position assumption.

Theorem 5.4.5 states that the prescribed correspondence extends to an isomorphism of face posets exactly when it preserves every relative-interior test on the Gale configurations. For every subset J of vertex indices, the origin belongs to the relative interior of the convex hull of the rows G(J) if and only if it belongs to the relative interior of the convex hull of H(θ(J)). Relative interior means interior within the affine span of the selected convex hull, not interior in the whole coordinate space.

The equivalence concerns every subset of indices and both directions of implication. It retains the prescribed permutation rather than merely asking whether the polytopes have some combinatorial equivalence. Indexing the Gale points also keeps track of which original vertices they represent when several Gale rows coincide. Taking a set image does not change the convex hull of a chosen subconfiguration.

The empty subset is included: its convex hull has empty relative interior, so both membership tests are false. For a simplex, n=d+1 and the Gale space has dimension zero. Its nonempty row subconfigurations consist of the zero vector, and the relative-interior formulation still applies. Zero-dimensional polytopes are also retained.

This mission is the equivalence criterion itself, with the concrete definitions of a full-dimensional polytope, its face poset, and a Gale transform. The grouping keeps transform construction within the vocabulary of the criterion. The neighboring results on affine and projective equivalence have different conclusions and are outside this goal.

Source: Branko Grünbaum, Convex Polytopes, second edition (2003), §5.4, Theorem 5, printed page 89 (PDF page 115). The affine-dependence construction appears on printed pages 85–86 (PDF pages 111–112).

Change of variables along random paths

The ordinary chain rule describes how a smooth function changes along a differentiable path. A continuous stochastic path can have fluctuations whose accumulated squared increments remain visible even when the time partition becomes arbitrarily fine. The change of variables formula must account for these fluctuations as well as the part of the path with finite variation. Ethier and Kurtz give this identity for time-dependent functions of multidimensional continuous semimartingales in Chapter 5, Theorem 2.9, equations (2.40)–(2.41), of Markov Processes: Characterization and Convergence.

Processes and smooth functions

Work on a complete probability space with a filtration, an increasing family of sigma algebras describing the information available at each nonnegative time. The initial sigma algebra contains every ambient null set. For each coordinate, a continuous semimartingale has a decomposition

$$X_i(t)=X_i(0)+V_i(t)+M_i(t).$$

The initial vector is measurable with respect to the initial information. Each process $V_i$ is continuous and adapted, starts at zero, and has bounded variation on every bounded time interval. Each $M_i$ is a continuous adapted local martingale, initially zero almost surely: stopping along a suitable sequence of stopping times tending to infinity gives martingales. No Brownian driver or diffusion coefficient is specified.

Let $f(t,x)$ be a real-valued function of nonnegative time and a vector in $\mathbb R^d$. The regularity class $C^{1,2}$ requires joint continuity of the function, its first time derivative, all first spatial derivatives, and all second spatial derivatives. The time derivative at zero is interpreted from the right. The hypotheses impose no compact support, global derivative bound, or second time derivative.

The change of variables identity

The goal is the complete identity

$$\begin{aligned} f(t,X(t))-f(0,X(0))={}&\int_0^t f_t(s,X(s))\,ds\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dV_i(s)\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dM_i(s)\\ &+\frac12\sum_{i,j}\int_0^t f_{x_ix_j}(s,X(s))\,d\langle M_i,M_j\rangle_s. \end{aligned}$$

It holds almost surely simultaneously for every nonnegative time. The quadratic covariation $\langle M_i,M_j\rangle$ records the limit of sums of products of increments. Both diagonal and off-diagonal contributions occur. The bracket processes and integral versions are supplied by the conclusion, rather than imposed as additional restrictions on the input processes.

What the identity supplies

The formula determines how a smooth observation of the evolving state changes. Its terms separate explicit time dependence, finite-variation motion, martingale fluctuations, and their second-order correction. This is the calculus result for a given continuous semimartingale; existence or uniqueness of solutions to a stochastic differential equation is a separate mathematical question. The target is the known theorem in the cited book. Its mathematical assertion includes existence of the integral versions appearing in the displayed identity.

Why continuity does not give the ordinary chain rule

Continuity of the sample paths does not imply bounded variation of the martingale component. Consequently, ordinary pathwise integration against that component does not supply the needed calculus. The stochastic integral requires a probabilistic limiting interpretation. A further issue is the exceptional set: an identity established separately at each time does not by itself provide one event of full probability on which it holds at every time. The continuous versions and the order of the quantifiers address that distinction.

Representations and boundary conventions

Coordinates are indexed by Fin d, and time is nonnegative. Allowing zero coordinates also includes the consistent case of a function of time alone. A dyadic partition has $2^n$ intervals, so the denominators in the defining sums are nonzero, including at partition level zero. At time zero all increments vanish.

The finite-variation integrals are characterized pathwise by limits of left dyadic sums. The stochastic integrals are continuous adapted processes characterized by convergence of those sums in probability at each fixed time. The cross brackets are characterized by the corresponding increment-product sums and are required to have continuous adapted versions of locally bounded variation. These predicates do not assume the change of variables identity. The ordinary time integral has a continuous integrand on each compact interval, so its integrability follows from the stated hypotheses. The source's almost-sure version conventions are retained; right continuity of the filtration is not an additional hypothesis.

Selected reference

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. Chapter 5, Stochastic Integral Equations, §2, Theorem 2.9, printed p.287 (held PDF p.296). Probability-space and version conventions: printed pp.279–280 and 286 (PDF pp.288–289 and 295).

From local evolution to a Markov process

A stochastic process can be described through the way functions of its state change over time. For a suitable pair of functions f and g, the difference between f evaluated along the process and the accumulated integral of g has zero conditional drift. A martingale problem specifies a collection of such pairs. The question is whether these local conditions determine the evolution of the process, including the dependence of its future on its past. Ethier and Kurtz's Chapter 4, Theorem 4.1 answers this question under analytic hypotheses on the collection of pairs and a separation condition on the functions being observed.

State space, functions, and histories

Let E be a separable metric space, with its Borel sigma algebra. Write B(E) for the bounded real Borel functions, equipped with the uniform norm. A linear relation A is a linear subspace of B(E) × B(E). A pair (f,g) in A prescribes g as the drift associated with f; the relation is allowed to be multivalued. It is dissipative when

$$a\|f\|\leq\|af-g\|\qquad ((f,g)\in A,\ a>0).$$

Let μ be a probability measure on E. A solution X of the martingale problem for (A,μ) is a jointly measurable process on a probability space with initial law μ, satisfying the compensated moment identities of Chapter 4, equation (3.4). Those identities test each compensated increment against products of bounded Borel functions of finitely many earlier states. The natural past at time s is the sigma algebra generated by all coordinates X(r) with r≤s.

A subspace L of B(E) is separating if two Borel probability measures that have the same integral against every function in L must be equal. This is a condition on measures, stronger in purpose than merely distinguishing individual states.

Characterization target

Suppose A′ is a linear subrelation of A and, for some λ>0,

$$\overline{\mathcal R(\lambda-A')}=\overline{\mathcal D(A')}=L,$$

where both closures use the uniform norm and L is separating. Given a solution X of (A,μ), the target is the existence of a strongly continuous contraction semigroup T on L generated by the closed relation $\overline{A'}$, together with

$$\mathbb E[f(X(s+t))\mid\mathcal F_s^X]=(T(t)f)(X(s))\quad(s,t\geq0,\ f\in L).$$

The process is Markov: for every bounded Borel observable, conditioning a future observation on the entire past agrees almost surely with conditioning on the present state. In addition, any other solution with initial law μ has exactly the same finite-dimensional distributions as X. The competing solution may live on a different probability space. Existence of X is an assumption; the existence conclusion concerns its corresponding semigroup.

What the characterization establishes

The theorem joins an analytic description of evolution with a probabilistic one. The closed generator relation determines a semigroup, while the martingale identities identify the conditional evolution of the supplied process. Separation allows observables in L to determine probability laws. Uniqueness concerns every finite list of observation times, which is the source's convention for this martingale problem.

This is a known theorem of Ethier and Kurtz. The formalization target is its complete statement and eventually a machine-checked proof. The present theorem remains a proof obligation. Its expression infrastructure consists of bounded functions, the natural past, and the finite-history definition of a solution.

Mathematical difficulty

The observed functions initially lie in a subspace L, whereas the Markov conclusion ranges over all bounded Borel observations. Identifying only individual expectations does not by itself establish conditional evolution or equality of joint laws. The analytic part must also identify the entire generator graph: agreement on the original relation alone is weaker than the asserted equality with its closure. Both closure hypotheses and probability-measure separation are therefore part of the target.

Formalization scope

Bounded functions are actual pointwise real functions with the uniform norm. Borel measurability is imposed on the relation, and uniform limits preserve it. The construction does not use functions modulo almost-everywhere equality. The state space is separable and metric; completeness and local compactness are not additional hypotheses. Processes need no right-continuous or cadlag paths.

Histories may be empty, repeated, or unordered, with every history time at most the start of the increment. Products combine repeated observations. Boundedness and finite time intervals ensure the required integrability. Nonnegative real times index the processes. The semigroup is represented by a real-indexed family whose axioms concern nonnegative times; negative-time values have no mathematical role. Generator equality is a biconditional for the derivative limit from positive times. The target retains semigroup correspondence, the ordinary Markov property, and unrestricted finite-dimensional uniqueness as one theorem.

Selected references

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 4, Theorem 4.1, printed p.182 (PDF p.191); equations (3.4) and (4.2), printed pp.174 and 183. Separation conventions: Chapter 3, printed pp.112 and 116. Chapter 4.

Martingales with partially ordered time

Optional sampling relates a process observed at two random times. A martingale has a conditional expectation at an earlier index equal to its value there, but this defining property initially concerns deterministic indices. Random indices require a separate theorem. In Chapter 2, Section 8, Ethier and Kurtz extend optional sampling to a partially ordered family of indices for use in the time changes of Chapter 6. The target is their Theorem 8.7, printed pages 87–88.

Metric lattices and information

A metric lattice is a partially ordered metric space I in which each pair of points has a greatest lower bound and a least upper bound. These are written as the meet and join. Both operations are jointly continuous. Points need not be comparable. The interval between u ≤ v consists of all points w with u ≤ w ≤ v.

A subset is separable from above if it contains a sequence aₙ that approximates each of its points w by the finite meets of those aᵢ with w ≤ aᵢ and i ≤ n. Each such meet is taken once this finite set is nonempty. The resulting sequence of meets must converge to w. The theorem assumes this condition for each interval.

Let Ω carry a probability measure P and an ambient sigma algebra. A filtration assigns a sub-sigma algebra Fᵤ to each index u, increasing with the order. A real-valued process X is a martingale if each X(u) is Fᵤ-measurable and integrable and, whenever u ≤ v,

$$E[X(v)\mid F_u]=X(u)\quad\text{almost surely}.$$

Right continuity here has a specific lattice meaning: for every u and every outcome ω, X(u ∨ v,ω) tends to X(u,ω) as v tends to u. A stopping time τ is a Borel-measurable I-valued random variable such that {τ ≤ u} belongs to Fᵤ for every u.

The optional-sampling target

Take stopping times τ₁ ≤ τ₂ pointwise. Suppose there are deterministic sequences uₙ and vₙ in I such that

$$P\{u_n\leq\tau_1\leq\tau_2\leq v_n\}\longrightarrow1,$$

and

$$E[|X(v_n)|\mathbf1_{\{\tau_2\leq v_n\}^{c}}]\longrightarrow0.$$

Assume also that X(τ₂) is integrable. The target is

$$E[X(\tau_2)\mid F_{\tau_1}]=X(\tau_1)\quad\text{almost surely}.$$

The sigma algebra Fτ consists of ambient-measurable events A for which A ∩ {τ ≤ u} belongs to Fᵤ for every u. This is the information used in the conclusion.

What the result provides

The conclusion extends the martingale identity to random lattice indices under explicit exhaustion and tail assumptions. Neither a deterministic bound on both stopping times nor a linear ordering of all indices is part of the statement. This is a known theorem in the cited book. The formal target retains the full conditional-expectation identity; its proof remains to be formalized.

Why the hypotheses matter

In a partially ordered space, the complement of {τ₂ ≤ vₙ} includes incomparable indices. Replacing this complement by {vₙ < τ₂} would change the tail assumption. Likewise, right continuity must use lattice joins, rather than a one-dimensional time convention. Controlling probabilities of the exhaustion events alone does not state the integrability control required by the second limit. Both limits belong to the theorem.

Mathematical scope and conventions

The index space has a metric and a lattice structure with continuous meet and join. No top, bottom, completeness of the metric, or linear order is required. The filtration need not be complete or right continuous. The stopping times are finite I-valued variables; their measurability is explicit. The sequences uₙ and vₙ need not be monotone. The nonnegative tail expectation uses extended nonnegative integration, avoiding a default value for a nonintegrable real integral. Indexwise integrability is retained explicitly, along with terminal integrability.

The two accompanying definitions express separation from above and the stopped sigma algebra. Together with the martingale and stopping-time conditions, they specify the single optional-sampling theorem. The target contains no additional supporting-theorem milestones.

Source

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 2 §8, Theorem 8.7, printed pp. 87–88 (supplied PDF pp. 96–97); definitions and equation (8.6), printed p. 85 (PDF p. 94). Chapter 2.

Why two types change the limit

Critical branching is a basic scaling model for populations whose expected size neither grows nor decays at leading order. A single-type population has one macroscopic direction, but a two-type population has two coupled directions. In the critical regime considered by Ethier and Kurtz, one weighted population mode survives on the diffusive scale while a second mode is pulled rapidly toward zero. The rapid mode still leaves a random integrated contribution and an initial boundary layer, so discarding it would lose part of the limiting dynamics. The mission packages all of these conclusions from Chapter 9, Section 2, Theorem 2.1 of Ethier and Kurtz as one formal target.

The branching model

The state is a pair of natural numbers recording the numbers of particles of types 1 and 2. A type-$i$ particle lives for an exponential time with positive rate $\lambda_i$. At death it is replaced by a random pair of offspring with law $\rho_i$. The generator therefore applies the type-specific replacement rule at an intensity proportional to the current number of particles of that type. The formal predicate IsTwoTypeBranching records a measurable càdlàg process satisfying the corresponding natural-past martingale identities on finite-support tests, with an explicit integrability condition.

The offspring mean matrix has strictly positive entries. Its critical weighted rate matrix has a positive eigenvector $\nu$ with eigenvalue zero and an opposite-sign eigenvector $\mu$ with eigenvalue $-\eta$, where $\eta>0$. For the $n$th process, Lean consistently uses the positive index $n+1$. At accelerated time $(n+1)t$, the scaled modes are

$$X_n(t)=\frac{\nu_1 Z^{(n)}_1((n+1)t)+\nu_2 Z^{(n)}_2((n+1)t)}{n+1}, \qquad Y_n(t)=\frac{\mu_1 Z^{(n)}_1((n+1)t)+\mu_2 Z^{(n)}_2((n+1)t)}{n+1}.$$

The compensated fast coordinate is

$$W_n(t)=Y_n(t)+\int_0^t (n+1)\eta Y_n(s)\,ds.$$

Formalization target

The goal is the complete three-part statement of Theorem 2.1. First, $(X_n,W_n)$ converges jointly in path law to a continuous two-dimensional diffusion $(X,W)$. Its covariance matrix is built from the raw second moments of the two offspring replacement increments, and its generator has the form

$$Af(x,w)=\frac{x}{2}\left(a_{11}f_{xx}+2a_{12}f_{xw}+a_{22}f_{ww}\right)(x,w).$$

Second, on every finite time interval the fast mode is uniformly close in probability to its exponentially decaying initial layer $Y_n(0)e^{-(n+1)\eta t}$. On every interval $0<t_1<t_2$, its integrated drift converges weakly to $W(t_2)-W(t_1)$. Third, the first population coordinate is uniformly reconstructed from $X_n$ together with that same initial layer. The limit statement keeps the possibly nonzero initial fast coordinate and the separate nonnegativity conclusion for the slow coordinate.

What the result supplies

The theorem identifies both the persistent and collapsing directions of a critical multitype system. The slow direction produces population-scale diffusion, while the compensated fast direction records fluctuations that remain visible after the raw fast mode contracts. The reconstruction formula connects these mode coordinates back to the original particle count. Keeping the path limit, fast decay, integrated limit, and reconstruction together prevents an apparently simpler marginal statement from omitting the initial-layer behavior needed at time zero.

The textbook theorem is already mathematically proved. This mission asks for a Lean proof of the reviewed formal statement; the uploaded goal is intentionally a statement with a proof placeholder, not a claim of machine-checked completion. The concrete generator, branching-law predicate, scaling map, càdlàg condition, and diffusion martingale-problem predicate provide reusable vocabulary for related multitype limit theorems.

Where the formal difficulty lies

Coordinatewise convergence is insufficient. The result couples full path laws, a continuous diffusion martingale problem, compact-uniform control of an initial layer, and a positive-time integral of a rapidly changing mode. The naive step of simply setting the fast mode to zero fails at time zero and erases the exponential term needed in the population reconstruction. The covariance coefficients also come from replacement increments rather than centered offspring counts, so changing that convention alters the limiting operator.

Formalization scope and conventions

The state space is exactly $\mathbb N\times\mathbb N$; both offspring laws are probability measures, both coordinates have finite third moments under each parent law, and all four entries of the mean matrix are positive. Initial populations are deterministic floors of $(n+1)z_i$ for nonnegative densities $z_i$. The positive indexing avoids division by zero in every scaling, clock, and exponential. Natural-number subtraction in the generator is used only with a zero event intensity when the relevant population is empty.

Path convergence is represented by a joint probability-space realization carrying the correct complete prelimit path laws and almost-sure uniform convergence on compact intervals to a continuous limit. This is the continuous-limit Skorohod convention used in the reviewed development. The definitions are concrete: none contains the target theorem or assumes its conclusions. The mission includes only expression-essential dependencies, reusing exact private book-wide definitions for càdlàg paths and the continuous diffusion generator law. It does not add proof-only lemmas or split the three source conclusions into separate missions.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 9, Section 2, Theorem 2.1, printed pp. 392–393. DOI

Why reconstruction from partial face data matters

A convex polytope has both a geometric realization and a finite combinatorial structure: its faces, ordered by inclusion. Reconstruction asks how much of that structure must be known before the rest is forced. Chapter 12 of Branko Grünbaum's Convex Polytopes distinguishes several forms of unambiguity and then proves reconstruction results for general polytopes and for important special classes. The central input is not a coordinate description. It is a lower-dimensional part of the face lattice, such as the graph or a higher skeleton.

This mission groups five established results that address the same recovery problem under different hypotheses. The main theorem reconstructs every d-polytope, for d ≥ 3, from a supplied equivalence of its (d−2)-skeleton. The supporting targets sharpen the amount of data needed for simple polytopes, simplicial polytopes, and zonotopes, and record a polynomial-time version whose output is the vertex–facet incidence relation. Each theorem retains its own quantified polytopes, equivalence, and reconstruction witness. Grouping them does not require a single witness to serve all five regimes.

Face lattices, skeletons, and unambiguity

A d-polytope is represented as the convex hull of a nonempty finite subset of Fin d → ℝ, with affine span equal to the whole ambient space. A face is an exposed face in Mathlib's sense. This convention includes the empty face and the polytope itself. PolytopeFace P is the resulting face poset ordered by set inclusion.

For a natural number k, the k-skeleton face poset SkeletonFace P k contains the empty face and every nonempty exposed face whose affine dimension is at most k. An equivalence of skeletons is an order equivalence, so it preserves and reflects every inclusion relation among the retained faces. Strong unambiguity is represented by demanding an extension of every supplied skeleton equivalence, rather than merely asserting that some full face-lattice equivalence exists. The extension equation requires agreement on every skeleton face.

The graph of a polytope is modeled through its vertices and one-dimensional faces. PolytopeVertex P consists of points whose singleton is exposed. Two distinct vertices are adjacent in polytopeGraph P when they lie in a common one-dimensional exposed face. A source polytope is simple when every vertex has exactly d graph neighbors. A simplicial polytope is one whose facets are simplices. A zonotope is a finite vector sum of closed line segments; full dimension is imposed separately by the d-polytope hypothesis.

Formalization targets

General reconstruction from the (d−2)-skeleton

For d ≥ 3, d-polytopes P and Q, and every supplied order equivalence

$$\varphi:\operatorname{Skel}_{d-2}(P)\simeq_o\operatorname{Skel}_{d-2}(Q),$$

the main target produces an order equivalence of the complete face posets whose restriction is exactly φ. This is the explicit face-lattice reformulation of Theorem 12.3.1. It asserts strong and weak d-unambiguity, but it does not add dimensional unambiguity.

Reconstruction from graphs and half-dimensional skeletons

The Blind–Mani target uses only the 1-skeleton when the source is simple. The target polytope is arbitrary in the same dimension; its simplicity is not assumed separately. The Björner–Edelman–Ziegler target likewise uses the 1-skeleton when the source is a full-dimensional zonotope, without requiring the target to be a zonotope.

Perles's target has a different domain. The source is a simplicial d-polytope, the target is an arbitrary e-polytope, and the input compares their floor(d/2)-skeletons. Its conclusion includes both e=d and extension of the supplied skeleton equivalence. Thus this clause, unlike the other reconstruction clauses, explicitly includes dimensional unambiguity.

Polynomial-time incidence reconstruction

The algorithmic target states that one binary function works uniformly for every d ≥ 3, every vertex count, and every valid labelled d-polytope input. The input contains the complete duplicate-free table of nonempty faces in dimensions at most d−2; the output contains exactly the facets, as labelled vertex sets. Dimension, vertex count, and row count are self-delimiting headers, followed by dense incidence rows. Correctness is required on valid encodings, while the binary function itself is total. ContainmentPolyTime uses Mathlib's Turing-machine polynomial-time predicate together with finite stack alphabets.

Significance

The general theorem says that codimension-two face data already fixes every missing facet and incidence relation. The special-class results show that much smaller data can suffice: only the graph for simple polytopes and zonotopes, and the half-dimensional skeleton for simplicial polytopes. Perles's result also recovers ambient dimension. The algorithmic theorem separates mere uniqueness from effective recovery by requiring one polynomial-time procedure and a concrete vertex–facet output.

Formalizing these results creates reusable interfaces for face-poset reconstruction, graph-based simplicity, zonotopes, and finite incidence encodings. It also records distinctions that informal summaries can blur: extension of every supplied equivalence versus existence of an unrelated isomorphism; combinatorial reconstruction versus dimension recovery; and uniqueness versus polynomial-time computability. The statements are established mathematics, but their Lean theorem bodies remain open and use sorry; this mission makes no proof-completion claim.

Difficulty

Counting faces or matching their dimensions does not reconstruct the face lattice. The conclusion must preserve every inclusion relation and agree with the specific equivalence supplied on the visible skeleton. An arbitrary isomorphism of complete face lattices would be too weak if it failed to extend that map.

For simple polytopes and zonotopes, graph isomorphism alone does not expose higher-dimensional faces directly; the target still asks for all incidences. In the simplicial case, reconstructing the lattice without proving e=d would omit the dimensional-unambiguity clause. For the effective result, a mathematical reconstruction argument is insufficient unless it yields one uniform polynomial-time binary function. Conversely, an efficient procedure on an incomplete or coordinate-dependent input would not meet the stated incidence model.

Formalization scope

All geometric ambient spaces are finite-dimensional real coordinate spaces. Full-dimensional polytopes are nonempty finite convex hulls. Exposed faces include both improper faces. Skeletons retain the empty face separately, avoiding a natural-number encoding of its source dimension −1. Natural subtraction in d−2 is protected by the explicit 3 ≤ d hypothesis wherever that threshold is used.

The graph definition removes loops and symmetrizes adjacency. Simplicity is the exact neighbor-cardinality condition at every vertex. The zonotope definition allows arbitrary segment endpoints and degenerate summands, but the separate full-dimensionality hypothesis rules out a lower-dimensional source. Only the simplicial theorem compares different ambient dimensions and concludes their equality.

The algorithm receives no real coordinates. Its vertex map is injective and has range exactly the exposed singleton faces. The input and output row predicates are biconditionals, so they prohibit missing faces and extraneous rows; Nodup prohibits repetitions. The empty face is implicit, and the output row order is unrestricted. Contributions must not weaken extension to unrelated existence, assume the target belongs to the source's special class, omit Perles's dimension equality, replace complete incidence tables by partial data, or allow the polynomial bound to depend on the individual instance.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §§12.1–12.4 and §15.1. DOI: 10.1007/978-1-4613-0019-9.
• Roswitha Blind and Peter Mani-Levitska, Puzzles and polytope isomorphisms, Aequationes Mathematicae 34 (1987), 287–297. DOI: 10.1007/BF01830678.
• Anders Björner, Paul H. Edelman, and Günter M. Ziegler, Hyperplane arrangements with a lattice of regions, Discrete & Computational Geometry 5 (1990), 263–288. DOI: 10.1007/BF02187791.

Motivation

A stochastic linear program is a linear optimization problem whose coefficients depend on a random parameter. Even when the model is feasible and bounded almost surely, its optimal value is itself a random quantity. Knowing only its expectation can hide the probability of unusually favorable or unfavorable outcomes; its full distribution supports threshold probabilities, quantiles, and later risk-sensitive decisions. Chapter II of Peter Kall's Stochastic Linear Programming develops a finite-dimensional method for determining that distribution when the constraint matrix, right-hand side, and objective coefficients depend affinely on the same random vector. Theorem 8, printed p. 29 / PDF35, is the chapter's general distribution formula. This mission asks for that known theorem to be proved in Lean from its reviewed statement.

Setting

Fix a finite parameter vector $t\in\mathbb R^r$. An affine random linear program supplies a matrix $A(t)\in\mathbb R^{m\times n}$, a right-hand side $b(t)\in\mathbb R^m$, and costs $c(t)\in\mathbb R^n$, each affine in $t$. Its optimal value is the extended-real infimum

$$\gamma(t)=\inf\{c(t)^\top x:A(t)x=b(t),\ x\ge 0\}.$$

The parameter has a probability law $\mu$, supported almost surely on a measurable set $T$, with a nonnegative extended-real density $f$ relative to Lebesgue measure. The extended-real value records infeasibility as $+\infty$ and unboundedness as $-\infty$; the target distribution deliberately restricts to the finite-value event $-\infty<\gamma(t)\le\xi$.

A candidate basis is an increasing selection $\sigma:\operatorname{Fin}(m)\to\operatorname{Fin}(n)$. Its basis matrix $B_\sigma(t)$ consists of the selected columns of $A(t)$. Kall enumerates exactly those candidate bases whose determinant is nonzero at some point of $T$. For each one, its raw optimality region consists of the parameters for which $B_\sigma(t)^{-1}b(t)\ge0$ and the reduced costs $c(t)^\top-c_B(t)^\top B_\sigma(t)^{-1}A(t)$ are nonnegative. Matrix inversion is totalized to zero at singular matrices, matching the source convention. The ordered basis regions remove every earlier raw region, so overlapping optimal bases are assigned to the first enumerated basis. On a basis region the associated value is

$$\gamma_\sigma(t)=c_B(t)^\top B_\sigma(t)^{-1}b(t).$$

Assumption A1 is explicit in Lean: the density and support clauses above, both almost-sure feasibility/boundedness implications from Theorem 4, and the existence of one full-row-rank column minor at a point of $T$. The basis enumeration is injective and exhaustive for the almost nonsingular increasing selections.

Formalization targets

Theorem 8: distribution by basis regions

For the ordered regions $B_i$, the theorem states

$$\mu\!\left(\bigcup_i B_i\right)=\sum_i\mu(B_i)=1.$$

For every real threshold $\xi$, it further identifies the finite optimal-value distribution by

$$\mu\{t\in T:-\infty<\gamma(t)\le\xi\} =\sum_i\int_{\{t\in B_i:\gamma_i(t)\le\xi\}} f(t)\,dt.$$

The normalization and distribution identity are the two clauses of the same source theorem and remain one goal. Determinant facts, special stochastic models, and examples elsewhere in the chapter are context rather than additional mission targets.

Significance

The result turns the distribution of a random optimization value into a finite sum of ordinary density integrals over explicitly described parameter regions. It connects parametric linear programming geometry with probabilistic questions about the optimum and provides the chapter's foundation for studying particular stochastic models and derived distributional quantities. Without the coverage and normalization clauses, the integral expression could omit positive-probability parameter regimes; without the finite-value event, extended-real exceptional outcomes would be conflated with a real-valued distribution function.

The theorem is established in the 1976 source, but the staged Lean declaration contains a proof placeholder. Completing it would produce a machine-checked account of the basis-region decomposition under the source's full hypotheses. The reusable content includes the affine model, basis matrix, raw-region inequalities, ordered disjointification, basis value, and the referenced extended-real linear-program value.

Difficulty

The natural pointwise argument chooses an optimal basis and substitutes its basic solution. That alone does not prove a measurable probability decomposition: several bases may be optimal at the same parameter, bases may become singular on exceptional sets, and the optimal value may be infinite. The ordered subtraction of earlier regions resolves overlap only after one proves exhaustive coverage under A1. The final equality must also connect the extended-real infimum to the real basis value on each region and justify the density integrals on the threshold sets. Treating the raw regions as automatically disjoint or silently assuming every parameter has a unique nonsingular optimizer would bypass the central issues.

Formalization scope

All dimensions and basis lists are finite. The law is a probability measure on $\operatorname{Fin}(r)\to\mathbb R$, represented as volume.withDensity f; $T$ is measurable and carries the law almost surely. The density is ENNReal-valued and the displayed integrals are nonnegative lintegrals. No integrability or finite-moment hypothesis is imposed on the optimal value. LPValue is an existing referenced platform definition using EReal.sInf; the book-local declarations remain in the shared Kall1976 namespace. Mathlib's nonsingular inverse supplies the source's zero value at singular matrices.

The formal target must retain both almost-sure implications, the one-point full-rank condition, increasing and exhaustive basis enumeration, region ordering, probability-one normalization, the strict lower bound by $-\infty$, and the weak upper threshold $\le\xi$. Removing any of these clauses would change the reviewed theorem rather than simplify its proof. Contributions may develop measurable-region, finite-basis coverage, LP optimality, and density-integration lemmas, provided they preserve these conventions.

Selected references

• Peter Kall, Stochastic Linear Programming, Springer, 1976, Chapter II §1: Theorem 4 printed p. 25 / PDF31; model (5) printed p. 27 / PDF33; Assumption A1 printed p. 28 / PDF34; Theorem 8 printed p. 29 / PDF35. DOI.

Why infinite spin systems need a generation theorem

A spin-flip system models a countable collection of two-state components whose transition rates may depend on the entire current configuration. Such systems are basic examples of interacting particle processes: each local move is simple, but infinitely many possible moves may be active and their rates interact through the configuration. The central analytic question is whether the formal sum of local flip operators determines a genuine time evolution on continuous observables. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, answers this question under uniform rate and influence bounds Ethier--Kurtz, Theorem 3.5.

This mission states that result without replacing the countable system by a finite-state chain or assuming finite total jump intensity. It also retains the theorem's cylinder-function core, which identifies finitely coordinate-dependent observables as a sufficient starting class for recovering the closed generator.

Configuration space and coordinate variation

Let S be a countable type of sites. A configuration is a function η : S → Bool; false and true relabel the source spins -1 and 1. The product topology on these configurations is the one induced by the discrete topology on each coordinate. The Lean space C(S → Bool, ℝ) consists of real-valued continuous observables on this compact product space and carries its uniform norm.

For a site i, spinFlip i η agrees with η away from i and negates the Boolean value at i. For an observable f, its coordinate variation at i is

$$\operatorname{var}_i(f)=\sup_{\eta}\left|f(\operatorname{flip}_i\eta)-f(\eta)\right|.$$

The domain used in the theorem is the full class of continuous observables for which ∑ i, var_i(f) is summable. This is a one-coordinate variation domain: it measures the effect of changing one spin, rather than exchanging two occupied sites.

For every site i, the flip rate c i is itself a continuous function of the configuration. Rates are nonnegative and uniformly bounded in the uniform norm. Their dependence on other coordinates is controlled by a second uniform bound: for each i, the series ∑ j, var_j(c i) is summable, with a bound independent of i. These are the two clauses of equation (3.24).

Formalization target

The pre-generator graph implements equation (3.25). For every pair (f,g) in that graph, f has summable coordinate variation and

$$g(\eta)=\sum_i c_i(\eta)\bigl(f(\operatorname{flip}_i\eta)-f(\eta)\bigr).$$

The goal is Theorem 3.5 in full. It asserts that every function in the prescribed domain has a continuous image in the graph; the closure of the graph in the product uniform-norm topology is single-valued; and that closure is exactly the generator graph of a strongly continuous contraction semigroup. The semigroup is positive and preserves the constant function one, giving the conservative Feller conclusion used by the source.

The final clause retains the source's cylinder core. Restrict the initial graph to functions depending on a finite set of coordinates, expressed by the existence of a finite set F such that agreement on F forces equal function values. The closure of this restricted graph equals the full generator graph. Generation and the core are kept together because both are conclusions of the same theorem.

Significance of the result

The result turns an infinite formal sum of local moves into a closed, single-valued Markov generator. This is stronger than merely defining the pointwise series: it supplies the strongly continuous positive contraction evolution, conservativity, and the derivative characterization of the entire generator domain. The cylinder-core clause means that finite-coordinate observables are graph-norm dense enough to recover that generator, even though the state space and the total collection of possible flips are countable.

The theorem is already proved in the source. The formalization target is its precise Lean statement, including the infinite-site domain, the uniform influence hypothesis, generator closure, and core. The reusable infrastructure consists of the book-wide strongly continuous contraction-semigroup predicate and the mission-local flip, variation, and graph definitions.

Where the analytic difficulty lies

The naive finite-rate jump argument does not apply. A uniform bound on each individual rate does not bound the sum of rates over a countably infinite site set, so the system may have infinite total potential flip intensity. Pointwise notation for the generator also does not by itself show that its image is continuous or that its graph closure is single-valued. The coordinate-influence bound and summable-variation domain are therefore essential parts of the target rather than optional regularity decoration.

The neighboring exclusion-process theorem is not interchangeable with this one. A spin flip changes one coordinate and permits creation or destruction of occupation, whereas exclusion dynamics exchanges two coordinates and conserves particle number. Their domains and rate conditions are correspondingly different.

Formalization scope

The Lean statement allows empty, finite, and countably infinite S; it does not impose nonemptiness or finiteness. Bool is an exact two-state relabeling, not a restriction to a special numerical spin convention. spinVariation uses a real supremum over the nonempty compact configuration space. Explicit Summable hypotheses prevent divergent real tsum expressions from receiving an unintended default interpretation.

The operator graph uses the actual pointwise series and requires a continuous output. Closure is taken in C(S → Bool, ℝ) × C(S → Bool, ℝ). The semigroup is indexed by real time, but every law and bound uses nonnegative times; negative-time values carry no mathematical requirement. No finite-total-rate hypothesis, finite-site approximation, two-site exchange dynamics, or weakened core statement is admitted.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 1, Section 3; Chapter 4; Chapter 8, Section 3, Theorem 3.5, equations (3.24)--(3.25), printed p. 381. Wiley DOI

Why boundary refinement and skeleton embeddings matter

A convex polytope carries more than its underlying topological ball. Its faces form a finite complex whose incidence relations record the polytope's combinatorial structure. Chapter 11 of Branko Grünbaum's Convex Polytopes asks how this structure can be represented by subdivisions and by embeddings into Euclidean spaces of smaller dimension. The first target places every polytope boundary over the simplest boundary complex in the same dimension, that of a simplex. The second determines exactly how much ambient dimension is needed to realize any prescribed skeleton, both topologically and as a genuine polytopal complex.

These are established mathematical results, not open conjectures. The mission poses their reviewed Lean statements as formal proof tasks. It groups Theorems 11.1.1 and 11.1.9 because both use the boundary-complex, carrier, refinement, skeleton, and incidence-equivalence model introduced at the start of §11.1. They remain separate statements with separate quantified objects; no common homeomorphism, realization, or witness is imposed between them.

Geometric and combinatorial setting

A d-polytope is represented in Lean as the convex hull of a nonempty finite subset of Fin d → ℝ whose affine span is the whole ambient space. A face uses Mathlib's exposed-face convention. For polytopes this includes the proper exposed faces as well as the empty and full improper faces.

The boundary complex boundaryFaces P consists of every exposed face of P except P itself. Thus the empty face is retained. Its carrier is the union of those cells. The statement BoundaryRefines P Q supplies one homeomorphism between the two complete boundary carriers. For each boundary face of Q, its inverse image must be exactly the union of a finite subfamily of boundary faces of P, and that subfamily must be closed under taking faces. Exact inverse-image equality is essential: containment alone would not express the source's refinement relation.

The k-skeleton face poset SkeletonFace P k contains the empty face and every nonempty exposed face of affine dimension at most k, ordered by inclusion. Its topological carrier skeletonCarrier P k is the union of these cells. A finite polytopal complex in real m-space is a finite family of polytopal cells, explicitly permitting the empty cell, closed under taking faces, with each pairwise intersection a face of both participating cells. Combinatorial equivalence is represented by an order isomorphism of the complete cell posets, rather than merely by a homeomorphism of their carriers.

Formalization targets

Boundary refinement by a simplex

For every natural dimension d, every full-dimensional d-polytope P, and every affinely independent family of d+1 vertices in real d-space, the first target states

$$\mathcal B(P)\text{ refines }\mathcal B(T^d).$$

The chosen vertices describe an arbitrary d-simplex. The result does not assume that P is simplicial. The same homeomorphism controls all target-face inverse images, and the zero-dimensional case retains its empty boundary carrier.

Exact skeleton embedding dimensions

For 1 ≤ k ≤ d and every d-polytope P, the second target identifies two attained minima. The first ranges over dimensions m for which the carrier of the k-skeleton is homeomorphic to some subset of real m-space. The second ranges over dimensions m for which a finite polytopal complex in real m-space has a cell poset order-isomorphic to the complete k-skeleton face poset. Both minima equal

$$a(d,k)=b(d,k)= \begin{cases} d, & d\le k+1,\\ \min(d-1,2k+1), & d>k+1. \end{cases}$$

This compact formula preserves the four cases stated in Theorem 11.1.4: d=k, d=k+1, k+2≤d≤2k+2, and d≥2k+2. The latter two formulas agree at their shared endpoint. Applying the arbitrary-polytope statement to simplices retains the source comparison with a(d,k) and b(d,k).

Significance

The refinement theorem gives a uniform relationship between the boundary complex of an arbitrary polytope and the simplex boundary. It preserves both topology and the subdivision data carried by faces. The embedding theorem then gives the exact ambient dimension required by every k-skeleton, while showing that allowing an arbitrary topological embedding does not improve on the best dimension obtainable from a combinatorially equivalent polytopal complex.

Formalizing these targets provides reusable infrastructure for boundary carriers, face-closed refinements, skeleton carriers, and finite polytopal complexes. The definitions distinguish topological equivalence from incidence equivalence and record attainment as well as lower bounds through IsLeast. The theorem bodies remain open: the proposal does not claim that either classical result already has a Lean proof.

Difficulty

For the refinement target, a homeomorphism of boundary carriers alone is insufficient. One must also prove, simultaneously for every target cell, that its inverse image is exactly a finite union of source cells closed under faces. The obvious topological equivalence of polytope boundaries therefore does not establish the required combinatorial refinement.

For the embedding target, constructing one realization in the displayed dimension proves only attainment. It does not rule out all realizations in smaller dimensions. Conversely, a lower-bound argument does not construct the topological subset or polytopal complex required by IsLeast. Both notions of realization must meet at the same explicit value without replacing the full cell-poset equivalence by a weaker topological condition.

Formalization scope

All ambient spaces are finite-dimensional real coordinate spaces. Polytopes are nonempty finite convex hulls, and the goal polytopes are full-dimensional. Exposed faces include the empty face and the whole polytope; the boundary removes only the whole polytope. Skeleton dimension is the real dimension of an affine-span direction, with the empty face admitted separately. The topological minimum ranges over arbitrary subsets with the subspace topology, while the combinatorial minimum ranges only over finite polytopal complexes satisfying face closure and the common-face intersection condition.

IsLeast asserts both membership of the displayed value and that it is a lower bound for every attainable dimension. The condition 1 ≤ k ≤ d excludes the source's untreated k=0 case. Natural subtraction occurs only in the branch d>k+1, so the formula does not gain a truncated-subtraction shortcut. Contributions must not drop attainment, restrict the arbitrary polytope, replace exact inverse-image equality by containment, omit empty faces, weaken order isomorphism to a carrier homeomorphism, or require the two source theorems to share a witness.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §11.1, Theorems 11.1.1, 11.1.4, and 11.1.9. DOI: 10.1007/978-1-4613-0019-9.

Why nonlocal generators matter

Markov processes with jumps model changes that cannot be represented by continuous diffusion paths: arrivals in queueing systems, sudden failures, population events, and discontinuous changes in financial or physical systems. Their infinitesimal descriptions are nonlocal generators, because the value of the operator at a state depends on test-function values at displaced states rather than only on derivatives at the current point. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), treats three complementary regimes. Theorem 3.1 covers finite-rate jumps on a general locally compact state space. Theorem 3.4 treats homogeneous Lévy operators on Euclidean space, including infinite jump activity and degenerate covariance. Theorem 3.3 gives the main target here: well-posedness for a time- and state-dependent compensated Lévy-type martingale problem.

These results connect concrete jump kernels and integro-differential operators to two standard descriptions of stochastic dynamics. Autonomous operators are realized as generators of conservative Feller semigroups, while time-dependent operators are characterized through martingale identities. Keeping all three source results in one mission records the nonlocal-generator theme without claiming that their distinct hypotheses imply one another.

The setting

For the Euclidean results, the state space is $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d), with $d>0$. A covariance field $a(t,x)$ is a continuous linear endomorphism, a drift field $b(t,x)$ is a vector, and $\nu(t,x,dy)$ is a measure of jump displacements. For a smooth compactly supported test function $f$, the compensated Lévy-type operator is

$$L_t f(x)=\frac12\sum_{i,j}a_{ij}(t,x)\,\partial_{ij}f(x) +Df(x)[b(t,x)] +\int\!\left(f(x+y)-f(x)-\frac{Df(x)[y]}{1+\lVert y\rVert^2}\right)\nu(t,x,dy).$$

The denominator in the compensation term is part of the source convention. The covariance factor $1/2$ applies only to the second-order term; the drift is unscaled. The weighted moment $\lVert y\rVert^2/(1+\lVert y\rVert^2)$ permits measures with infinite total mass while controlling the compensated integral.

A solution of the Lévy-type martingale problem is a jointly measurable process with the prescribed initial pushforward law whose integrated-generator increments have zero expectation against every bounded continuous function of any finite history. Smooth compactly supported functions are the spatial tests. This definition imposes no path-continuity requirement.

The finite-rate model uses a locally compact, noncompact, separable metric space $E$, a nonnegative rate $\lambda(x)$, and a weakly continuous probability transition kernel $\mu(x,dy)$. Its operator is $Af(x)=\lambda(x)\int(f(y)-f(x))\mu(x,dy)$. Positive weights $\gamma$ and $\eta$ specify the graph domain and control behavior at infinity.

Formalization targets

Goal: nonautonomous Lévy-type well-posedness

The main target is Chapter 8, Section 3, Theorem 3.3. The covariance is continuous, symmetric, bounded, and strictly positive definite at every nonzero vector, without a uniform ellipticity constant. The drift is measurable and bounded. The weighted jump measure is integrable, and for every measurable set its weighted mass is a bounded continuous function of time and state.

For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every solution on every probability space. Setwise continuity is retained exactly; it is not replaced by weak convergence of measures or by finite total jump intensity.

Related target: homogeneous Lévy generation

Theorem 3.4 freezes the coefficients in time and space. The covariance may be degenerate but is symmetric and nonnegative, and the jump measure needs only the finite weighted integral. The full $\widehat C^2$ graph consists of functions, first derivatives, and second derivatives that vanish at infinity. Its closure is the exact generator of a positive conservative strongly continuous contraction semigroup on $C_0(\mathbb R^d)$, and smooth compactly supported functions form a core.

Related target: finite-rate jump generation

Theorem 3.1 retains the general-state-space jump model. The transition kernel is both setwise measurable and weakly continuous; the rate and weights satisfy the source's vanishing and signed integral bounds. The weighted graph closes to a single-valued conservative Feller generator, and compactly supported continuous functions form a core.

Significance

The main theorem says that the displayed nonlocal characteristics determine stochastic dynamics in distribution even when the drift is only measurable and jump activity need not be finite. The two autonomous theorems identify concrete domains whose closures are genuine Feller generators, including positivity, contraction, strong continuity, conservativity, and core statements. Together they distinguish finite-rate kernels, homogeneous compensated Lévy dynamics, and nonautonomous Lévy-type dynamics while sharing the same generator language.

The formal contribution is a machine-checkable statement layer, not a proof claim. It exposes the exact compensation, weighted-integrability, graph-domain, semigroup, and finite-history conventions on which later proofs depend. The common diffusion operator, bounded-pointwise closure, and strongly continuous contraction-semigroup predicate are reused from earlier private missions in the same textbook series rather than duplicated under conflicting identifiers.

Where the difficulty lies

The obvious finite-jump approximation does not by itself preserve the full conclusions. Infinite jump activity requires compensation near zero, and convergence of the associated operators must still identify the intended martingale problem or the exact closed Feller generator. In the nonautonomous theorem, setwise continuity of weighted jump masses must coexist with merely measurable drift, while uniqueness ranges over arbitrary probability-space realizations and all finite-dimensional laws. Strengthening to continuous drift, imposing finite total jump intensity, assuming uniform ellipticity, or comparing only continuous-path solutions would materially weaken or alter the source theorem.

Formalization scope and conventions

Nonnegative real time is represented by ℝ≥0; Euclidean coordinates use Fin d. Fréchet derivatives express both gradient and Hessian terms. The jump measure is a measure of displacements $y$, so the operator evaluates $f(x+y)$. Integrable hypotheses prevent Lean's totalized integral from silently assigning zero to a divergent positive weighted moment. Positive dimension is explicit through [NeZero d].

The martingale predicate includes empty finite histories and repeated observation times. Its bounded continuous history tests determine the same finite-dimensional identities used by the source, and no sample-path regularity is inserted. The autonomous graphs live in $C_0\times C_0$; bounded-pointwise closure means closure under uniformly bounded pointwise sequential limits, not ordinary norm closure. The finite-rate theorem preserves its restriction of the additional integrability clause to states with positive rate. No vacuous solution predicate, unweighted moment assumption, hidden nonzero-rate condition, or proof-only theorem dependency is introduced.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 3, Theorems 3.1, 3.3, and 3.4. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4, Sections 2–3 for Feller and martingale-problem conventions, and Appendix 3 for bounded-pointwise closure. Wiley DOI

Why a complete face-vector characterization matters

A convex polytope has finitely many faces in each dimension, and their numbers form its f-vector. Determining which integer vectors occur is a basic realization problem in discrete geometry: necessary identities such as Euler's relation do not by themselves decide whether a proposed vector comes from a polytope. For simplicial polytopes, whose facets are simplices, the g-theorem gives a complete answer. In the matrix formulation recorded in Chapter 10 of Branko Grünbaum's Convex Polytopes, realizable extended f-vectors are exactly the products of M-sequences with an explicit binomial matrix.

This is a known theorem, not an open conjecture. The mission asks for a machine-checked proof of the reviewed Lean statement while preserving the theorem's full biconditional. It is not merely a collection of upper or lower bounds on individual coordinates: one side asserts geometric realizability of the whole vector, and the other gives a simultaneous arithmetic characterization.

Geometric and arithmetic setting

A d-polytope is represented as a nonempty finite convex hull in the real coordinate space Fin d → ℝ whose affine span is the whole space. A nonempty exposed face has dimension equal to the real dimension of the direction space of its affine span. The function faceCount P j counts the nonempty exposed j-dimensional faces of P.

A simplicial d-polytope is a d-polytope for which every facet is the convex hull of d affinely independent points. The extended f-vector is indexed by Fin (d+1): its coordinate f 0 is fixed to one for the empty face, while f j.succ is the integer embedding of faceCount P j for each j : Fin d.

An M-sequence in the formalization is a natural-valued function g used only from index zero through m. It begins with g 0 = 1. Each positive entry through m is either zero, with empty boundary, or is represented by a strictly increasing binomial expansion whose upper boundary is at most the preceding entry. This is the finite Macaulay condition used on printed pages 198a–198b.

The integer-valued matrix gTheoremMatrix d j k is Björner's matrix $M_d$. Its entries are

$$(M_d)_{j,k}={d+1-j\choose d+1-k}-{j\choose d+1-k},$$

with rows $0\le j\le\lfloor d/2\rfloor$ and columns $0\le k\le d$. Subtraction is performed in the integers, not truncated natural-number arithmetic.

Formalization target

For every natural dimension d and every integer vector f : Fin (d+1) → ℤ, the main item states the equivalence

$$f\text{ is the extended f-vector of a simplicial }d\text{-polytope} \quad\Longleftrightarrow\quad \exists g\text{ an M-sequence},\ f=gM_d.$$

The left side includes both f 0 = 1 and a single simplicial polytope realizing every remaining coordinate. The right side uses one M-sequence and checks the matrix equation at every column. Its sum ranges over exactly Finset.range (d / 2 + 1), so the row indices are zero through the floor of half the dimension. Values of g outside that finite range are irrelevant on both sides of the arithmetic condition.

Significance

The theorem converts a geometric existence question into an exact finite arithmetic criterion. It characterizes the entire vector at once, retaining the correlations between face numbers that coordinatewise extremal theorems cannot express. The biconditional also has two substantive directions: every simplicial polytope produces an M-sequence, and every permitted M-sequence is realized by a simplicial polytope.

Formalizing this statement supplies reusable interfaces for full-dimensional polytopes, exposed-face counts, simpliciality, finite M-sequences, and the g-theorem matrix. The theorem body remains open in the proposal. The established mathematical result is being posed as a Lean proof task rather than claimed as already machine-checked.

Difficulty

Neither direction follows from Euler or Dehn–Sommerville linear identities alone. Those equations describe an affine subspace but do not impose the nonlinear integrality and growth conditions encoded by an M-sequence. Conversely, verifying the Macaulay inequalities for a candidate sequence does not directly construct a polytope realizing all coordinates. Proving separate inequalities for each face number would also be insufficient, because the target requires one polytope and one sequence to witness simultaneous equality of the complete vectors.

Formalization scope

All ambient geometry is finite-dimensional and real. Faces use Mathlib's exposed-face convention, and faceCount excludes the empty face before assigning a natural dimension; the leading coordinate f 0 = 1 restores the empty face in the extended vector. The polytope witness is full-dimensional in Fin d → ℝ. The matrix and the target vector are integer-valued, while the M-sequence itself is natural-valued.

The mission retains all dimensions, including the low-dimensional boundary cases. Natural subtractions inside binomial indices use Lean's truncated subtraction exactly as in the reviewed source adapter, while subtraction between the two binomial coefficients occurs in ℤ. The M-sequence witness is constrained only over the finite range used by the matrix product; no unintended condition is imposed on its unused tail.

The definitions of IsDPolytope and faceCount are reused from exact private platform declarations. The simplicial predicate is reused byte-for-byte from the preceding staged package, and the M-sequence and matrix declarations preserve their reviewed local definitions with only platform-compatible module imports. Contributions should prove the iff without weakening it to one direction, replacing realizability with coordinatewise inequalities, restricting the dimension, changing the index ranges, or allowing different witnesses for different coordinates.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §10.6, printed pp. 198a–198b / PDF pp. 235–236. DOI: 10.1007/978-1-4613-0019-9.

Why simplex diffusions matter

Finite-dimensional simplices are the natural state spaces for proportions: allele frequencies, population shares, and other collections of nonnegative coordinates whose total cannot exceed one. A diffusion on such a space must do more than solve an unconstrained stochastic equation. Its covariance degenerates on the boundary, and its drift must respect every face so that the process remains in the simplex. Chapter 8 of Ethier and Kurtz develops generator results for this setting as part of the analytic foundation for Markov-process models with constrained state spaces Ethier and Kurtz, Chapter 8, §2.

This mission formalizes their Theorem 2.8, a known generation theorem rather than an open conjecture. The theorem treats arbitrary Lipschitz drift satisfying the inward boundary inequalities. It identifies the closed diffusion graph as a Feller generator and also states that polynomial restrictions form a core. The generality of the drift distinguishes this result from later population-model applications with particular mutation or selection coefficients.

The simplex and its boundary

For a positive integer $d$, the simplex state space is

$$K_d=\left\{x\in\mathbb R^d: x_i\ge 0\ \text{for every }i, \quad \sum_{i=1}^d x_i\le 1\right\}.$$

The missing mass $1-\sum_i x_i$ may be viewed as an additional coordinate. In Lean, WFState d is the subtype of functions Fin d → ℝ satisfying precisely nonnegativity and the upper bound on the coordinate sum. These conditions already imply $x_i\le 1$ for every coordinate.

Let $b:K_d\to\mathbb R^d$ be the drift. The boundary conditions say that $b_i(x)\ge 0$ whenever $x_i=0$, while $\sum_i b_i(x)\le 0$ whenever $\sum_i x_i=1$. Thus the drift cannot point outward through a coordinate face or through the top face. No mutation–selection formula or extra smoothness condition is imposed: global Lipschitz continuity and these face inequalities are the complete drift hypotheses retained here.

The operator and target theorem

The covariance matrix is

$$a_{ij}(x)=x_i(\delta_{ij}-x_j),$$

and the associated simplex diffusion operator is

$$Gf(x)=\frac12\sum_{i,j}x_i(\delta_{ij}-x_j) \,\partial_i\partial_j f(x)+\sum_i b_i(x)\,\partial_i f(x).$$

Only the second-order sum is multiplied by $1/2$. The covariance becomes singular on boundary faces, so this is not an immediate instance of a uniformly elliptic whole-space theorem.

The formal target asserts that the uniform graph closure of

$$\{(f,Gf):f\in C^2(K_d)\}$$

is single-valued and is exactly the generator graph of a positive, conservative, strongly continuous contraction semigroup on $C(K_d)$. Conservativity is expressed by preservation of the constant function $1$. The generator is identified by the right derivative at time zero, not merely by containment of a convenient operator restriction.

The final clause says that polynomials restricted to $K_d$ are a core: closing the graph obtained from polynomial first coordinates gives the same full generator graph. This is a graph-closure statement and is stronger than uniform density of polynomials as functions.

What the result provides

Single-valuedness shows that the closed graph behaves as an operator rather than a multivalued relation. Generation supplies a Feller semigroup whose positivity and preservation of constants give the Markov interpretation. The exact generator biconditional fixes the full infinitesimal domain, while the polynomial-core conclusion permits generator questions to be reduced to algebraically structured test functions without changing the closed operator.

The source theorem is already proved in the book. The formalization task is to recover its generator statement and core conclusion in Lean with all boundary, closure, and semigroup conventions explicit. The current mission contributes a source-reviewed statement and its expression-level definitions; it does not claim a completed Lean proof.

Why the formalization is delicate

The obvious route through standard elliptic diffusion generation does not apply because $a(x)$ degenerates as coordinates approach the boundary. It is also insufficient to prove only that the displayed differential operator is contained in some generator: the theorem identifies the closure of the entire $C^2(K_d)$ graph and separately asserts the polynomial core.

Boundary semantics create another source of possible weakening. Dropping either inward condition would permit outward drift at a face. Replacing the arbitrary Lipschitz drift by a special population-genetics formula would narrow the theorem. Replacing graph equality by inclusion, or polynomial graph density by ordinary function density, would lose a stated conclusion. These distinctions are all preserved in the target.

Formalization scope

The Lean development uses the book-wide namespace EthierKurtz. The compact space $C(K_d)$ is represented by real-valued bounded continuous functions on WFState d; compactness makes this the intended continuous-function space with the uniform norm. A $C^2(K_d)$ function is represented through a globally twice continuously differentiable extension on the ambient finite-coordinate space, following the book’s Appendix 6 extension convention for closed convex sets.

The operator uses Fréchet derivatives evaluated on coordinate vectors, which represent the first and second partial derivatives in the finite-dimensional ambient space. The graph is closed in the product uniform norm. IsStronglyContinuousContractionSemigroup records identity at zero, the nonnegative-time semigroup law, contraction, and strong right continuity at zero. The target additionally records positivity, preservation of one, and equality between its derivative graph and the closed diffusion graph.

The scope excludes the zero-dimensional case, as required by 0 < d. It does not introduce a continuous-path hypothesis, a special drift parameterization, or uniform ellipticity. The only packaged declarations beyond the goal are the state space, operator, graph, and the already published semigroup predicate needed to state it. Proof-only lemmas and unrelated Chapter 8 results are outside this mission.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, §2, Theorem 2.8, printed p. 375; equation (1.15), printed p. 368; Appendix 6, printed pp. 499–500. DOI

Why endpoint classification matters

A one-dimensional diffusion is governed in the interior by a second-order differential operator, but the interior coefficients alone do not determine what happens when the process approaches the edge of its state space. An endpoint may be reachable from the interior or inaccessible; after arrival it may absorb, reflect, or retain the process according to a boundary parameter. The same issue persists when an endpoint is infinite. Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), organizes these alternatives through scale and speed integrals and identifies the exact operator domain that generates the corresponding Feller evolution. This mission formalizes Chapter 8, Section 1, Theorem 1.1, printed page 367.

The setting

Let $-\infty\le r_0<r_1\le\infty$. The real state interval is $I=[r_0,r_1]\cap\mathbb R$, its interior is $I^\circ=(r_0,r_1)$, and $\bar I$ is the closed interval in the extended real line. A function in $C(\bar I)$ is represented by a continuous function on that compact extended interval, so finite endpoint limits are part of the object even when an endpoint is infinite.

The interior diffusion operator is

$$Gf(x)=\frac{a(x)}2 f''(x)+b(x)f'(x),$$

where $a$ and $b$ are continuous on $I^\circ$ and $a(x)>0$ there. Choose an interior reference point $r$. Define

$$B(x)=\int_r^x \frac{2b(y)}{a(y)}\,dy, \qquad p(x)=\int_r^x e^{-B(y)}\,dy, \qquad m(x)=\int_r^x \frac{2e^{B(y)}}{a(y)}\,dy.$$

The corresponding endpoint tests $u$ and $v$ are nonnegative extended-real integrals. Their values may be $+\infty$; preserving that possibility is essential because the four boundary classes are distinguished precisely by which of the two tests are finite.

Formalization target

Theorem 1.1 — one-dimensional boundary diffusion generation

At either endpoint, the pair $(u,v)$ gives the Feller boundary class:

$$\begin{array}{c|cc} \text{class} & u & v\\ \hline \text{regular} & <\infty & <\infty\\ \text{exit} & <\infty & =\infty\\ \text{entrance} & =\infty & <\infty\\ \text{natural} & =\infty & =\infty. \end{array}$$

Entrance and natural endpoints are inaccessible, so the generator domain imposes no boundary equation there. At an exit endpoint the limiting generator value must be zero. At a regular endpoint $r_i$, a parameter $q_i\in[0,1]$ determines the boundary condition

$$q_i\lim_{x\to r_i}Gf(x) =(-1)^i(1-q_i)\lim_{x\to r_i}e^{B(x)}f'(x).$$

The target states that the graph consisting of $f\in C(\bar I)$ that are twice continuously differentiable in the interior, whose $Gf$ extends continuously to $\bar I$, and that satisfy the applicable condition at both endpoints is exactly the infinitesimal generator of a Feller semigroup on $C(\bar I)$. The conclusion includes the semigroup law, contraction, strong right continuity at zero, positivity, preservation of the constant function $1$, and a biconditional identifying the complete generator graph rather than merely an included core or its closure.

Significance

The theorem translates local coefficients into a global Markov evolution while retaining every possible finite or infinite endpoint type. The endpoint tests determine which boundary behavior is available, and the regular-boundary parameter records absorbing, reflecting, and intermediate behavior in one equation. Without the classification, writing down the differential expression does not specify a unique Feller generator because distinct domains can encode different stochastic behavior at the same endpoint.

The formal contribution is a machine-checkable statement layer for the source theorem. It makes the compactified state space, improper endpoint integrals, one-sided endpoint filters, and exact generator graph explicit. The theorem itself remains an open proof obligation in this statement-only mission. The definitions can also support later formal work on hitting distributions, killed or reflected diffusions, and comparison of boundary regimes.

Where the difficulty lies

The main difficulty is that the classification cannot be reduced to ordinary finite integrals or to boundary values at finite real points. Infinite endpoints and divergent scale or speed tests carry mathematical information; replacing extended-real integrals by totalized real integrals would collapse boundary classes. A second difficulty is identifying the full closed generator domain. Showing that the differential expression is meaningful on smooth interior functions is insufficient: the proof must connect its endpoint asymptotics to positivity, conservativity, strong continuity, and exact generation on the uniform-norm space.

Formalization scope and conventions

Endpoints use EReal, and the state space is Set.Icc r₀ r₁ in the extended line. Coefficients are constrained only on the open real interior; no boundedness or uniform ellipticity is added. The drift primitive and scale/speed tests use oriented interval integrals internally and ENNReal endpoint integrals externally, retaining $+\infty$. Absolute values correct the orientation on the left of the reference point.

The graph stores continuous endpoint extensions of both $f$ and $Gf$. Interior $C^2$ regularity is expressed by ContDiffOn ℝ 2, and endpoint limits use the one-sided neighborhood filter induced from the extended interval. The regular parameter is required to lie in $[0,1]$ only when both boundary tests are finite. The mission does not replace the four cases by an opaque classifier, assume finite endpoints, add a pathwise stochastic differential equation, or weaken exact generation to graph inclusion. The shared book definition of a strongly continuous contraction semigroup is reused from the earlier semigroup-generation mission rather than redeclared.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 1, Theorem 1.1 and equations (1.1)–(1.11), printed pp. 366–367. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4, printed p. 166, for the Feller semigroup convention used in the conclusion. Wiley DOI

Why whole-space diffusion generators matter

Diffusion processes connect stochastic differential equations, partial differential equations, and Markov semigroups. On Euclidean space, their local behavior is encoded by a second-order operator built from a covariance field and a drift field. A central question is whether those local coefficients determine an actual Markov evolution, and whether the resulting evolution is unique. Ethier and Kurtz organize these questions through generator graphs and martingale problems, which allow the same language to cover smooth elliptic diffusions, degenerate models, and coefficients that vary measurably with time. This mission formalizes three complementary whole-space regimes from Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), principally Theorems 1.6, 1.7, and 2.5.

The setting

The state space is the finite-dimensional Euclidean space $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d), with $d>0$. A covariance operator $a(t,x)$ is a continuous linear endomorphism of this space, while a drift $b(t,x)$ is a vector. For a smooth scalar test function $f$, the diffusion operator is

$$G_t f(x)=\frac12\sum_{i,j} a_{ij}(t,x)\,\partial_{ij}f(x) + Df(x)[b(t,x)].$$

The factor $1/2$ multiplies only the covariance-weighted second-order term. The formalization uses Fréchet derivatives evaluated in the standard coordinate directions. In the time-homogeneous cases, the smooth compactly supported graph consists of pairs $(f,Gf)$ viewed in $C_0(\mathbb R^d)\times C_0(\mathbb R^d)$, and its uniform closure is the candidate generator.

For time-dependent coefficients, a measurable process solves the time-inhomogeneous martingale problem when its initial pushforward law is prescribed and the integrated generator identity holds against every smooth compactly supported spatial test and every bounded continuous finite-history test. This formulation records the natural-past moment identities without imposing continuity of sample paths as an extra hypothesis.

Formalization targets

Goal: measurable-drift nonautonomous well-posedness

The main target is Chapter 8, Section 1, Theorem 1.7. The covariance and drift are jointly Borel measurable and locally bounded. The covariance is symmetric and nonnegative. At each fixed spatial point it is uniformly elliptic over every bounded positive time interval, and its spatial continuity is uniform over that interval. A common quadratic bound controls the covariance norm and the one-sided radial drift quantity $\langle x,b(t,x)\rangle$.

For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every such solution on any probability space. The drift is not assumed continuous, and no stronger norm-growth condition on the drift or moment condition on the initial law is inserted.

Related target: uniformly elliptic Feller generation

Chapter 8, Section 1, Theorem 1.6 treats bounded Hölder continuous time-homogeneous coefficients with symmetric, globally uniformly elliptic covariance. It concludes that the closure of the smooth compactly supported graph is single-valued and is exactly the generator of a positive, strongly continuous contraction semigroup on $C_0(\mathbb R^d)$. Conservativity is retained through membership of the constant graph pair $(1,0)$ in the bounded-pointwise closure.

Related target: degenerate smooth-core generation

Chapter 8, Section 2, Theorem 2.5 permits degenerate and unbounded covariance fields. Its assumptions are symmetry, nonnegativity, twice continuous differentiability of the matrix entries, bounded second partial derivatives, and a globally Lipschitz drift. Its conclusion is the same full Feller generation and conservativity statement. This regime is related to, but not implied by, the bounded uniformly elliptic regime.

Significance

Together the three statements separate distinct mechanisms for obtaining Markov dynamics from local diffusion data. The two autonomous theorems identify when a concrete smooth core closes to a Feller generator, including positivity, contraction, strong continuity, and conservativity. The nonautonomous theorem establishes existence and uniqueness in distribution under substantially rougher temporal behavior and merely measurable drift. Keeping the regimes together exposes the common operator while preserving their incompatible regularity hypotheses.

The formal contribution is a machine-checkable statement layer for these source results and their expression-essential definitions. It does not claim proofs of the theorems. The definitions make explicit the coordinate form of the generator, the $C_0$ graph, the bounded-pointwise closure convention, and the complete finite-history martingale identities. These components can support later formal proofs and other diffusion or martingale-problem developments.

Where the difficulty lies

The source conclusions are not consequences of a single elementary continuity argument. In the Feller cases, identifying the closure of a graph with the generator requires simultaneous control of the operator domain, the semigroup properties, positivity, and conservativity. In the time-dependent case, measurability of the drift is deliberately weaker than continuity, while uniqueness must cover all measurable-process realizations and all finite collections of observation times. Replacing that conclusion by uniqueness only among continuous processes, or strengthening the drift hypotheses until a standard smooth theory applies, would change the theorem.

Formalization scope and conventions

The development uses nonnegative real time and finite-dimensional real Euclidean space. Covariance matrices act as continuous linear maps; their entries are recovered in the standard orthonormal basis. Smoothness is expressed with ContDiff, compact support with HasCompactSupport, and autonomous generator graphs in C₀. The bounded-pointwise closure is the smallest set closed under uniformly bounded pointwise sequential limits, not merely the set of one-step limits.

The martingale-problem predicate requires joint measurability of the process, equality of the initial pushforward measure, and all bounded continuous finite-history identities. Empty histories and repeated observation times are included. The goal compares the complete finite-dimensional laws of any two solutions. No vacuous solution predicate, arbitrary extension of the generator, chosen matrix square root, hidden path-continuity assumption, or proof-only theorem dependency is used.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Theorems 1.6, 1.7, and 2.5. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4 for martingale-problem well-posedness and Feller conventions, and Appendix 3 for bounded-pointwise closure. Wiley DOI

Why stationary dependence matters

Classical central limit theorems begin with independent observations. Many stochastic models instead produce observations whose dependence persists across time: measurements from an equilibrium process, functions of a stationary Markov chain, and noise sequences in time-series models are standard examples. For such data, the variance of a long sum contains covariance terms from every lag, and independence cannot be used to discard them. Chapter 7, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), gives a functional central limit theorem under a quantitative mixing condition. The conclusion is stronger than convergence of one normalized sum: the whole partial-sum path converges to Brownian motion.

Stationary sequences and mixing

Fix a probability space $(\Omega,\mathcal F,P)$ and a two-sided real sequence $(Y_k)_{k\in\mathbb Z}$. Strict stationarity means that shifting every integer index by the same amount leaves the joint law of the entire sequence unchanged. Each $Y_k$ is measurable and centered, so $E[Y_k]=0$.

For a nonnegative lag $m$, let the past be the sigma-algebra generated by all $Y_k$ with $k\le 0$, and let the future be generated by all $Y_k$ with $k\ge m$. For $p\ge 1$, the book's $L^p$ mixing coefficient $\varphi_p(m)$ is the supremum, over future events $A$, of

$$\left\|P(A\mid\text{past})-P(A)\right\|_p.$$

Thus $\varphi_p(m)$ measures how far events at least $m$ time units in the future remain from being independent of the complete past. The Lean definition constructs both coordinate-generated sigma-algebras explicitly and represents conditional probability as the conditional expectation of an indicator.

Formalization target

For $n\ge 1$, define the scaled partial-sum process

$$X_n(t)=\frac{1}{\sqrt n}\sum_{k=1}^{\lfloor nt\rfloor}Y_k, \qquad t\ge 0.$$

The Lean sequence uses the index $n+1$ because Lean's natural numbers begin at zero; this is only a reindexing of the same positive scaling sequence. Suppose there is $\delta>0$ such that every coordinate has a finite $(2+\delta)$ moment. Set

$$p=\frac{2+\delta}{1+\delta}, \qquad \sum_{m=0}^{\infty}\varphi_p(m)^{\delta/(1+\delta)}<\infty.$$

The target is Theorem 3.1: the ordered covariance series converges and

$$\sigma^2=E[Y_1^2]+2\sum_{k=2}^{\infty}E[Y_1Y_k]$$

is nonnegative, while $X_n$ converges to centered Brownian motion with variance parameter $\sigma^2$. The variance is allowed to be zero. The covariance sum is encoded as convergence of its ordered partial sums, not as the stronger and unrequested assertion of absolute summability.

What the conclusion provides

The result identifies the macroscopic fluctuation process of a stationary dependent sequence. It supplies both the long-run variance, including every lag covariance, and a Brownian path limit. Consequently, continuous functionals of the accumulated process can be studied through the limiting Brownian motion rather than only through one-time normal approximations.

The formal statement preserves the book's functional interpretation. ConvergesToContinuousGaussian records the complete prelimit path laws, centered Gaussian finite-dimensional laws with covariance $\sigma^2\min(s,t)$, and convergence to a continuous limit through a common realization. This avoids weakening the theorem to convergence of a single terminal sum or to separate finite-dimensional marginals. The declaration is a statement-only formalization: the theorem remains an open Lean goal, while the mixing coefficient and partial-sum process are concrete definitions.

Where the difficulty lies

The usual independent-sum argument does not apply because blocks of observations are not independent and their covariance terms need not vanish. Merely showing that dependence becomes small at large lags is insufficient: the decay must interact with the available $(2+\delta)$ moment so that the total contribution of distant dependence is summable. A scalar central limit theorem would also leave tightness of the path sequence unresolved. The theorem packages both issues into the summability condition on the precise $L^p$ coefficient and concludes a path-level Brownian limit.

Formalization scope and conventions

The formalization uses a two-sided sequence indexed by $\mathbb Z$, matching the source's convenient stationary extension. Stationarity is equality of the laws of the whole shifted and unshifted sequence, which entails every finite-dimensional shift identity without adding Markov or independence assumptions. The probability measure is explicit, and every coordinate has an explicit measurability hypothesis.

stationaryLpMixing uses the past through zero and the future beginning at lag $m$. Its codomain is the extended nonnegative reals, so an infinite norm or supremum is not silently totalized to an ordinary real. The summability hypothesis is an extended-real infinite sum strictly below infinity. stationaryPartialSums embeds the real sum in one-dimensional Euclidean space so it can reuse the book-wide continuous-Gaussian path-convergence definition. The exact floor, positive indexing, square-root normalization, covariance order, and degenerate zero-variance case are retained. No interpolation, absolute covariance summability, positive-variance assumption, Markov property, or independence condition is introduced.

The expression-essential infrastructure consists of the two definitions introduced here and the compatible book-wide ConvergesToContinuousGaussian definition already staged for the preceding diffusion-limit mission. The latter is imported rather than duplicated under a conflicting name. Useful future work includes proving the theorem from martingale approximation and developing reusable results relating concrete mixing bounds to the required summability hypothesis.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 7, Section 3, Theorem 3.1, printed pp. 350–351; mixing convention in Section 2, printed pp. 345–346. Wiley DOI

Why diffusion limits matter

Many stochastic models are built from small random changes occurring at high frequency. Queue lengths, population counts, particle systems, and numerical schemes may be discrete or have jumps at every finite scale, yet their large-scale behavior is often described by a continuous diffusion. A diffusion approximation replaces the detailed microscopic model by a process whose drift and covariance depend on its current state. This can make asymptotic probabilities and qualitative behavior accessible without claiming that the original model itself has continuous paths.

Chapter 7 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, develops general limit theorems for this passage. The retained results in this mission are Theorem 1.4, a martingale functional central limit theorem with deterministic covariance, and Theorem 4.1, a state-dependent diffusion approximation from localized characteristics. They are related limit regimes, but the former is not presented here as a literal specialization of the latter: its covariance may vary deterministically with time, whereas the state-dependent theorem uses time-homogeneous coefficient fields evaluated along the evolving state.

The probabilistic setting

A càdlàg process is right-continuous and has a finite left limit at every positive time. For each index $n$, the state process $X_n$ and its finite-variation characteristic $B_n$ have càdlàg paths in $\mathbb R^d$. A symmetric matrix process $A_n$ has càdlàg entries and positive-semidefinite increments. The natural filtration records the histories of $X_n$, $B_n$, and $A_n$ jointly.

The centered process $M_n=X_n-B_n$ is required to be a local martingale coordinatewise. Its quadratic characteristic is represented by requiring every product

$$M_n^i M_n^j-A_n^{ij}$$

to be a local martingale as well. These conditions identify $B_n$ as the approximate drift and $A_n$ as the approximate covariance accumulation. They do not impose independence of the coordinates or of the prelimit processes.

Localization uses the first time $\tau_n^r$ at which either the current value $X_n(t)$ or its left limit $X_n(t-)$ reaches radius $r$. The jump and characteristic conditions are checked only up to $T\wedge\tau_n^r$, for each radius $r>0$ and time horizon $T>0$. This is essential when coefficients are controlled locally but not globally.

Formalization targets

State-dependent diffusion approximation

Let $a(x)$ be a continuous symmetric positive-semidefinite matrix field and let $b(x)$ be a continuous vector field. For smooth compactly supported $f$, define

$$Gf(x)=\frac12\sum_{i,j}a_{ij}(x)\,\partial_i\partial_jf(x) +\sum_i b_i(x)\,\partial_i f(x).$$

Assume the continuous-path martingale problem for this operator is well posed for every initial probability law. The goal states that if the stopped squared jumps of $X_n$ and $B_n$ vanish in expected supremum, the stopped first-power jumps of each $A_n^{ij}$ vanish, and the stopped characteristics converge in probability to

$$\int_0^t b_i(X_n(s))\,ds \quad\text{and}\quad \int_0^t a_{ij}(X_n(s))\,ds,$$

then weak convergence of the initial laws implies convergence of the complete path laws to the unique continuous diffusion law.

Martingale functional central limit theorem

The retained milestone treats vector local martingales with deterministic limiting covariance $C(t)$. It preserves both alternatives in the source: either first-power martingale jumps vanish and $A_n$ is the actual cross variation, or the jumps of $A_n$ and the squared jumps of the martingale vanish while $M_n^iM_n^j-A_n^{ij}$ is locally martingale. Pointwise convergence in probability of $A_n^{ij}(t)$ to $C_{ij}(t)$ then yields the centered continuous Gaussian limit with covariance $C(\min(s,t))$.

Significance

The state-dependent theorem packages a common diffusion-limit argument into conditions on observable local characteristics. It separates model-specific work—identifying the drift, covariance, localization, and jump bounds—from the general conclusion that the entire trajectory converges. The martingale theorem records the important deterministic-covariance regime without erasing either of its two source alternatives.

For formalization, the mission provides concrete predicates for càdlàg paths, stopped maximum jumps, localized characteristic discrepancies, the diffusion generator, continuous martingale-problem laws, and Gaussian process convergence. The result is statement-only: the theorem bodies remain open with sorry, while every expression dependency is a concrete definition. No theorem proof, adapter-equivalence proof, or claim of completed formal verification is included.

Where the difficulty lies

Finite-dimensional convergence alone does not control whole trajectories. The central obstacle is simultaneous control of oscillations, jumps, and characteristics after localization. A naive argument that replaces $B_n$ and $A_n$ by their limiting integrals pointwise misses the uniform stopped discrepancies and does not justify tightness of path laws. Likewise, ignoring the left limit in the exit rule can miss a jump that crosses the localization boundary.

Well-posedness is also substantive. Identifying every subsequential limit with a solution of the martingale problem gives uniqueness only when that problem is well posed for the relevant initial law. The formal statement therefore retains existence and uniqueness for every initial probability law rather than silently assuming a distinguished solution.

Formalization scope

Time is nonnegative and the sequence is indexed from zero rather than one. Expectations of jump suprema take values in $\mathbb R_{\ge0}\cup\{\infty\}$, so no unmentioned integrability assumption is introduced. Matrix positivity is Matrix.PosSemidef, which includes the real symmetric positive-semidefinite condition used by the source. The exit time includes both the current value and the positive-time left limit, and an empty exit set gives infinity.

The diffusion law uses continuous canonical paths, smooth compactly supported tests, and bounded measurable functions of finitely many past states to express the natural-filtration martingale identities. Full process convergence is encoded by a joint realization that preserves every complete prelimit path law and converges almost surely uniformly on each compact interval to a continuous limit. This is the source-reviewed continuous-limit Skorohod representation convention, not merely convergence of finitely many observations.

The two shared definitions EthierKurtz.IsSourceLocalMartingale and EthierKurtz.HasCrossVariation are imported from the earlier book-wide stochastic-calculus package. All other definitions needed to state these two results are included here. Contributions should preserve the localization quantifiers, both central-limit jump alternatives, the full martingale-problem well-posedness hypothesis, and the complete path-law conclusions.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 7, Sections 1 and 4, Theorems 1.4 and 4.1. Wiley digital edition

Brownian equations as models of evolving systems

A Brownian stochastic equation describes a state that changes through a deterministic drift and random fluctuations. Such equations are basic models for diffusions and connect probabilistic sample paths with analytic operators. Chapter 5, Section 3 of Stewart Ethier and Thomas Kurtz's Markov Processes: Characterization and Convergence develops this connection in both directions and then separates three questions: whether a solution exists, whether it is unique when driven by fixed noise, and whether all solutions have the same distribution. The mission records four central results from that section as one coherent formalization target. The principal goal is the fixed-driver existence theorem, Theorem 3.11. Theorems 3.3, 3.6, and 3.10 retain the representation, uniqueness, and weak-existence variants without treating one as a consequence of another.

State space, coefficients, and solutions

Fix a dimension $d$. The state space is the Euclidean space $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d). A diffusion coefficient

$$\sigma:[0,\infty)\times\mathbb R^d\longrightarrow\mathbb R^{d\times d}$$

controls the random fluctuations, and a drift coefficient

$$b:[0,\infty)\times\mathbb R^d\longrightarrow\mathbb R^d$$

controls the finite-variation part. Given a $d$-dimensional Brownian motion $W$ and initial state $\xi$, a solution $X$ satisfies, componentwise,

$$X(t)=X(0)+\int_0^t \sigma(s,X(s))\,dW(s)+\int_0^t b(s,X(s))\,ds.$$

The formal statement does not postulate an opaque stochastic-integral operator. The predicate HasBrownianItoIntegral uses bounded predictable dyadic step approximations, integrated squared-error convergence in probability, and convergence in probability of the corresponding stochastic sums. SolvesBrownianSDE requires continuous paths, adaptation to the completed natural past of $W$ and $\xi$, integrability of the drift, and one almost-sure equation holding for every time and coordinate.

A weak solution may choose its probability space, filtration, and Brownian driver. Its Brownian future increments are independent of the entire filtration past, its state process is adapted after completion, and its initial distribution is prescribed. Pathwise uniqueness compares two solutions on the same space with the same filtration and driver. Distribution uniqueness compares solutions that may live on different spaces and asks for equality of their whole coordinate-path laws.

Formalization targets

Theorem 3.3: martingale-problem representation

For locally bounded Borel coefficients, a given continuous solution of the diffusion martingale problem can be lifted to the completed product with an auxiliary Brownian space. On that specific extension there exists a Brownian motion making the lifted original process a weak solution of the stochastic equation. The generator is

$$Gf(t,x)=\frac12\sum_{i,j}(\sigma\sigma^{\mathsf T})_{ij}(t,x)\,\partial_i\partial_j f(x)+\sum_i b_i(t,x)\,\partial_i f(x).$$

This target retains the factor $1/2$, the complete drift term, possibly singular diffusion matrices, the given process, and the exact completed product filtration.

Theorem 3.6: uniqueness implication

For locally bounded Borel $\sigma$ and $b$ and any initial probability law $\mu$, pathwise uniqueness implies uniqueness in distribution. No existence, Lipschitz, ellipticity, or moment assumption is added.

Theorem 3.10: weak existence

When both coefficients are continuous and a constant $K$ satisfies

$$\lVert\sigma(t,x)\rVert^2\le K(1+\lVert x\rVert^2),\qquad x\cdot b(t,x)\le K(1+\lVert x\rVert^2),$$

there is a weak solution for every initial probability law. The drift hypothesis is one-sided and does not bound $\lVert b(t,x)\rVert$.

Theorem 3.11: strong existence on fixed noise

The main goal assumes locally bounded Borel coefficients, the preceding one-sided growth condition locally in time, and local Lipschitz control on each bounded state ball. For every Brownian motion $W$ and every independent square-integrable initial variable $\xi$ already given on a probability space, there exists $X$ solving the equation with respect to the completed natural past of $W$ and $\xi$. The quantifier order preserves the fixed driver and original probability space.

Why these results matter

The representation theorem connects the analytic martingale problem with the pathwise stochastic-integral formulation while preserving a given process on a prescribed extension. The uniqueness theorem explains when the apparently stronger same-noise comparison controls the law of arbitrary weak solutions. The weak-existence theorem supplies solutions under continuity and one-sided growth without local Lipschitz assumptions. The strong-existence theorem supplies a solution driven by noise and initial data that are fixed in advance, under local Lipschitz regularity.

Formalizing the group creates reusable definitions for completed filtrations, Brownian drivers, local Itô integration, weak solutions, pathwise uniqueness, and time-dependent diffusion generators. The source results are classical theorems, and this proposal records their reviewed Lean statements as open proof obligations. It does not claim machine-checked proofs.

Main formalization difficulty

The central difficulty is keeping the probabilistic quantifiers and filtrations exact. Replacing the local stochastic integral by an unconstrained witness would make the equation too weak. Replacing weak existence by existence on a fixed space would make Theorem 3.10 too strong. Conversely, existentially choosing a new driver in Theorem 3.11 would lose its fixed-noise content. The representation theorem also cannot be reduced to equality in law: it must retain the original process through first projection and use the completed product past specified in the source.

Formalization scope

Time is ℝ≥0, states are finite-dimensional real Euclidean spaces, and diffusion matrices use the Frobenius norm. Brownian motion is represented by independent scalar Brownian coordinates with measurable evaluations and continuous paths. Completion adds every subset of an ambient measurable null set. The local Itô relation uses left-endpoint dyadic step functions, interval integrability, and convergence in probability. Equality of path laws is expressed on the coordinate function space; for continuous Euclidean paths this matches the usual continuous-path law.

The main theorem keeps Borel measurability, compact-set local boundedness, one-sided drift growth, squared diffusion growth, local Lipschitz bounds, independence of $\xi$ and $W$, and the second moment of $\xi$. The weak theorem keeps continuity and an arbitrary initial law. The representation target keeps compactly supported smooth tests and the exact covariance contraction. These conditions rule out vacuous solution predicates and default-valued integrals. Contributions may prove the four theorem statements or establish reusable lemmas for the concrete integral, completion, martingale, and path-law infrastructure.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 5, Section 3, Theorems 3.3, 3.6, 3.10, and 3.11. Wiley

Motivation

A continuous stochastic process may combine a finite-variation drift with a local martingale fluctuation. To understand a function of that process, one needs a change-of-variables rule that accounts for both parts and for their quadratic covariation. The ordinary chain rule has no term for covariation. The result here is the time-dependent, multidimensional Itô formula in Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), Chapter 5, Section 2, Theorem 2.9, printed page 287 (PDF page 296). It applies to arbitrary continuous semimartingales satisfying the stated decomposition; its input is not restricted to a particular stochastic differential equation.

Setting

Time is the nonnegative real half-line and the state has d real coordinates, indexed by Fin d. The sample space Ω has a complete probability measure P and a filtration ℱ. The initial sigma algebra contains every ambient measurable null set. For each coordinate i, V_i is a continuous adapted finite-variation process, zero at time zero; M_i is a continuous adapted local martingale, zero at time zero almost surely. The process X_i has an ℱ₀-measurable initial value and satisfies X_i(t)=X_i(0)+V_i(t)+M_i(t) for all times and samples.

The test function f(t,x) has a continuous first time derivative, continuous first spatial derivatives, and continuous second spatial derivatives. At time zero, the time derivative is taken within the nonnegative-time domain. The notation f_t, f_{x_i}, and f_{x_i x_j} denotes these derivative witnesses. The conclusion supplies processes representing the continuous cross variations and integrals; their existence is part of the theorem. The Stieltjes relations use pathwise left dyadic sums for continuous finite-variation integrators. Martingale integrals and cross variations use convergence in probability of their corresponding dyadic sums. The integral versions are continuous and adapted where the theorem requires those properties.

Formalization targets

Theorem 2.9 — time-dependent multidimensional Itô formula

For every t ≥ 0, outside one null set independent of t, the target is

$$\begin{aligned} f(t,X(t))-f(0,X(0))={}&\int_0^t f_t(s,X(s))\,ds\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dV_i(s)\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dM_i(s)\\ &+\frac12\sum_{i,j}\int_0^t f_{x_i x_j}(s,X(s))\,d\langle M_i,M_j\rangle_s. \end{aligned}$$

The goal is EthierKurtz.ito_formula. It retains every term and both coordinate indices in the cross-variation sum. The bracket and integral witnesses are existential conclusions, so the statement does not require their existence as an extra hypothesis on X.

Significance

The formula identifies the effect of a smooth, time-dependent transformation on any process with the stated continuous semimartingale decomposition. In particular, it exposes the second-order correction that distinguishes stochastic change of variables from deterministic calculus. This makes it a general calculus result that can later be applied to diffusion equations, martingale problems, and transformed processes, independently of how the input process was constructed.

The cited theorem is established in the source book. This mission provides a compiled Lean statement and concrete expression dependencies; it does not provide a Lean proof. Formalizing the proof would require the stochastic-integral and covariation infrastructure to support the source's continuous local-martingale setting and version conventions. A solver's result should prove this full statement or develop reusable infrastructure that supports it without changing its hypotheses or conclusion.

Difficulty

The ordinary deterministic chain rule cannot account for the double sum of cross variations. A statement limited to Brownian motion, an absolutely continuous bracket, or a fixed stochastic differential equation would omit cases covered by the source. The local-martingale integral also needs a continuous adapted version with a common almost-sure interpretation over all times; merely obtaining a separate fixed-time limit does not by itself supply that final identity. These requirements make the exact scope of the integral and bracket relations central to the formalization.

Formalization scope

The Lean declaration uses ℝ≥0 for time, Fin d → ℝ for state vectors, Measure Ω for the probability law, and Filtration ℝ≥0 for the filtration. It includes completeness of P, the initial-null-set condition on ℱ 0, continuity and adaptation of V and M, local bounded variation of V, stopping-time localization for M, the full decomposition of X, and continuous derivative witnesses for f. The final almost-everywhere quantifier precedes the universal time quantifier. There is no Brownian driver, global square-integrability requirement, right-continuity assumption on the filtration, or diagonal-only bracket simplification.

Five definitions are expression dependencies: IsSourceLocalMartingale, HasCrossVariation, itoStepSum, HasContinuousStieltjesIntegral, and HasContinuousMartingaleIntegral. Their staged declarations retain the reviewed source definitions under a consistent EthierKurtz namespace. The dyadic-sum definitions do not embed the change-of-variables identity, so the theorem cannot be discharged by unfolding a definition of the desired answer. The mission asks for a proof of the stated result, not a weakened special case. The empty-coordinate case is admitted consistently; no positive-dimensional source case is excluded.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986 (held reprint 1986/2005), Chapter 5, Section 2, Theorem 2.9, printed p. 287 (PDF p. 296), equations (2.40)–(2.41). Conventions: printed pp. 279–280 and 286 (PDF pp. 288–289 and 295). Cross variation: Chapter 2, equation (6.4), printed p. 79 (PDF p. 88).

Motivation

Continuous-time Markov processes are often studied through operators that describe how observables evolve. The generation question asks when an operator specified on a domain actually determines a strongly continuous family of contractions. Ethier and Kurtz place this question at the start of Markov Processes: Characterization and Convergence because the resulting semigroup language supports their later treatment of processes and convergence. This mission records the full generation characterization in Chapter 1, Theorem 2.6, and retains the related perturbation result in Theorem 7.1.

Setting

Let (E) be a real Banach space. A linear operator (A) has a linear domain (D(A)\subseteq E), which need not equal (E). A family (T(t)), for nonnegative real (t), consists of bounded linear maps (E\to E). It is a strongly continuous contraction semigroup when (T(0)) is the identity, (T(s+t)=T(s)T(t)), every (T(t)) has norm at most one, and (T(t)x\to x) as (t\downarrow0) for every (x\in E). Its infinitesimal generator has exactly those (x) for which the right-hand difference quotient (t^{-1}(T(t)x-x)) converges, and sends each such (x) to the limit.

An operator is dissipative here when

$$r\lVert x\rVert\leq\lVert rx-Ax\rVert \quad(x\in D(A),\ r>0).$$

The range condition for a positive (r) says every vector in (E) is (rx-Ax) for some (x\in D(A)). Density means that vectors in (D(A)) approximate every vector in (E). These are independent requirements in the formal statement; neither the domain nor the operator is assumed closed or bounded.

For the related perturbation theorem, (A) and (B) may have different domains. Their sum uses the intersection of those domains. Closure is closure of the graph in (E\times E). A graph closure is required to be the graph of a single-valued operator before it can be called a generator.

Formalization targets

Theorem 2.6: generation characterization

The goal is the equivalence

$$A\text{ generates a strongly continuous contraction semigroup} \quad\Longleftrightarrow\quad \overline{D(A)}=E,\quad A\text{ is dissipative},\quad \operatorname{Ran}(rI-A)=E\text{ for some }r>0.$$

The left side uses the full infinitesimal-generator domain, rather than agreement with a generator only on a smaller subdomain. The right side includes dissipativity for every positive parameter and full surjectivity for at least one positive parameter.

Theorem 7.1: relatively bounded perturbation

The retained related result assumes that the closure of (A) is single-valued and generates a strongly continuous contraction semigroup, (D(A)\subseteq D(B)), and (B) is dissipative. It further assumes

$$\lVert Bx\rVert\leq\alpha\lVert Ax\rVert+\beta\lVert x\rVert \quad(x\in D(A)),\qquad 0\leq\alpha<1,\quad\beta\geq0.$$

It concludes that the closure of (A+B) is single-valued and generates such a semigroup, and that its entire graph equals the sum of the graph closures of (A) and (B). This theorem is a related generation variant within the same mission, not a separate main goal.

Significance

The equivalence turns an existence question about a family of operators into conditions on a single potentially unbounded operator. In particular, it preserves the exact-domain requirement: proving only that a semigroup generator extends (A) would answer a weaker question. The perturbation theorem then identifies circumstances under which an already generating operator remains useful after adding a dissipative term that need not itself be bounded.

The textbook proves both statements. The Lean files supplied here are statements with intentional proof holes; they do not claim machine-checked proofs. A completed formalization would supply proofs of these source results while keeping the domain, range, closure, and relative-bound conditions shown in the statements.

Difficulty

The hypotheses describe a linear map on only part of the Banach space, while the conclusion requires bounded operators on all of (E) at every nonnegative time. Checking a semigroup law on a convenient subspace is insufficient unless the resulting operators and generator have the stated full domains. For perturbations, graph closure can enlarge a domain. An equality of formulas on (D(A)) alone would therefore omit the theorem's graph and domain conclusion.

Formalization scope

Lean uses NormedAddCommGroup E, NormedSpace ℝ E, and CompleteSpace E for the real Banach space; Submodule ℝ E for each domain; D →ₗ[ℝ] E for an operator that need not be bounded; and E →L[ℝ] E for each semigroup operator. Semigroup values at negative real times are unconstrained. The derivative is the right limit through positive times. Graph closure is topological closure in the ambient product, and graph sum requires a common input. The strict relative bound (\alpha<1) and positive resolvent parameter remain explicit.

The reusable definitions are the semigroup predicate, full generator predicate, operator graph, and graph sum. The mission welcomes proofs of the two stated theorems and genuinely source-based supporting lemmas. A model with an empty operator domain, an operator restricted from a larger generator, or a conclusion that drops the graph equality would not satisfy the target.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 1, Sections 2 and 7, Theorems 2.6 and 7.1. Book record.